BACK Mascot image.
← MA0 1 · Introduction to University Mathematics (Proofs)

Lesson 5

Natural Numbers

Taught

Natural Numbers

The Set of Natural Numbers

The starting point of our journey shall be the counting numbers, 1,2,31, 2, 3 and so on. We are all convinced that such a collection exists, and yet a little reflection leads quickly to thoughtfulness. Do not some cosmological theories hold that our universe is finite? If so, and if every elementary particle occupies a non-vanishing, indivisible volume, must not the number of particles be finite? Where then is room for this obviously infinite set? Or, much more primitively, how does one so much as name

10(10(1010))?10^{\left(10^{\left(10^{10}\right)}\right)} \quad ?

Following preliminary work by Dedekind, it was Peano who in 1889 codified our notion of the counting numbers as a successive progression from an origin. Rather than say what a number is, he left the first number and the successor rule undefined, and asked instead which conditions would force the resulting system to hold exactly the objects we want. We follow him, taking the distinguished first element to be 00.

The Axiom of Infinity

At the close of the last chapter we watched the passage from AA to A∪{A}A \cup \{A\} generate

∅,{∅},{∅,{∅}},{∅,{∅},{∅,{∅}}},…\emptyset, \quad \{\emptyset\}, \quad \bigl\{\emptyset, \{\emptyset\}\bigr\}, \quad \Bigl\{\emptyset, \{\emptyset\}, \bigl\{\emptyset, \{\emptyset\}\bigr\}\Bigr\}, \quad \ldots

and noted that our axioms build each of these but no set holding all of them at once. To close the gap we name the property such a set would have. Throughout we write s(x)=defx∪{x}s(x) \defeq x \cup \{x\} and call it the successor of xx.

Definition 5.1 (Inductive set).

A set II is inductive if ∅∈I\emptyset \in I and s(x)∈Is(x) \in I for every x∈Ix \in I.

Axiom 5.2 (Infinity).

An inductive set exists: ∃I (∅∈I∧∀x (x∈I  ⟹  x∪{x}∈I))\exists I\,\bigl(\emptyset \in I \land \forall x\,(x \in I \implies x \cup \{x\} \in I)\bigr).

The notation x∪{x}x \cup \{x\} is meaningful by the pairing and union axioms. Note that what it asserts is also new: every earlier axiom builds a set from sets already held, and none guarantees the existence of a set with infinitely many members. An inductive set may be far larger than the chain above, holding all manner of things besides; in our case we want the chain, so we take the smallest inductive set there is.

Definition 5.3 (The natural numbers).

Let II be an inductive set. We write N0\mathbb{N}_0 for the intersection of all inductive subsets of II,

N0=def⋂{J∈P(I)  ∣  J is inductive},\mathbb{N}_0 \defeq \bigcap \bigl\{J \in \mathcal{P}(I) \;\big|\; J \text{ is inductive}\bigr\},

and N=defN0∖{∅}\mathbb{N} \defeq \mathbb{N}_0 \setminus \{\emptyset\}. The elements of N\mathbb{N} are the natural numbers.

The collection being intersected is a set by comprehension applied to P(I)\mathcal{P}(I), and it is non-empty, since II is one of its members, so its intersection is defined. Writing 0=def∅0 \defeq \emptyset, 1=defs(0)1 \defeq s(0), 2=defs(1)2 \defeq s(1) and so on, we have

N0=N∪{0}={0,1,2,…},N={1,2,3,…}.\mathbb{N}_0 = \mathbb{N} \cup \{0\} = \{0, 1, 2, \ldots\}, \qquad \mathbb{N} = \{1, 2, 3, \ldots\}.

Remark (Where to start).

Whether 00 counts as a natural number is a matter of convention rather than of mathematics, and both choices are in use. We keep 11 as the first natural number, which is the older habit and the one that makes “natural number” mean “counting number”, and carry the zero explicitly when we need it. Peano’s system needs a distinguished element with no predecessor, so it is N0\mathbb{N}_0 rather than N\mathbb{N} that the axioms below describe.

Proposition 5.4 (Zero belongs to N0\mathbb{N}_0).

0∈N00 \in \mathbb{N}_0.

Discussion.

Membership in N0\mathbb{N}_0 is membership in every inductive subset of II, so we take an arbitrary such subset and check what being inductive says about it. The first clause of that definition puts ∅\emptyset in it, and since the subset was arbitrary the conclusion follows for the intersection.

Proof.

Let JJ be an arbitrary inductive subset of II. Then ∅∈J\emptyset \in J by the definition of an inductive set. Since JJ was arbitrary, ∅\emptyset belongs to every inductive subset of II, and so 0=∅∈N00 = \emptyset \in \mathbb{N}_0.

Proposition 5.5 (Closure under successors).

If n∈N0n \in \mathbb{N}_0, then s(n)∈N0s(n) \in \mathbb{N}_0.

Discussion.

The same argument, now for the successor. Assuming n∈N0n \in \mathbb{N}_0 and taking an arbitrary inductive subset JJ of II, the definition of the intersection puts nn in JJ, and the second clause of inductiveness carries it to s(n)∈Js(n) \in J. As JJ was arbitrary, s(n)s(n) lies in every inductive subset, which is membership in N0\mathbb{N}_0.

Proof.

Suppose n∈N0n \in \mathbb{N}_0 and let JJ be an arbitrary inductive subset of II. Then n∈Jn \in J, and so s(n)∈Js(n) \in J by the definition of an inductive set. Since JJ was arbitrary, s(n)s(n) belongs to every inductive subset of II, hence s(n)∈N0s(n) \in \mathbb{N}_0.

The two propositions together say that N0\mathbb{N}_0 is itself inductive, and by its very definition it lies inside every inductive subset of II. So N0\mathbb{N}_0 is the smallest inductive subset of II.

Theorem 5.6 (Induction for sets).

Let S⊂N0S \subset \mathbb{N}_0 with 0∈S0 \in S and s(n)∈Ss(n) \in S whenever n∈Sn \in S. Then S=N0S = \mathbb{N}_0.

Discussion.

We prove the equality by two inclusions, and one of them is the hypothesis. The two conditions on SS are word for word the definition of an inductive set, so SS is one of the subsets being intersected, and the intersection is contained in each of them; that gives N0⊂S\mathbb{N}_0 \subset S and finishes it.

Proof.

The two hypotheses say precisely that SS is inductive, and S⊂N0⊂IS \subset \mathbb{N}_0 \subset I, so SS is an inductive subset of II. The intersection defining N0\mathbb{N}_0 is contained in each set intersected, so N0⊂S\mathbb{N}_0 \subset S. With S⊂N0S \subset \mathbb{N}_0 from the hypothesis, mutual inclusion gives S=N0S = \mathbb{N}_0.

The theorem speaks about a subset, but an induction proof usually begins with a predicate. The two describe the same problem: membership in a fixed set is a predicate, and conversely a predicate PP determines the subset {n∈N0∣P(n)}\{n \in \mathbb{N}_0 \mid P(n)\}, so proving PP of every natural number is proving that this subset is everything.

Theorem 5.7 (Induction for predicates).

Let PP be a predicate on N0\mathbb{N}_0 with P(0)P(0) true and P(n)  ⟹  P(s(n))P(n) \implies P(s(n)) for every n∈N0n \in \mathbb{N}_0. Then P(n)P(n) holds for every n∈N0n \in \mathbb{N}_0.

Discussion.

We pass from the predicate to the set it cuts out and apply the previous theorem. Put S=def{n∈N0∣P(n)}S \defeq \{n \in \mathbb{N}_0 \mid P(n)\}, a set by comprehension. The first hypothesis is 0∈S0 \in S and the second is closure of SS under ss, which are the two conditions the previous theorem asks for, so S=N0S = \mathbb{N}_0; and that says PP holds everywhere.

Proof.

Let S=def{n∈N0∣P(n)}S \defeq \{n \in \mathbb{N}_0 \mid P(n)\}. By the first hypothesis 0∈S0 \in S. If n∈Sn \in S, then P(n)P(n) holds, so P(s(n))P(s(n)) holds by the second hypothesis and s(n)∈Ss(n) \in S. The previous theorem forces S=N0S = \mathbb{N}_0, which says that P(n)P(n) holds for every n∈N0n \in \mathbb{N}_0.

Problem 5.1.

Let II and JJ be inductive sets.

  1. Show that I∩JI \cap J is inductive.
  2. Would your argument work for three inductive sets? For a thousand? For a family {Iα}α∈A\{I_\alpha\}_{\alpha \in A} indexed by an arbitrary non-empty set?

The definition of N0\mathbb{N}_0 began by choosing an inductive set II, and nothing so far says the answer does not depend on that choice. It does not, because N0\mathbb{N}_0 is contained in every inductive set, not only in the inductive subsets of II.

Proposition 5.8 (The least inductive set).

N0\mathbb{N}_0 is inductive, and N0⊂K\mathbb{N}_0 \subset K for every inductive set KK.

Discussion.

That N0\mathbb{N}_0 is inductive is the two propositions above read together, one supplying ∅\emptyset and the other closure under ss. The second claim is harder, since an arbitrary inductive KK need not be a subset of II and so is not among the sets we intersected. The problem above gets around this: I∩KI \cap K is inductive, and it is a subset of II, so it is one of the sets intersected and therefore holds N0\mathbb{N}_0. Being inside I∩KI \cap K puts N0\mathbb{N}_0 inside KK.

Proof.

The propositions above give ∅∈N0\emptyset \in \mathbb{N}_0 and closure under ss, which is what it means for N0\mathbb{N}_0 to be inductive.

Now let KK be any inductive set. By the problem above I∩KI \cap K is inductive, and I∩K⊂II \cap K \subset I, so I∩KI \cap K is an inductive subset of II and hence one of the sets whose intersection defines N0\mathbb{N}_0. An intersection is contained in each set intersected, so N0⊂I∩K⊂K\mathbb{N}_0 \subset I \cap K \subset K.

