IsarMathLib 1.28.0: Binomial theorem

This release adds the binomial theorem to IsarMathLib. Binomial theorem is an elementary result stating that in commutative rings $(x+y)^n = \sum_{k=0}^n {n \choose k} x^{n-k} y^k$ .
The assertion of the theorem as it is presented on the isarmathlib.org site actually reads $(x+y)^n = \sum \{\langle k,{n \choose k} x^{n-k} y^k\rangle. k\in n+1\}$ which probably requires some explanation.
The first question a reader may have is: Why the summation sign does not have limits like in the standard mathematical notation? I guess setting up such notation in Isabelle/ZF would be possible, perhaps with some Standard ML code, but I don’t know how to do that. Instead, the $\sum$ symbol is defined as an operator that expects a list as its argument (see the ring3 locale). A list in IsarMathLib is a function whose domain is an initial segment of the set of natural numbers, like $\{0,1,2,...,n\}$ where $n$ is a natural number. Functions in ZF set theory are sets of (argument,value) pairs, hence that $\langle k,{n \choose k} x^{n-k} y^k\rangle$ syntax. Now what does that mean that $k \in n+1$ ? The natural numbers in ZF set theory are defined so that zero is the empty set and for $n>0$ we have $n = \{0,1,...,n-1\}$ . Hence, the notation $k\in n+1$ means that $k\in \{0, 1, ... ,n\}$ .

Is “1/0=1/0” true or false?

This question was asked some time ago on the math.stackexchange.com site. The answer depends on the foundation used, in ZF (as implemented in Isabelle/ZF and Metamath’s set.mm) the answer is “true” as we have the empty set on both sides of the equality (formally verified version of this assertion here). Some people have emotional reactions to this fact of life – I have seen comments like “it’s horrible”, “I’d like to know what text that is, so I can avoid it” etc. Still it’s interesting to know why expressions like $1/0$ cannot be just easily declared as “undefined” or “meaningless” in FOL once we leave the realm of aesthetics and philosophy and enter the realm of logic and facts. The answer by user21820 sheds some light on this question (note this is not accepted or highest rated answer).

Tags: formalized mathematics, Isabelle/ZF, IsarMathLib releases, weirdmath

This entry was posted on May 7, 2023 at 6:59 pm and is filed under announcements, IsarMathLib releases, mathematics. You can follow any responses to this entry through the RSS 2.0 feed. You can leave a response, or trackback from your own site.

Formalized Mathematics