Corollary 5.9 (The construction does not depend on the choice).

Let II and I′I' be inductive sets, and let N0\mathbb{N}_0 and N0′\mathbb{N}_0' be built from them as above. Then N0=N0′\mathbb{N}_0 = \mathbb{N}_0'.

Proof.

Both are inductive by the proposition, and both are contained in every inductive set, so N0⊂N0′\mathbb{N}_0 \subset \mathbb{N}_0' and N0′⊂N0\mathbb{N}_0' \subset \mathbb{N}_0. Mutual inclusion gives the equality.

One more fact about the successor: nothing lies strictly between xx and s(x)s(x).

Proposition 5.10 (The successor is the next set up).

For every set xx we have x⊂s(x)x \subset s(x), and there is no set zz with x⊊z⊊s(x)x \subsetneq z \subsetneq s(x).

Discussion.

The inclusion is immediate, since s(x)s(x) is a union with xx as one of its parts. For the second claim we take any zz with x⊂z⊂s(x)x \subset z \subset s(x) and show it must be one of the two ends, which is the same thing as saying nothing sits strictly between them. Either zz adds nothing to xx, in which case the two inclusions make z=xz = x; or it holds something outside xx, and that element must be xx itself, since the only element of s(x)s(x) outside xx is xx. Then x∈zx \in z, and with x⊂zx \subset z already in hand every element of s(x)s(x) lies in zz.

Proof.

Since s(x)=x∪{x}s(x) = x \cup \{x\}, every element of xx lies in s(x)s(x), so x⊂s(x)x \subset s(x).

Now let zz satisfy x⊂z⊂s(x)x \subset z \subset s(x). If z⊂xz \subset x, then with x⊂zx \subset z we get z=xz = x. Otherwise some y∈zy \in z has y∉xy \notin x; since y∈z⊂x∪{x}y \in z \subset x \cup \{x\}, this forces y=xy = x, so x∈zx \in z. Together with x⊂zx \subset z this puts every element of x∪{x}x \cup \{x\} in zz, that is, s(x)⊂zs(x) \subset z, and so z=s(x)z = s(x). Hence zz is xx or s(x)s(x), and no zz satisfies x⊊z⊊s(x)x \subsetneq z \subsetneq s(x).

Peano Systems

Definition 5.11 (Peano system).

A Peano system is a set XX together with a distinguished element 00 and a map ss, called the successor, satisfying

  1. 0∈X0 \in X;
  2. s(x)∈Xs(x) \in X whenever x∈Xx \in X;
  3. if s(x)=s(y)s(x) = s(y), then x=yx = y;
  4. s(x)≠0s(x) \neq 0 for every x∈Xx \in X;
  5. if Y⊂XY \subset X, 0∈Y0 \in Y, and s(y)∈Ys(y) \in Y whenever y∈Yy \in Y, then Y=XY = X.

We write it (X,0,s)(X, 0, s).

The first two conditions are what it means for ss to be a function from XX to XX with 00 a member of the domain; the third says ss is injective, and the fourth that 00 lies outside its range.

In any Peano system we write 1=defs(0)1 \defeq s(0), 2=defs(1)2 \defeq s(1), 3=defs(2)3 \defeq s(2), and so on, the symbols recording positions in the successor chain and nothing more.

The first two conditions let us start at 00 and keep taking successors, producing 00, s(0)s(0), s(s(0))s(s(0)), and so on. The last two prevent repetitions among what is produced: were two of them equal, repeated use of the third condition would strip successors from both sides until the fourth was contradicted. So XX holds infinitely many distinct elements. What we do not yet know is whether it holds anything else.

Example 5.12.

Reading the construction back gives the familiar symbols as sets:

0=∅,1=s(0)=∅∪{∅}={∅},2=s(1)={∅}∪{{∅}}={∅,{∅}},\begin{aligned} 0 &= \emptyset, \\ 1 &= s(0) = \emptyset \cup \{\emptyset\} = \{\emptyset\}, \\ 2 &= s(1) = \{\emptyset\} \cup \bigl\{\{\emptyset\}\bigr\} = \bigl\{\emptyset, \{\emptyset\}\bigr\}, \end{aligned}

and so on, each of these sets holding exactly its predecessors.

Example 5.13 (Informal).

The fifth condition cannot be dropped. Take XX to be the real numbers xx with x⩾0x \geqslant 0, with the usual 00 and s(x)=defx+1s(x) \defeq x + 1. The first four conditions all hold, yet 12\tfrac{1}{2} lies in XX and is reached by no finite string of successors from 00. It is the fifth that fails: the subset YY consisting of 00 and the counting numbers holds 00, and holds y+1y + 1 whenever it holds yy, yet Y≠XY \neq X.

The fifth condition is the principle of induction, and Peano made it one of the axioms for the numbers, rather than a proof technique applied to them from outside. Its predicate form follows in any Peano system as it did above, by passing from a predicate to the subset it defines.

Theorem 5.14 (The natural numbers form a Peano system).

(N0,0,s)(\mathbb{N}_0, 0, s) is a Peano system.

Discussion.

Four of the five conditions are already in hand. The first two are the two propositions above, and the fifth is induction for sets. What is left is the third and fourth, and neither follows from minimality alone: they are claims about the particular successor x∪{x}x \cup \{x\}, not about smallness. The fourth is quick, since s(x)s(x) always holds xx and so is never empty. The third asks that x∪{x}=y∪{y}x \cup \{x\} = y \cup \{y\} force x=yx = y, and the proof goes through the fact that every element of N0\mathbb{N}_0 is also a subset of it, which is itself proved by induction. Both are left to the problems below.

Proof.

The first condition is the proposition that 0∈N00 \in \mathbb{N}_0, the second is closure under successors, and the fifth is induction for sets. The third and fourth are the two problems below.

Problem 5.2.

Show that s(x)≠∅s(x) \neq \emptyset for every set xx, which is the fourth condition for (N0,0,s)(\mathbb{N}_0, 0, s).

Problem 5.3.

Call a set tt transitive if every element of tt is also a subset of tt.

  1. Prove by induction that every element of N0\mathbb{N}_0 is transitive.
  2. Deduce that if s(m)=s(n)s(m) = s(n) for m,n∈N0m, n \in \mathbb{N}_0, then m=nm = n, which is the third condition.

Problem 5.4.

Let A={0,1,2,3}A = \{0, 1, 2, 3\} with 00 distinguished, and define s(0)=def1s(0) \defeq 1, s(1)=def2s(1) \defeq 2, s(2)=def3s(2) \defeq 3 and s(3)=def0s(3) \defeq 0. Which of the five conditions does this system satisfy? For each one that fails, exhibit the failure.

The numerals are nothing but names for positions in the chain, so even the most obvious facts about them have to be proved from the five conditions.

Proposition 5.15 (Three is a natural number).

3∈X3 \in X.

Discussion.

We walk along the chain. The first condition puts 00 in XX, and the second carries membership from any element to its successor, so we apply it three times, at 00, at 11 and at 22.

Proof.

By the first condition 0∈X0 \in X. By the second, s(0)=1∈Xs(0) = 1 \in X. By the second again, s(1)=2∈Xs(1) = 2 \in X, and once more, s(2)=3∈Xs(2) = 3 \in X.

Proposition 5.16 (Four is not zero).

4≠04 \neq 0.

Discussion.

Do not laugh. Because of the way 44 has been defined, as the successor of the successor of the successor of the successor of 00, it is not true a priori that it differs from 00, however obvious that looks; a system in which the chain closes back on itself would have 4=04 = 0, and the problems below give one. What rules it out here is the fourth condition, which says no element of XX has 00 as its successor. To apply it we need 33 to be an element of XX, which is the previous proposition.

Proof.

By definition 4=s(3)4 = s(3), and 3∈X3 \in X by the previous proposition. The fourth condition gives s(3)≠0s(3) \neq 0, that is, 4≠04 \neq 0.

Proposition 5.17 (Six is not two).

6≠26 \neq 2.

Discussion.

Here the fourth condition does not apply directly, since neither number is 00. Instead we work backwards down the chain with the third condition, which strips a successor from both sides of an equation: assuming 6=26 = 2 gives s(5)=s(1)s(5) = s(1), hence 5=15 = 1, hence s(4)=s(0)s(4) = s(0), hence 4=04 = 0. That is what the previous proposition forbids, so the assumption cannot stand. This is the argument sketched after the definition: repeated use of the third condition reduces any equality to a contradiction with the fourth.

Proof.

Suppose, for contradiction, that 6=26 = 2. Then s(5)=s(1)s(5) = s(1), so the third condition gives 5=15 = 1. Then s(4)=s(0)s(4) = s(0), so the third condition gives 4=04 = 0, contradicting the previous proposition. Hence 6≠26 \neq 2.

Predecessors

Theorem 5.18 (Predecessors).

In a Peano system, s(X)=X∖{0}s(X) = X \setminus \{0\}. Consequently every element other than 00 is the successor of exactly one element.

Discussion.

We prove the equality by two inclusions. The fourth condition gives s(X)⊂X∖{0}s(X) \subset X \setminus \{0\} at once, since no successor is 00. For the reverse inclusion we cannot chase an element directly, since being non-zero says nothing about where an element came from; instead we put Y=def{0}∪s(X)Y \defeq \{0\} \cup s(X) and use induction. This YY holds 00 by construction and is closed under ss because every s(y)s(y) lies in s(X)s(X), so the fifth condition forces Y=XY = X, and every non-zero element is therefore a successor. The uniqueness of the predecessor is then the third condition.

Proof.

Let Y=def{0}∪s(X)Y \defeq \{0\} \cup s(X). Then 0∈Y0 \in Y, and if y∈Yy \in Y then s(y)∈s(X)⊂Ys(y) \in s(X) \subset Y, so Y=XY = X by the fifth condition. Thus every x≠0x \neq 0 lies in s(X)s(X), while 00 does not by the fourth, and so s(X)=X∖{0}s(X) = X \setminus \{0\}.

If s(m)=x=s(n)s(m) = x = s(n), then m=nm = n by the third condition, so the element producing xx is unique.

So ss can be inverted. Regarded as a map onto X∖{0}X \setminus \{0\}, the successor is surjective by the theorem and injective by the third condition, so it is a bijection, and invertibility supplies an inverse

s−1:X∖{0}→X,s^{-1} : X \setminus \{0\} \to X,

the predecessor map, satisfying s−1∘s=id⁡Xs^{-1} \circ s = \operatorname{id}_X and s∘s−1=id⁡X∖{0}s \circ s^{-1} = \operatorname{id}_{X \setminus \{0\}}. This shortens the axiom list: in place of the second, third and fourth conditions we may simply demand that s:X→X∖{0}s : X \to X \setminus \{0\} be a bijection.

Corollary 5.19 (No element is its own successor).

In a Peano system, s(x)≠xs(x) \neq x for every x∈Xx \in X.

Proof.

Let Y=def{x∈X∣s(x)≠x}Y \defeq \{x \in X \mid s(x) \neq x\}. By the fourth condition s(0)≠0s(0) \neq 0, so 0∈Y0 \in Y. Suppose x∈Yx \in Y. If s(s(x))=s(x)s(s(x)) = s(x), then s(x)=xs(x) = x by the third condition, contradicting x∈Yx \in Y; hence s(x)∈Ys(x) \in Y. By the fifth condition, Y=XY = X.

Induction Without Order

In the counting numbers we expect every non-empty subset to have a least element, but least is an order notion and a Peano system carries no order. The property can still be stated without an order: a non-empty subset should hold an element that is not the successor of any of its elements.

Theorem 5.20 (Induction without order).

Let XX be a set with an element 00 and let s:X→X∖{0}s : X \to X \setminus \{0\} be a bijection. Then the following are equivalent.

  1. The only subset of XX holding 00 and closed under ss is XX itself.
  2. Every non-empty subset M⊂XM \subset X holds an element mm with m∉s(M)m \notin s(M).

Discussion.

We prove both implications by contradiction, since each hypothesis is a statement about all subsets and gives us nothing to construct from. Suppose the first holds and the second fails. Then some non-empty MM satisfies M⊂s(M)M \subset s(M), and we pass to the complement Y=defX∖MY \defeq X \setminus M: the codomain of ss excludes 00, which puts 00 in YY, and injectivity shows YY is closed under ss, so the first condition makes Y=XY = X and MM empty. Conversely, suppose the second holds and some proper YY holds 00 and is closed under ss. The complement MM is non-empty, so it has a starting element mm, which is not 00 and is therefore s(n)s(n) for some nn by surjectivity. Whether nn lies in MM or in YY, we get a contradiction.

Proof.

Suppose the second statement fails for the non-empty set M⊂XM \subset X, so M⊂s(M)M \subset s(M), and put Y=defX∖MY \defeq X \setminus M. If 0∈M0 \in M, then 0∈s(M)⊂s(X)0 \in s(M) \subset s(X), which is impossible since the codomain of ss is X∖{0}X \setminus \{0\}; hence 0∈Y0 \in Y. Let y∈Yy \in Y and suppose s(y)∉Ys(y) \notin Y. Then s(y)∈M⊂s(M)s(y) \in M \subset s(M), so s(y)=s(m)s(y) = s(m) for some m∈Mm \in M, and injectivity gives y=m∈My = m \in M, contradicting y∈Yy \in Y. Thus YY holds 00 and is closed under ss, so Y=XY = X by the first statement and M=∅M = \emptyset, a contradiction.

Conversely, let Y⊂XY \subset X hold 00 and be closed under ss, and suppose Y≠XY \neq X. Then M=defX∖YM \defeq X \setminus Y is non-empty, and the second statement provides m∈Mm \in M with m∉s(M)m \notin s(M). Since 0∈Y0 \in Y we have m≠0m \neq 0, so surjectivity gives m=s(n)m = s(n) for some n∈Xn \in X. If n∈Mn \in M, then m∈s(M)m \in s(M), against the choice of mm; if n∈Yn \in Y, then m=s(n)∈Ym = s(n) \in Y by closure, against m∈Mm \in M. Neither is possible, so no such YY exists.

Problem 5.5 (Informal).

Note that

1=1,1−4=−(1+2),1−4+9=1+2+3,1−4+9−16=−(1+2+3+4).\begin{aligned} 1 &= 1, \\ 1 - 4 &= -(1 + 2), \\ 1 - 4 + 9 &= 1 + 2 + 3, \\ 1 - 4 + 9 - 16 &= -(1 + 2 + 3 + 4). \end{aligned}

Guess the general law suggested here and prove it by induction.

Problem 5.6 (Informal).

Note that 1+1/2=2−1/21 + 1/2 = 2 - 1/2, that 1+1/2+1/4=2−1/41 + 1/2 + 1/4 = 2 - 1/4, and that 1+1/2+1/4+1/8=2−1/81 + 1/2 + 1/4 + 1/8 = 2 - 1/8. Guess the general law suggested here and prove it by induction.

Problem 5.7 (Informal).

Note that 1−1/2=1/21 - 1/2 = 1/2, that (1−1/2)(1−1/3)=1/3(1 - 1/2)(1 - 1/3) = 1/3, and that (1−1/2)(1−1/3)(1−1/4)=1/4(1 - 1/2)(1 - 1/3)(1 - 1/4) = 1/4. Guess the general law suggested here and prove it by induction.

Problem 5.8.

For every n∈Nn \in \mathbb{N} with n⩾2n \geqslant 2, guess a general law which simplifies the product

(1−14)(1−19)(1−116)⋯(1−1n2),\left(1 - \frac{1}{4}\right)\left(1 - \frac{1}{9}\right)\left(1 - \frac{1}{16}\right) \cdots \left(1 - \frac{1}{n^2}\right),

and prove it by induction.

Recursion

In what sense are the natural numbers unique? The elements of two Peano systems may look completely different, but the conditions determine everything except the names. Any two are linked by a relabelling that respects the only structure present, the zero and the successor:

0⟼s(0)⟼s(s(0))⟼⋯↓↓↓0′⟼s′(0′)⟼s′(s′(0′))⟼⋯\begin{array}{ccccccc} 0 & \longmapsto & s(0) & \longmapsto & s(s(0)) & \longmapsto & \cdots \\ \big\downarrow & & \big\downarrow & & \big\downarrow & & \\ 0' & \longmapsto & s'(0') & \longmapsto & s'(s'(0')) & \longmapsto & \cdots \end{array}

Whatever the relabelling is, it must send 00 to 0′0', hence s(0)s(0) to s′(0′)s'(0'), and so on down the ladder. What the picture does not show is that the instruction “start at 0′0' and keep applying s′s'” defines a map on all of XX. Turning such an instruction into a function is called recursion, or inductive definition.

One piece of language first. Given maps α:A→B\alpha : A \to B, β:B→D\beta : B \to D, γ:A→C\gamma : A \to C and δ:C→D\delta : C \to D, we draw

A→  α  B↓γ↓βC→  δ  D\begin{array}{ccc} A & \xrightarrow{\ \ \alpha\ \ } & B \\ \big\downarrow{\scriptstyle \gamma} & & \big\downarrow{\scriptstyle \beta} \\ C & \xrightarrow{\ \ \delta\ \ } & D \end{array}

and call the square commutative if β∘α=δ∘γ\beta \circ \alpha = \delta \circ \gamma, that is, if the two routes from AA to DD agree. A larger diagram, like the ladder above, is commutative when every square inside it is.

Theorem 5.21 (Recursion theorem).

Let (X,0,s)(X, 0, s) be a Peano system, let AA be a set with an element a∈Aa \in A, and let g:A→Ag : A \to A. Then there is exactly one map α:X→A\alpha : X \to A with α(0)=a\alpha(0) = a and α∘s=g∘α\alpha \circ s = g \circ \alpha; that is, exactly one α\alpha sending 00 to aa and making the square

X→  s  X↓α↓αA→  g  A\begin{array}{ccc} X & \xrightarrow{\ \ s\ \ } & X \\ \big\downarrow{\scriptstyle \alpha} & & \big\downarrow{\scriptstyle \alpha} \\ A & \xrightarrow{\ \ g\ \ } & A \end{array}

commute.

Discussion.

Pointwise the commuting square says α(s(n))=g(α(n))\alpha(s(n)) = g(\alpha(n)), so the map is prescribed at 00 and prescribed one step at a time thereafter. We must prove both uniqueness and existence, and they need different tools. Uniqueness is induction: for two candidates, the set where they agree holds 00 and is closed under ss, so the fifth condition makes it all of XX. Existence cannot be induction, since there is no map yet to induct on; instead we build the map as a set of pairs. Call C⊂X×AC \subset X \times A admissible when it holds (0,a)(0, a) and sends each (n,c)∈C(n, c) \in C to (s(n),g(c))∈C(s(n), g(c)) \in C, and let Γ\Gamma be the intersection of all admissible subsets, which is admissible in its turn and sits inside every one of them. By the definition of a function it remains to show that each n∈Xn \in X occurs in exactly one pair of Γ\Gamma, and both halves of that are inductions. The second half uses a deletion argument: a pair not forced by the closure rule can be removed, leaving a smaller admissible set, which contradicts the minimality of Γ\Gamma; the fourth and third conditions justify the two deletions.

Proof.

For uniqueness, let α\alpha and β\beta both satisfy the two requirements and put Y=def{n∈X∣α(n)=β(n)}Y \defeq \{n \in X \mid \alpha(n) = \beta(n)\}. Since α(0)=a=β(0)\alpha(0) = a = \beta(0) we have 0∈Y0 \in Y, and if n∈Yn \in Y then α(s(n))=g(α(n))=g(β(n))=β(s(n))\alpha(s(n)) = g(\alpha(n)) = g(\beta(n)) = \beta(s(n)), so s(n)∈Ys(n) \in Y. By the fifth condition Y=XY = X, that is, α=β\alpha = \beta.

For existence, call C⊂X×AC \subset X \times A admissible if (0,a)∈C(0, a) \in C and (s(n),g(c))∈C(s(n), g(c)) \in C whenever (n,c)∈C(n, c) \in C. The whole of X×AX \times A is admissible, so the admissible sets form a non-empty collection, carved from P(X×A)\mathcal{P}(X \times A) by comprehension; let Γ\Gamma be its intersection, which is admissible in turn and lies inside every admissible set. We claim each n∈Xn \in X appears in exactly one pair of Γ\Gamma; by the definition of a function the claim makes Γ\Gamma a function α:X→A\alpha : X \to A, and admissibility then reads α(0)=a\alpha(0) = a and α(s(n))=g(α(n))\alpha(s(n)) = g(\alpha(n)).

That each nn appears in some pair is an induction on Y=def{n∈X∣(n,c)∈Γ for some c∈A}Y \defeq \{n \in X \mid (n, c) \in \Gamma \text{ for some } c \in A\}: admissibility puts (0,a)∈Γ(0, a) \in \Gamma, so 0∈Y0 \in Y, and if (n,c)∈Γ(n, c) \in \Gamma then (s(n),g(c))∈Γ(s(n), g(c)) \in \Gamma, so YY is closed under ss.

That no nn appears twice is an induction on Z=def{n∈X∣n appears in exactly one pair of Γ}Z \defeq \{n \in X \mid n \text{ appears in exactly one pair of } \Gamma\}. In both steps, a pair not forced by the closure rule may be deleted from Γ\Gamma, leaving a set which is still admissible yet strictly smaller than the smallest admissible set, a contradiction.

For the base step, suppose (0,c)∈Γ(0, c) \in \Gamma with c≠ac \neq a, and delete it. The set Γ∖{(0,c)}\Gamma \setminus \{(0, c)\} still holds (0,a)(0, a), and it is still closed, since every pair the rule produces has first coordinate s(n)s(n), which is never 00 by the fourth condition. Hence no such cc exists and 0∈Z0 \in Z.

For the inductive step, let nn appear only in the pair (n,c)(n, c), suppose (s(n),d)∈Γ(s(n), d) \in \Gamma with d≠g(c)d \neq g(c), and delete it. Again (0,a)(0, a) survives, by the fourth condition. For closure, take a surviving pair (p,e)(p, e); the rule demands (s(p),g(e))(s(p), g(e)), and this survived too: if s(p)≠s(n)s(p) \neq s(n) it is not the deleted pair, while if s(p)=s(n)s(p) = s(n) then p=np = n by the third condition, so e=ce = c by the choice of nn and g(e)=g(c)≠dg(e) = g(c) \neq d. The same contradiction forbids dd, so s(n)s(n) appears only in (s(n),g(c))(s(n), g(c)) and s(n)∈Zs(n) \in Z. By the fifth condition, Z=XZ = X.

Theorem 5.22 (Uniqueness of Peano systems).

Let (X,0,s)(X, 0, s) and (X′,0′,s′)(X', 0', s') be Peano systems. Then there is exactly one bijection α:X→X′\alpha : X \to X' with α(0)=0′\alpha(0) = 0' making the square

X→  s  X↓α↓αX′→  s′  X′\begin{array}{ccc} X & \xrightarrow{\ \ s\ \ } & X \\ \big\downarrow{\scriptstyle \alpha} & & \big\downarrow{\scriptstyle \alpha} \\ X' & \xrightarrow{\ \ s'\ \ } & X' \end{array}

commute.

Discussion.

Apply the recursion theorem with A=X′A = X', a=0′a = 0' and g=s′g = s'. It gives a unique map α\alpha with α(0)=0′\alpha(0) = 0' and α∘s=s′∘α\alpha \circ s = s' \circ \alpha, and any bijection meeting the requirements must be that map, so only bijectivity is left to prove. We get it by producing an inverse rather than by checking injectivity and surjectivity separately. Applying the theorem again with the two systems exchanged gives α′:X′→X\alpha' : X' \to X, and the composite α′∘α\alpha' \circ \alpha sends 00 to 00 and commutes with ss, so it solves the same recursion problem on XX as the identity does; uniqueness identifies the two. The same argument on the other side finishes it.

Proof.

Applying the recursion theorem with A=X′A = X', a=0′a = 0' and g=s′g = s' gives exactly one map α:X→X′\alpha : X \to X' with α(0)=0′\alpha(0) = 0' and α∘s=s′∘α\alpha \circ s = s' \circ \alpha; it remains to prove α\alpha bijective. Exchanging the systems gives likewise a unique α′:X′→X\alpha' : X' \to X with α′(0′)=0\alpha'(0') = 0 and α′∘s′=s∘α′\alpha' \circ s' = s \circ \alpha'.

Put ι=defα′∘α:X→X\iota \defeq \alpha' \circ \alpha : X \to X. Then ι(0)=α′(0′)=0\iota(0) = \alpha'(0') = 0, and associativity of composition lets us compute without brackets:

ι∘s=α′∘α∘s=α′∘s′∘α=s∘α′∘α=s∘ι.\iota \circ s = \alpha' \circ \alpha \circ s = \alpha' \circ s' \circ \alpha = s \circ \alpha' \circ \alpha = s \circ \iota.

So ι\iota solves the recursion problem on XX with a=0a = 0 and g=sg = s; so does id⁡X\operatorname{id}_X; and by the uniqueness clause ι=id⁡X\iota = \operatorname{id}_X. The same argument with the systems exchanged gives α∘α′=id⁡X′\alpha \circ \alpha' = \operatorname{id}_{X'}. Hence α′\alpha' is an inverse of α\alpha, and α\alpha is bijective by invertibility.

The condition α(0)=0′\alpha(0) = 0' is in fact automatic: any bijection β:X→X′\beta : X \to X' with β∘s=s′∘β\beta \circ s = s' \circ \beta already sends 00 to 0′0'. Otherwise surjectivity would provide some n≠0n \neq 0 with β(n)=0′\beta(n) = 0', the theorem on predecessors would write n=s(m)n = s(m), and then 0′=β(s(m))=s′(β(m))0' = \beta(s(m)) = s'(\beta(m)) would exhibit 0′0' as a successor in X′X', against the fourth condition.

So there is, up to relabelling, only one system of natural numbers. Whether we take the Hindu-Arabic symbols 0,1,2,3,…0, 1, 2, 3, \ldots, the Roman ones augmented with a zero, or the nested empty sets of the example above, the arithmetic that follows is the same.

Arithmetic

The recursion theorem lets us define arithmetic inside any Peano system, with no arithmetic assumed from outside.

Any addition should satisfy m+1=s(m)m + 1 = s(m), should be associative, and should have 00 as an identity. These requirements determine it, since the first two give

m+s(n)=m+(n+1)=(m+n)+1=s(m+n),m + s(n) = m + (n + 1) = (m + n) + 1 = s(m + n),

which determines m+nm + n for every nn once m+0=mm + 0 = m is fixed. That some operation satisfies them is a separate question, settled by the recursion theorem.

Definition 5.23 (Addition).

Let (X,0,s)(X, 0, s) be a Peano system and let m∈Xm \in X. The recursion theorem applied with A=XA = X, a=ma = m and g=sg = s yields exactly one map σm:X→X\sigma_m : X \to X with σm(0)=m\sigma_m(0) = m and σm∘s=s∘σm\sigma_m \circ s = s \circ \sigma_m. We write m+n=defσm(n)m + n \defeq \sigma_m(n), so that

m+0=mandm+s(n)=s(m+n).m + 0 = m \qquad\text{and}\qquad m + s(n) = s(m + n).

In particular m+1=m+s(0)=s(m+0)=s(m)m + 1 = m + s(0) = s(m + 0) = s(m). The defining clauses deal with a 00 or an ss on the right of a sum; for the laws of addition we also need them on the left.

Proposition 5.24 (Addition from the left).

For all m,n∈Xm, n \in X, we have 0+n=n0 + n = n and s(m)+n=s(m+n)s(m) + n = s(m + n).

Discussion.

We induct on the right-hand variable nn in both, since that is the position the defining clauses are about. For the first, the base case is the clause m+0=mm + 0 = m read at m=0m = 0, and the step uses the other clause: 0+s(n)=s(0+n)=s(n)0 + s(n) = s(0 + n) = s(n). For the second, fix mm and take the statement s(m)+n=s(m+n)s(m) + n = s(m + n). Its base case reduces both sides by the first clause. For the step, apply the successor clause on the left, replace s(m)+ns(m) + n by s(m+n)s(m + n) using the hypothesis, and apply the clause once more. As mm was arbitrary throughout, the result holds for all mm and nn.

Proof.

Let Y=def{n∈X∣0+n=n}Y \defeq \{n \in X \mid 0 + n = n\}. Since 0+0=00 + 0 = 0 we have 0∈Y0 \in Y, and if n∈Yn \in Y then 0+s(n)=s(0+n)=s(n)0 + s(n) = s(0 + n) = s(n), so s(n)∈Ys(n) \in Y. By the fifth condition Y=XY = X.

Now fix m∈Xm \in X and let Z=def{n∈X∣s(m)+n=s(m+n)}Z \defeq \{n \in X \mid s(m) + n = s(m + n)\}. Since s(m)+0=s(m)=s(m+0)s(m) + 0 = s(m) = s(m + 0) we have 0∈Z0 \in Z. If n∈Zn \in Z, then

s(m)+s(n)=s(s(m)+n)=s(s(m+n))=s(m+s(n)),s(m) + s(n) = s\bigl(s(m) + n\bigr) = s\bigl(s(m + n)\bigr) = s\bigl(m + s(n)\bigr),

so s(n)∈Zs(n) \in Z. By the fifth condition Z=XZ = X, and since mm was arbitrary the identity holds throughout.

Theorem 5.25 (Laws of addition).

For all m,n,p∈Xm, n, p \in X, we have (m+n)+p=m+(n+p)(m + n) + p = m + (n + p) and m+n=n+mm + n = n + m.

Discussion.

Both are inductions on the variable sitting in the right-hand position of a sum, where the definition applies. For associativity, fix mm and nn and take the statement (m+n)+p=m+(n+p)(m + n) + p = m + (n + p); its base case reduces both sides by r+0=rr + 0 = r, and its step rewrites the left as s((m+n)+p)s((m+n)+p), applies the hypothesis, and uses the successor clause twice to arrive at m+(n+s(p))m + (n + s(p)). For commutativity, fix mm and take m+n=n+mm + n = n + m; the base case is m+0=m=0+mm + 0 = m = 0 + m, which needs the first identity of the preceding proposition, and the step turns m+s(n)m + s(n) into s(m+n)s(m + n), applies the hypothesis, and then uses the second identity to reach s(n)+ms(n) + m. Neither induction would close without that proposition, since both steps have to move a successor across to the left of a sum.

Proof.

Fix m,n∈Xm, n \in X and let Y=def{p∈X∣(m+n)+p=m+(n+p)}Y \defeq \{p \in X \mid (m + n) + p = m + (n + p)\}. Both (m+n)+0(m + n) + 0 and m+(n+0)m + (n + 0) equal m+nm + n, so 0∈Y0 \in Y. If p∈Yp \in Y, then

(m+n)+s(p)=s((m+n)+p)=s(m+(n+p))=m+s(n+p)=m+(n+s(p)),(m + n) + s(p) = s\bigl((m + n) + p\bigr) = s\bigl(m + (n + p)\bigr) = m + s(n + p) = m + \bigl(n + s(p)\bigr),

so s(p)∈Ys(p) \in Y, and Y=XY = X by the fifth condition.

Next fix m∈Xm \in X and let Z=def{n∈X∣m+n=n+m}Z \defeq \{n \in X \mid m + n = n + m\}. The preceding proposition gives 0+m=m=m+00 + m = m = m + 0, so 0∈Z0 \in Z. If n∈Zn \in Z, then

m+s(n)=s(m+n)=s(n+m)=s(n)+m,m + s(n) = s(m + n) = s(n + m) = s(n) + m,

using that proposition again at the last step, so s(n)∈Zs(n) \in Z. By the fifth condition Z=XZ = X, and since mm was arbitrary the identity holds throughout.

Definition 5.26 (Positive elements).

An element nn of a Peano system is positive if n≠0n \neq 0.

Proposition 5.27 (Positivity is absorbing).

If aa is positive and b∈Xb \in X, then a+ba + b is positive.

Discussion.

We induct on bb, since the defining clauses of addition are about the right-hand variable. The base case is a+0=aa + 0 = a, which is positive by hypothesis. For the step, the successor clause turns a+s(b)a + s(b) into s(a+b)s(a + b), and the fourth condition says no successor is 00, so the conclusion needs nothing from the inductive hypothesis at all.

Proof.

Let Y=def{b∈X∣a+b is positive}Y \defeq \{b \in X \mid a + b \text{ is positive}\}. Since a+0=aa + 0 = a and aa is positive, 0∈Y0 \in Y. If b∈Yb \in Y, then a+s(b)=s(a+b)a + s(b) = s(a + b), which is not 00 by the fourth condition, so s(b)∈Ys(b) \in Y. By the fifth condition Y=XY = X.

Corollary 5.28 (A sum is zero only when both parts are).

If a,b∈Xa, b \in X satisfy a+b=0a + b = 0, then a=0a = 0 and b=0b = 0.

Proof.

Suppose a≠0a \neq 0. Then aa is positive, so a+ba + b is positive by the proposition, contradicting a+b=0a + b = 0. Hence a=0a = 0, and by commutativity the same argument gives b=0b = 0.

Problem 5.9.

Define multiplication in a Peano system by the clauses m⋅0=def0m \cdot 0 \defeq 0 and m⋅s(n)=defm⋅n+mm \cdot s(n) \defeq m \cdot n + m. Show that these clauses do define a map from X×XX \times X to XX.

Problem 5.10.

Using the previous problem, prove that for all m,n,p∈Xm, n, p \in X:

  1. m⋅(n+p)=m⋅n+m⋅pm \cdot (n + p) = m \cdot n + m \cdot p;
  2. m⋅n=n⋅mm \cdot n = n \cdot m;
  3. 1⋅m=m⋅1=m1 \cdot m = m \cdot 1 = m;
  4. 0⋅m=m⋅0=00 \cdot m = m \cdot 0 = 0;
  5. (m⋅n)⋅p=m⋅(n⋅p)(m \cdot n) \cdot p = m \cdot (n \cdot p).

Proposition 5.29 (Positive elements are closed under addition and multiplication).

Let aa and bb be positive elements of a Peano system, with multiplication as in the two problems above. Then a+ba + b and a⋅ba \cdot b are positive.

Discussion.

The sum is Proposition 5.27 read at a positive bb, which puts no condition on bb. The product needs one more step. Being positive, bb is not 00, so the theorem on predecessors writes it as s(c)s(c) for a unique cc, and the second clause of the multiplication problem turns a⋅s(c)a \cdot s(c) into a⋅c+aa \cdot c + a. That is a sum whose left part we know nothing about and whose right part is positive, which is the case Proposition 5.27 covers, once commutativity puts the positive part in front. No induction is needed, since writing bb as a successor lets us apply the second clause once.

Proof.

That a+ba + b is positive is Proposition 5.27 , since aa is positive.

For the product, b≠0b \neq 0, so the theorem on predecessors gives b=s(c)b = s(c) for some c∈Xc \in X. Then a⋅b=a⋅s(c)=a⋅c+aa \cdot b = a \cdot s(c) = a \cdot c + a by the second clause of the multiplication problem, and a⋅c+a=a+a⋅ca \cdot c + a = a + a \cdot c by commutativity of addition. Since aa is positive, Proposition 5.27 makes a+a⋅ca + a \cdot c positive, so a⋅ba \cdot b is positive.

Problem 5.11.

Write N\mathbb{N} for the positive elements of a Peano system, and recall 1=s(0)1 = s(0). Show that every n∈Nn \in \mathbb{N} with n≠1n \neq 1 is s(m)s(m) for some m∈Nm \in \mathbb{N}. Why does the argument need n≠1n \neq 1, and not merely n≠0n \neq 0?

Problem 5.12.

Let a∈Xa \in X. Use the recursion theorem, with a starting element and a map g:X→Xg : X \to X of your choosing, to produce a unique map exp⁡a:X→X\exp_a : X \to X satisfying

exp⁡a(0)=1andexp⁡a(s(n))=exp⁡a(n)⋅a,\exp_a(0) = 1 \qquad\text{and}\qquad \exp_a(s(n)) = \exp_a(n) \cdot a,

written ana^n for exp⁡a(n)\exp_a(n). Prove directly from the clauses that as(0)=aa^{s(0)} = a, and, writing 2=defs(1)2 \defeq s(1), compute 1+11 + 1, 2⋅22 \cdot 2 and 222^2 from the definitions alone.

Problem 5.13.

Let α:X→X\alpha : X \to X satisfy α∘s=s∘α\alpha \circ s = s \circ \alpha. Prove that α(n)=α(0)+n\alpha(n) = \alpha(0) + n for every n∈Xn \in X. No commutativity is needed.

Problem 5.14.

Let x,y,z∈Xx, y, z \in X.

  1. Prove that if x≠yx \neq y, then x+z≠y+zx + z \neq y + z.
  2. Deduce that x+z=y+zx + z = y + z implies x=yx = y.
  3. Show that if n=m+bn = m + b with bb positive, then n≠mn \neq m.

Problem 5.15.

Prove that (am)n=am⋅n(a^m)^n = a^{m \cdot n} for all a,m,n∈Xa, m, n \in X, and that the map sending nn to ana^n is the unique one with φ(0)=1\varphi(0) = 1, φ(1)=a\varphi(1) = a and φ(m+n)=φ(m)⋅φ(n)\varphi(m + n) = \varphi(m) \cdot \varphi(n) for all m,n∈Xm, n \in X.

Sums

Some recursive definitions do not fit the recursion theorem as it stands.

Imagine defining the running totals σn\sigma_n, the sum of everything up to nn. Once σn\sigma_n is found, the next total should be σs(n)=σn+s(n)\sigma_{s(n)} = \sigma_n + s(n): the old total is kept and the next term added. That update needs both the previous value and the index, whereas the recursion theorem applies a fixed map to the previous value alone and never sees where it is. The fix is to carry the index along.

Proposition 5.30 (Parametrised recursion).

Let (X,0,s)(X, 0, s) be a Peano system, let AA be a set with an element a∈Aa \in A, and let G:X×A→AG : X \times A \to A. Then there is exactly one map α:X→A\alpha : X \to A with

α(0)=aandα(s(n))=G(n,α(n))for every n∈X.\alpha(0) = a \qquad\text{and}\qquad \alpha(s(n)) = G\bigl(n, \alpha(n)\bigr) \quad\text{for every } n \in X.

Discussion.

In the recursion theorem the next value is computed from the previous value alone, while GG also needs the index. So we make the previous value carry its own index: apply the theorem on X×AX \times A rather than on AA, starting at (0,a)(0, a) and stepping by (n,c)↦(s(n),G(n,c))(n, c) \mapsto \bigl(s(n), G(n, c)\bigr). That gives a map β:X→X×A\beta : X \to X \times A, and an induction shows its first coordinate at nn is always nn itself, so the second coordinate is the α\alpha we want. Uniqueness goes the same way in reverse: any rival α′\alpha' can be paired with its index to give a rival β′\beta', which solves the same recursion problem on X×AX \times A and is therefore β\beta by the uniqueness already proved.

Proof.

Apply the recursion theorem with target set X×AX \times A, initial element (0,a)(0, a), and the map sending (n,c)(n, c) to (s(n),G(n,c))\bigl(s(n), G(n, c)\bigr). It gives a unique β:X→X×A\beta : X \to X \times A with β(0)=(0,a)\beta(0) = (0, a) and β(s(n))=(s(n),G(n,c))\beta(s(n)) = \bigl(s(n), G(n, c)\bigr) whenever β(n)=(n,c)\beta(n) = (n, c).

Let YY be the set of n∈Xn \in X for which β(n)=(n,c)\beta(n) = (n, c) for some c∈Ac \in A. Since β(0)=(0,a)\beta(0) = (0, a) we have 0∈Y0 \in Y; and if n∈Yn \in Y with β(n)=(n,c)\beta(n) = (n, c), the displayed equation gives β(s(n))=(s(n),G(n,c))\beta(s(n)) = \bigl(s(n), G(n, c)\bigr), so s(n)∈Ys(n) \in Y. By the fifth condition Y=XY = X.

For each n∈Xn \in X write β(n)=(n,α(n))\beta(n) = \bigl(n, \alpha(n)\bigr). Then α(0)=a\alpha(0) = a, and the defining equation for β\beta reads α(s(n))=G(n,α(n))\alpha(s(n)) = G\bigl(n, \alpha(n)\bigr).

If α′\alpha' is another map with these two properties, let β′(n)=def(n,α′(n))\beta'(n) \defeq \bigl(n, \alpha'(n)\bigr). Then β′(0)=(0,a)\beta'(0) = (0, a) and β′(s(n))=(s(n),G(n,α′(n)))\beta'(s(n)) = \bigl(s(n), G(n, \alpha'(n))\bigr), so β′\beta' solves the same recursion problem as β\beta; the uniqueness clause of the recursion theorem gives β′=β\beta' = \beta, and comparing second coordinates gives α′=α\alpha' = \alpha.

Before using sums we should say what the dots are doing. In

a1+a2+⋯+ana_1 + a_2 + \cdots + a_n

they leave the middle terms to the pattern made visible by the terms around them. This is a convention for readers, not a definition: a1+a7+⋯+a41a_1 + a_7 + \cdots + a_{41} determines nothing without further context. We replace the convention by a recursion, so that the expression has a meaning whether or not the pattern is visible.

Proposition 5.31 (The summation symbol).

Let (X,0,s)(X, 0, s) be a Peano system with addition, and let a:X→Xa : X \to X be a map, written aia_i for a(i)a(i). Then there is exactly one map Σ:X→X\Sigma : X \to X with

Σ(0)=0andΣ(s(n))=Σ(n)+as(n)for every n∈X.\Sigma(0) = 0 \qquad\text{and}\qquad \Sigma(s(n)) = \Sigma(n) + a_{s(n)} \quad\text{for every } n \in X.

We write ∑i=1nai\displaystyle\sum_{i=1}^{n} a_i for Σ(n)\Sigma(n), so that the two clauses read

∑i=10ai=0and∑i=1s(n)ai=(∑i=1nai)+as(n).\sum_{i=1}^{0} a_i = 0 \qquad\text{and}\qquad \sum_{i=1}^{s(n)} a_i = \left(\sum_{i=1}^{n} a_i\right) + a_{s(n)}.

Discussion.

The update needs the index as well as the running total, since it is the index that says which term comes next, so this is parametrised recursion rather than the plain kind. We take A=XA = X, initial element 00, and G(n,c)=defc+as(n)G(n, c) \defeq c + a_{s(n)}, which is a map from X×XX \times X to XX because addition is. The two clauses of the proposition are then exactly the two the previous result delivers, and its uniqueness clause gives ours.

Proof.

Apply parametrised recursion with A=XA = X, initial element 00, and G:X×X→XG : X \times X \to X given by G(n,c)=defc+as(n)G(n, c) \defeq c + a_{s(n)}. It supplies exactly one map Σ:X→X\Sigma : X \to X with Σ(0)=0\Sigma(0) = 0 and Σ(s(n))=G(n,Σ(n))=Σ(n)+as(n)\Sigma(s(n)) = G\bigl(n, \Sigma(n)\bigr) = \Sigma(n) + a_{s(n)}, which are the two clauses asserted.

The limits carry no order with them: nothing here says that ii runs through the elements between 11 and nn, only that the recursion starts at 00 and steps by ss. Once an order is available the notation will mean what it looks like it means.

The index is bound by the symbol and may be renamed at will, so that

∑i=1nai=∑j=1naj,\sum_{i=1}^{n} a_i = \sum_{j=1}^{n} a_j,

while nn may not be renamed, since the value depends on it. The value ∑i=10ai=0\sum_{i=1}^{0} a_i = 0 is the empty sum, worth keeping both because it starts the recursion and because it spares us a separate case whenever a sum is allowed to run out of terms. Notice too that the clauses fix one reading of a1+⋯+ana_1 + \cdots + a_n, the one that brackets from the left; that any other bracketing gives the same element is a consequence of the laws of addition, and we leave it to a problem.

Problem 5.16.

Show that there is exactly one map Π:X→X\Pi : X \to X with Π(0)=1\Pi(0) = 1 and Π(s(n))=Π(n)⋅as(n)\Pi(s(n)) = \Pi(n) \cdot a_{s(n)} for every n∈Xn \in X, where multiplication is as defined in the problems above, and write ∏i=1nai\displaystyle\prod_{i=1}^{n} a_i for Π(n)\Pi(n). Which clause takes the place of the empty sum, and why is that the right choice?

Problem 5.17.

Argue from the defining clauses alone.

  1. Let ai=def1a_i \defeq 1 for every ii. Prove that ∑i=1nai=n\displaystyle\sum_{i=1}^{n} a_i = n and ∏i=1nai=1\displaystyle\prod_{i=1}^{n} a_i = 1 for every n∈Xn \in X.
  2. Let ai=defia_i \defeq i for every ii, so that the sum is the running total of everything up to nn. Prove that
∑i=1ni  +  ∑i=1ni  =  n⋅s(n).\sum_{i=1}^{n} i \;+\; \sum_{i=1}^{n} i \;=\; n \cdot s(n).

Problem 5.18.

Prove that

∑i=1m+nai=∑i=1mai  +  ∑i=1nam+i,\sum_{i=1}^{m+n} a_i = \sum_{i=1}^{m} a_i \;+\; \sum_{i=1}^{n} a_{m+i},

stating carefully what the second sum on the right means as a recursion in its own right. Where do the laws of addition enter?

Problem 5.19.

Let (X,0,s)(X, 0, s) and (X′,0′,s′)(X', 0', s') be Peano systems, each carrying the addition of Definition 5.23 and the multiplication of Problem 5.9 , and let α:X→X′\alpha : X \to X' be the bijection of Theorem 5.22 . Prove that α(m+n)=α(m)+α(n)\alpha(m + n) = \alpha(m) + \alpha(n) and α(m⋅n)=α(m)⋅α(n)\alpha(m \cdot n) = \alpha(m) \cdot \alpha(n) for all m,n∈Xm, n \in X.

Problem 5.20.

Let (X,0,s)(X, 0, s) be a Peano system with multiplication.

  1. Produce a map F:X→XF : X \to X with F(0)=1F(0) = 1 and F(s(n))=s(n)⋅F(n)F(s(n)) = s(n) \cdot F(n) for every n∈Xn \in X.
  2. Show that there is no g:X→Xg : X \to X with F(s(n))=g(F(n))F(s(n)) = g\bigl(F(n)\bigr) for every n∈Xn \in X, and deduce that Theorem 5.21 taken with A=XA = X cannot produce FF.

Problem 5.21.

Let SS be a non-empty set and let H:S→SH : S \to S. Taking for AA the set SSS^S of all maps from SS to itself, use Theorem 5.21 to produce the iterates HnH^n of HH, characterised by H0=id⁡SH^0 = \operatorname{id}_S and Hs(n)=H∘HnH^{s(n)} = H \circ H^n for every n∈N0n \in \mathbb{N}_0.

  1. Suppose H(H(y))=yH\bigl(H(y)\bigr) = y for some y∈Sy \in S. Determine H80(y)H^{80}(y) and H81(y)H^{81}(y), with proof.
  2. Suppose instead that H(H(y))=H(y)H\bigl(H(y)\bigr) = H(y). Determine H80(y)H^{80}(y), with proof.
  3. Find a map H:N0→N0H : \mathbb{N}_0 \to \mathbb{N}_0 with H∘H=HH \circ H = H, H(1)=36H(1) = 36, H(2)=5H(2) = 5 and H(13)=47H(13) = 47.
  4. Decide whether there is a map H:N0→N0H : \mathbb{N}_0 \to \mathbb{N}_0 with H∘H=HH \circ H = H, H(1)=7H(1) = 7 and H(7)=18H(7) = 18.

Problem 5.22.

Let a,b:X→Xa, b : X \to X be maps, written aia_i for a(i)a(i) and bib_i for b(i)b(i), and let c∈Xc \in X. Prove that for every n∈Xn \in X:

  1. ∑i=1n(ai+bi)=∑i=1nai+∑i=1nbi\displaystyle\sum_{i=1}^{n} (a_i + b_i) = \sum_{i=1}^{n} a_i + \sum_{i=1}^{n} b_i;
  2. ∑i=1nc⋅ai=c⋅∑i=1nai\displaystyle\sum_{i=1}^{n} c \cdot a_i = c \cdot \sum_{i=1}^{n} a_i;
  3. if as(i)=ai+bs(i)a_{s(i)} = a_i + b_{s(i)} for every i∈Xi \in X, then a0+∑i=1nbi=an\displaystyle a_0 + \sum_{i=1}^{n} b_i = a_n.

Problem 5.23.

Let A(n)A(n) denote the statement 8⋅∑i=1ni=(2n+1)28 \cdot \displaystyle\sum_{i=1}^{n} i = (2n + 1)^2.

  1. Prove that if A(k)A(k) holds for some k∈Nk \in \mathbb{N}, then A(s(k))A(s(k)) holds.
  2. Criticise the statement: “by induction it follows that A(n)A(n) holds for every n∈Nn \in \mathbb{N}”.
  3. Determine which n∈Nn \in \mathbb{N}, if any, satisfy A(n)A(n).

Problem 5.24.

Work in a Peano system with addition, multiplication and the powers of Problem 5.12 .

  1. Prove that 4⋅∑i=1ni3=n2⋅s(n)24 \cdot \displaystyle\sum_{i=1}^{n} i^3 = n^2 \cdot s(n)^2 for every n∈Nn \in \mathbb{N}.
  2. Deduce that ∑i=1ni3=(∑i=1ni)2\displaystyle\sum_{i=1}^{n} i^3 = \left(\sum_{i=1}^{n} i\right)^2.

Problem 5.25.

The Fibonacci numbers are 1,1,2,3,5,8,13,21,34,55,…1, 1, 2, 3, 5, 8, 13, 21, 34, 55, \ldots, each after the second being the sum of the two before it.

  1. Produce exactly one map a:X→Xa : X \to X with a0=as(0)=1a_0 = a_{s(0)} = 1 and as(s(n))=as(n)+ana_{s(s(n))} = a_{s(n)} + a_n for every n∈Xn \in X, writing ana_n for a(n)a(n).
  2. Prove that for every n∈Xn \in X exactly one of
an⋅as(s(n))=s(as(n)⋅as(n))andas(n)⋅as(n)=s(an⋅as(s(n)))a_n \cdot a_{s(s(n))} = s\bigl(a_{s(n)} \cdot a_{s(n)}\bigr) \qquad\text{and}\qquad a_{s(n)} \cdot a_{s(n)} = s\bigl(a_n \cdot a_{s(s(n))}\bigr)

holds, and that which of the two holds changes at every step.

Exercises

 

Answers are checked in your browser, as often as you like. Nothing is sent anywhere and nothing is kept but your own work. A formula may be written with the symbols themselves or with ~ & | -> <-> ^, and \and, \or, \to expand as you type.

Exercise 5.1.

The numerals, read back as the sets they were built from.

The set 33 is:

answer one of these

The number of elements of the set 44 is:

answer one of these

Of the two statements 2∈32 \in 3 and 2⊂32 \subset 3:

answer one of these

Exercise 5.2.

Inductive sets.

The set N\mathbb{N} of natural numbers proper is:

answer one of these

And P(N0)\mathcal{P}(\mathbb{N}_0) is:

answer one of these

Let KK be any inductive set. Then N0∩K\mathbb{N}_0 \cap K is:

answer one of these

Exercise 5.3.

Each line below alters (N0,0,s)(\mathbb{N}_0, 0, s) in one place. Say which of the five conditions the result fails.

The successor is replaced by s∘ss \circ s.

answer one of these

The carrier is cut down to N\mathbb{N}, keeping ss, with 11 distinguished in place of 00.

answer one of these

The successor is left alone except at 00, where s(0)=def0s(0) \defeq 0.

answer one of these

Exercise 5.4.

Starting elements. Work in an arbitrary Peano system (X,0,s)(X, 0, s).

The elements that are not successors are:

answer one of these

Induction without order gives every non-empty M⊂XM \subset X an element mm with m∉s(M)m \notin s(M). For M=X∖{0}M = X \setminus \{0\} that element is:

answer one of these

And for M=XM = X:

answer one of these

Exercise 5.5.

What the recursion theorem produces. Take A=XA = X throughout, with the addition and multiplication of the chapter.

With a=0a = 0 and g=defs∘sg \defeq s \circ s, the map α\alpha is:

answer one of these

With a=1a = 1 and g(c)=defc+cg(c) \defeq c + c, it is:

answer one of these

Exercise 5.6.

Relabelling. Let (X,0,s)(X, 0, s) and (X′,0′,s′)(X', 0', s') be Peano systems.

Let α:X→X′\alpha : X \to X' satisfy α(0)=0′\alpha(0) = 0' and α∘s=s′∘α\alpha \circ s = s' \circ \alpha. Then α(3)\alpha(3) is:

answer one of these

Drop the condition at 00. The number of maps β:X→X′\beta : X \to X' with β∘s=s′∘β\beta \circ s = s' \circ \beta is then:

answer one of these

And the number of those that are bijections is:

answer one of these

Exercise 5.7.

Arithmetic in a Peano system.

The product s(m)⋅s(n)s(m) \cdot s(n) is:

answer one of these

Suppose a⋅b=0a \cdot b = 0 with aa positive. Then:

answer one of these

Exercise 5.8.

Sums.

The result that defines ∑i=1nai\sum_{i=1}^{n} a_i is:

answer one of these

With ai=defia_i \defeq i, the element ∑i=13ai\sum_{i=1}^{3} a_i is:

answer one of these

In the expression ∑i=1nai\sum_{i=1}^{n} a_i:

answer one of these

Exercises in Lean

 

The proofs below are checked in your browser. Nothing is sent anywhere, and nothing is stored but your own work. Type \to for →, \and for ∧, \< and \> for ⟨ ⟩.

The last sheet gave the checker pairs, products, maps, and the sets the pairing axiom lists. This one adds a Peano system to compute in.

The successor

A listed set is typed as it is written, {x} and {x, y}, and its membership criterion is the one the axiom gives: y ∈ {x} is y = x, in the way that x ∈ A ∩ B was a conjunction on an earlier sheet. So the successor needs no notation of its own; it is x ∪ {x}.

Example.

The membership and the equation are one statement, so nothing has to be done to pass between them.

lean worked
1example (x y : Obj) (h : y ∈ {x}) : y = x := by
verified
goalGoals accomplished.

Example.

A union is a disjunction, and its right half is an equation that holds of itself.

lean worked
1example (x : Obj) : x ∈ x ∪ {x} := by
verified
goalGoals accomplished.

Exercise 5.9.

The first half of Proposition 5.10 .

lean proof
1example (x : Obj) : x ⊆ x ∪ {x} := by
goalx : Obj ⊢ x ⊆ x ∪ {x}

Exercise 5.10.

The fourth Peano condition for (N0,0,s)(\mathbb{N}_0, 0, s).

lean proof
1example (x : Obj) : x ∪ {x} ≠ ∅ := by
goalx : Obj ⊢ ¬x ∪ {x} = ∅

Exercise 5.11.

Two inductive sets, and their intersection.

lean proof
1example (I J : Obj) (hI : ∅ ∈ I ∧ ∀ x : Obj, x ∈ I → x ∪ {x} ∈ I)2    (hJ : ∅ ∈ J ∧ ∀ x : Obj, x ∈ J → x ∪ {x} ∈ J) :3    ∅ ∈ I ∩ J ∧ ∀ x : Obj, x ∈ I ∩ J → x ∪ {x} ∈ I ∩ J := by
goalI J : Obj hI : ∅ ∈ I ∧ (∀ (x : Obj), x ∈ I → x ∪ {x} ∈ I) hJ : ∅ ∈ J ∧ (∀ (x : Obj), x ∈ J → x ∪ {x} ∈ J) ⊢ ∅ ∈ I ∩ J ∧ (∀ (x : Obj), x ∈ I ∩ J → x ∪ {x} ∈ I ∩ J)

Exercise 5.12.

Transitivity passes to the successor, which is the step of the induction that makes every element of N0\mathbb{N}_0 transitive.

lean proof
1example (t : Obj) (h : ∀ y : Obj, y ∈ t → y ⊆ t) :2    ∀ y : Obj, y ∈ t ∪ {t} → y ⊆ t ∪ {t} := by
goalt : Obj h : ∀ (y : Obj), y ∈ t → y ⊆ t ⊢ ∀ (y : Obj), y ∈ t ∪ {t} → y ⊆ t ∪ {t}

Exercise 5.13.

The second half of Proposition 5.10 : a set between xx and its successor which reaches outside xx is the successor.

lean proof
1example (x z y : Obj) (h1 : x ⊆ z) (h2 : z ⊆ x ∪ {x}) (hy : y ∈ z) (hyx : y ∉ x) :2    z = x ∪ {x} := by
goalx z y : Obj h1 : x ⊆ z h2 : z ⊆ x ∪ {x} hy : y ∈ z hyx : ¬y ∈ x ⊢ z = x ∪ {x}

Exercise 5.14.

And the third Peano condition, which transitivity was proved for.

lean proof
1example (m n : Obj) (hm : ∀ y : Obj, y ∈ m → y ⊆ m) (hn : ∀ y : Obj, y ∈ n → y ⊆ n)2    (h : m ∪ {m} = n ∪ {n}) : m = n := by
goalm n : Obj hm : ∀ (y : Obj), y ∈ m → y ⊆ m hn : ∀ (y : Obj), y ∈ n → y ⊆ n h : m ∪ {m} = n ∪ {n} ⊢ m = n

A Peano system

ℕ is now read as the carrier XX, with 0 its distinguished element and succ its successor. Nothing about the sets 0=∅0 = \emptyset and 1={∅}1 = \{\emptyset\} survives the change: what a proof may use is the five conditions and nothing else. Two of them have names, Nat.succ_inj for the third and Nat.succ_ne_zero for the fourth. The fifth is a tactic.

induction

induction n with k ih is the fifth condition applied to the set of nn at which the goal holds. It leaves two goals: the goal at 0, and the goal at succ k with ih recording it at k. Prove them under focus dots, as with any pair of goals.

Addition and multiplication arrive as their defining clauses, Nat.add_zero and Nat.add_succ, Nat.mul_zero and Nat.mul_succ. A clause may be cited bare: rw [Nat.add_succ] finds the first ?m + succ ?n in the goal and reads the two off it, and rw [Nat.add_succ m n] names them.

Example.

Two clauses, in the order the sum is peeled: the successor first, then the zero underneath it. rw closes what is left when both sides come out the same.

lean worked
1example (m : ℕ) : m + succ 0 = succ m := by
verified
goalGoals accomplished.

Example.

The first half of Proposition 5.24 . It is listed below as Nat.zero_add, along with the rest of what the lecture proved, so the exercises may lean on it.

lean worked
1example (n : ℕ) : 0 + n = n := by
verified
goalGoals accomplished.

Exercise 5.15.

One is not zero.

lean proof
1example : succ 0 ≠ 0 := by
goal⊢ ¬succ 0 = 0

Exercise 5.16.

A successor may be moved from one side of a sum to the other.

lean proof
1example (m n : ℕ) : m + succ n = succ m + n := by
goalm n : ℕ ⊢ m + succ n = succ m + n

Exercise 5.17.

Corollary 5.19 .

lean proof
1example (n : ℕ) : succ n ≠ n := by
goaln : ℕ ⊢ ¬succ n = n

Exercise 5.18.

Addition cancels.

lean proof
1example (x y z : ℕ) : x + z = y + z → x = y := by
goalx y z : ℕ ⊢ x + z = y + z → x = y

Exercise 5.19.

Corollary 5.28 .

lean proof
1example (m n : ℕ) : m + n = 0 → m = 0 ∧ n = 0 := by
goalm n : ℕ ⊢ m + n = 0 → m = 0 ∧ n = 0

Exercise 5.20.

Nothing but zero can be added without moving.

lean proof
1example (m b : ℕ) : b ≠ 0 → m + b ≠ m := by
goalm b : ℕ ⊢ ¬b = 0 → ¬m + b = m

Exercise 5.21.

A map commuting with the successor is a translation. No commutativity is needed.

lean proof
1example (a : ℕ → ℕ) (h : ∀ n : ℕ, a (succ n) = succ (a n)) (n : ℕ) :2    a n = a 0 + n := by
goala : ℕ → ℕ h : ∀ (n : ℕ), a (succ n) = succ (a n) n : ℕ ⊢ a n = a 0 + n

Exercise 5.22.

Multiplication from the left, at zero.

lean proof
1example (m : ℕ) : 0 * m = 0 := by
goalm : ℕ ⊢ 0 * m = 0

Exercise 5.23.

And one is an identity on the right.

lean proof
1example (m : ℕ) : m * succ 0 = m := by
goalm : ℕ ⊢ m * succ 0 = m

Exercise 5.24.

Multiplication from the left, at a successor. The two clauses only ever act on the right, so this one takes more work.

lean proof
1example (m n : ℕ) : succ m * n = m * n + n := by
goalm n : ℕ ⊢ succ m * n = m * n + n

Exercise 5.25.

Multiplication distributes over addition.

lean proof
1example (m n p : ℕ) : m * (n + p) = m * n + m * p := by
goalm n p : ℕ ⊢ m * (n + p) = m * n + m * p

Exercise 5.26.

And it commutes, once both sides can be peeled.

lean proof
1example (m n : ℕ) : m * n = n * m := by
goalm n : ℕ ⊢ m * n = n * m
What the checker understands

Tactics

intro h assume the hypothesis of an implication, naming it h
exact e give the proof outright
apply f reduce the goal to the hypotheses of f
assumption close the goal with a hypothesis already present
trivial close the goal True
exfalso replace the goal with False
by_contra h assume the negation of the goal
constructor split ∧ into both halves, or ↔ into both directions
left / right choose which half of a ∨ to prove
rcases h with a | b argue by cases on a disjunction
obtain ⟨a, b⟩ := h take a conjunction or an existential apart
cases h as above, keeping the name
refine e give the proof with holes left in it
have h : p := … record an intermediate result
show p restate the goal in an equal form
use w give a witness for ∃
specialize h a instantiate a ∀ hypothesis
rw [h] rewrite with an equation, ← to go backwards
rfl both sides compute to the same thing
decide / norm_num settle a closed computation
tauto close a goal that is true by pure logic
induction n with k ih the fifth Peano condition: prove the goal at 0, then at succ k from ih

Results you may cite

Classical.em ∀ (a : Prop), a ∨ ¬a — the law of excluded middle
Classical.byContradiction ∀ {a : Prop}, (¬a → False) → a — proof by contradiction; the tactic by_contra does this for you
Classical.byCases ∀ {a b : Prop}, (a → b) → (¬a → b) → b — split on whether a holds
not_not ∀ {a : Prop}, ¬¬a ↔ a — double negation
not_and_or ∀ {a b : Prop}, ¬(a ∧ b) ↔ ¬a ∨ ¬b — De Morgan
not_or ∀ {a b : Prop}, ¬(a ∨ b) ↔ ¬a ∧ ¬b — De Morgan
not_imp ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
and_comm ∀ {a b : Prop}, a ∧ b ↔ b ∧ a
or_comm ∀ {a b : Prop}, a ∨ b ↔ b ∨ a
Set.ext ∀ {A B : Obj}, (∀ x : Obj, x ∈ A ↔ x ∈ B) → A = B — extensionality: sets with the same elements are equal
Set.ext_iff ∀ {A B : Obj}, A = B ↔ (∀ x : Obj, x ∈ A ↔ x ∈ B) — extensionality and substitution, in one biconditional
Set.subset_antisymm ∀ {A B : Obj}, A ⊆ B → B ⊆ A → A = B — mutual inclusion is equality
Set.empty_subset ∀ {A : Obj}, ∅ ⊆ A — the empty set is a subset of every set
Set.pair_eq ∀ {a b c d : Obj}, ((a, b) = (c, d)) ↔ (a = c ∧ b = d) — two ordered pairs are equal exactly when their coordinates are
Nat.succ_inj ∀ {m n : ℕ}, succ m = succ n → m = n — the third Peano condition: the successor is injective
Nat.succ_ne_zero ∀ (n : ℕ), succ n ≠ 0 — the fourth: zero is nobody's successor
Nat.pred ∀ {n : ℕ}, n ≠ 0 → ∃ m : ℕ, n = succ m — predecessors: everything but zero is a successor
Nat.add_zero ∀ (m : ℕ), m + 0 = m — the first clause of addition
Nat.add_succ ∀ (m n : ℕ), m + succ n = succ (m + n) — the second clause of addition
Nat.zero_add ∀ (n : ℕ), 0 + n = n — addition from the left
Nat.succ_add ∀ (m n : ℕ), succ m + n = succ (m + n) — addition from the left, at a successor
Nat.add_assoc ∀ (m n p : ℕ), (m + n) + p = m + (n + p) — addition is associative
Nat.add_comm ∀ (m n : ℕ), m + n = n + m — addition is commutative
Nat.add_ne_zero ∀ {a : ℕ} (b : ℕ), a ≠ 0 → a + b ≠ 0 — positivity is absorbing
Nat.mul_zero ∀ (m : ℕ), m * 0 = 0 — the first clause of multiplication
Nat.mul_succ ∀ (m n : ℕ), m * succ n = m * n + m — the second clause of multiplication
Nat.zero_mul ∀ (m : ℕ), 0 * m = 0 — multiplication from the left
Nat.succ_mul ∀ (m n : ℕ), succ m * n = m * n + n — multiplication from the left, at a successor

From the logical core

And.intro ∀ {a b : Prop}, a → b → a ∧ b
And.left ∀ {a b : Prop}, a ∧ b → a
And.right ∀ {a b : Prop}, a ∧ b → b
And.symm ∀ {a b : Prop}, a ∧ b → b ∧ a
Or.inl ∀ {a b : Prop}, a → a ∨ b
Or.inr ∀ {a b : Prop}, b → a ∨ b
Or.elim ∀ {a b c : Prop}, a ∨ b → (a → c) → (b → c) → c
Or.symm ∀ {a b : Prop}, a ∨ b → b ∨ a
Iff.intro ∀ {a b : Prop}, (a → b) → (b → a) → (a ↔ b)
Iff.mp ∀ {a b : Prop}, (a ↔ b) → a → b
Iff.mpr ∀ {a b : Prop}, (a ↔ b) → b → a
Iff.symm ∀ {a b : Prop}, (a ↔ b) → (b ↔ a)
Iff.rfl ∀ {a : Prop}, a ↔ a
Iff.trans ∀ {a b c : Prop}, (a ↔ b) → (b ↔ c) → (a ↔ c)
True.intro True
False.elim ∀ {a : Prop}, False → a
absurd ∀ {a b : Prop}, a → ¬a → b
id ∀ {a : Prop}, a → a
mt ∀ {a b : Prop}, (a → b) → ¬b → ¬a
Eq.refl ∀ {α : Type} (a : α), a = a
Eq.symm ∀ {α : Type} {a b : α}, a = b → b = a
Eq.trans ∀ {α : Type} {a b c : α}, a = b → b = c → a = c
congrArg ∀ {α : Type} {β : Type} {a b : α} (f : α → β), a = b → f a = f b
Exists.intro ∀ {α : Type} {p : α → Prop} (w : α), p w → ∃ x : α, p x
Exists.elim ∀ {α : Type} {p : α → Prop} {b : Prop}, (∃ x : α, p x) → (∀ y : α, p y → b) → b