← MA0 1 · Introduction to University Mathematics (Proofs)

Lesson 5

Natural Numbers

Taught 15 Aug 2026

Natural Numbers

The Set of Natural Numbers

The starting point of our journey shall be the counting numbers, $1, 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^{\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 $0$ .

The Axiom of Infinity

At the close of the last chapter we watched the passage from $A$ to $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. That gap is closed by naming the property such a set would have. Throughout we write $s(x) \defeq x \cup \{x\}$ and call it the successor of $x$ .

Definition 5.1 (Inductive set).

A set $I$ is inductive if $\emptyset \in I$ and $s(x) \in I$ for every $x \in I$ .

Axiom 5.2 (Infinity).

An inductive set exists: $\exists I\,\bigl(\emptyset \in I \land \forall x\,(x \in I \implies x \cup \{x\} \in I)\bigr)$ .

The notation $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 $I$ be an inductive set. We write $\mathbb{N}_0$ for the intersection of all inductive subsets of $I$ ,

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

and $\mathbb{N} \defeq \mathbb{N}_0 \setminus \{\emptyset\}$ . The elements of $\mathbb{N}$ are the natural numbers.

The collection being intersected is a set by comprehension applied to $\mathcal{P}(I)$ , and it is non-empty, since $I$ is one of its members; the intersection of a system then does the rest. Writing $0 \defeq \emptyset$ , $1 \defeq s(0)$ , $2 \defeq s(1)$ and so on, we have

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

Remark (Where to start).

Whether $0$ counts as a natural number is a matter of convention rather than of mathematics, and both choices are in use. We keep $1$ 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 $\mathbb{N}_0$ rather than $\mathbb{N}$ that the axioms below describe.

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

$0 \in \mathbb{N}_0$ .

Discussion.

Membership in $\mathbb{N}_0$ is membership in every inductive subset of $I$ , so there is nothing to construct: we take an arbitrary such subset and read off what being inductive already 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 $J$ be an arbitrary inductive subset of $I$ . Then $\emptyset \in J$ by the definition of an inductive set. Since $J$ was arbitrary, $\emptyset$ belongs to every inductive subset of $I$ , and so $0 = \emptyset \in \mathbb{N}_0$ .

Proposition 5.5 (Closure under successors).

If $n \in \mathbb{N}_0$ , then $s(n) \in \mathbb{N}_0$ .

Discussion.

The same move again, one step further along. Assuming $n \in \mathbb{N}_0$ and taking an arbitrary inductive subset $J$ of $I$ , the definition of the intersection puts $n$ in $J$ , and the second clause of inductiveness carries it to $s(n) \in J$ . As $J$ was arbitrary, $s(n)$ lies in every inductive subset, which is membership in $\mathbb{N}_0$ .

Proof.

Suppose $n \in \mathbb{N}_0$ and let $J$ be an arbitrary inductive subset of $I$ . Then $n \in J$ , and so $s(n) \in J$ by the definition of an inductive set. Since $J$ was arbitrary, $s(n)$ belongs to every inductive subset of $I$ , hence $s(n) \in \mathbb{N}_0$ .

The two propositions together say that $\mathbb{N}_0$ is itself inductive, and by its very definition it lies inside every inductive subset of $I$ . It is the smallest inductive set of all, and that is exactly what makes induction work.

Theorem 5.6 (Induction for sets).

Let $S \subset \mathbb{N}_0$ with $0 \in S$ and $s(n) \in S$ whenever $n \in S$ . Then $S = \mathbb{N}_0$ .

Discussion.

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

Proof.

The two hypotheses say precisely that $S$ is inductive, and $S \subset \mathbb{N}_0 \subset I$ , so $S$ is an inductive subset of $I$ . The intersection defining $\mathbb{N}_0$ is contained in each set intersected, so $\mathbb{N}_0 \subset S$ . With $S \subset \mathbb{N}_0$ from the hypothesis, mutual inclusion gives $S = \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 $P$ determines the subset $\{n \in \mathbb{N}_0 \mid P(n)\}$ , so proving $P$ of every natural number is proving that this subset is everything.

Theorem 5.7 (Induction for predicates).

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

Discussion.

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

Proof.

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

Problem 5.1.

Let $I$ and $J$ be inductive sets.

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

The definition of $\mathbb{N}_0$ began by choosing an inductive set $I$ , and nothing so far says the answer does not depend on that choice. It does not, and the reason is that $\mathbb{N}_0$ is smaller than every inductive set, not merely than the inductive subsets of $I$ .

Proposition 5.8 (The least inductive set).

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

Discussion.

That $\mathbb{N}_0$ is inductive is the two propositions above read together, one supplying $\emptyset$ and the other closure under $s$ . The second claim is the delicate half, since an arbitrary inductive $K$ need not be a subset of $I$ and so is not among the sets we intersected. The problem above repairs that: $I \cap K$ is inductive, and it is a subset of $I$ , so it is one of the sets intersected and therefore holds $\mathbb{N}_0$ . Being inside $I \cap K$ puts $\mathbb{N}_0$ inside $K$ .

Proof.

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

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

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

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

Proof.

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

One more fact about the successor is worth having before we leave it, since it says exactly how much $s$ adds.

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

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

Discussion.

The inclusion is immediate, since $s(x)$ is a union with $x$ as one of its parts. For the second claim we take any $z$ with $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 $z$ adds nothing to $x$ , in which case the two inclusions make $z = x$ ; or it holds something outside $x$ , and that something has nowhere to be but $x$ itself, since the only element of $s(x)$ outside $x$ is $x$ . Then $x \in z$ , and with $x \subset z$ already in hand every element of $s(x)$ lies in $z$ .

Proof.

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

Now let $z$ satisfy $x \subset z \subset s(x)$ . If $z \subset x$ , then with $x \subset z$ we get $z = x$ . Otherwise some $y \in z$ has $y \notin x$ ; since $y \in z \subset x \cup \{x\}$ , this forces $y = x$ , so $x \in z$ . Together with $x \subset z$ this puts every element of $x \cup \{x\}$ in $z$ , that is, $s(x) \subset z$ , and so $z = s(x)$ . Hence $z$ is $x$ or $s(x)$ , and no $z$ satisfies $x \subsetneq z \subsetneq s(x)$ .

Peano Systems

Definition 5.11 (Peano system).

A Peano system is a set $X$ together with a distinguished element $0$ and a map $s$ , called the successor, satisfying

$0 \in X$ ;
$s(x) \in X$ whenever $x \in X$ ;
if $s(x) = s(y)$ , then $x = y$ ;
$s(x) \neq 0$ for every $x \in X$ ;
if $Y \subset X$ , $0 \in Y$ , and $s(y) \in Y$ whenever $y \in Y$ , then $Y = X$ .

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

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

In any Peano system we write $1 \defeq s(0)$ , $2 \defeq s(1)$ , $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 $0$ and keep taking successors, producing $0$ , $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 $X$ 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:

\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 is not idle. Take $X$ to be the real numbers $x$ with $x \geqslant 0$ , with the usual $0$ and $s(x) \defeq x + 1$ . The first four conditions all hold, yet $\tfrac{1}{2}$ lies in $X$ and is reached by no finite string of successors from $0$ . It is the fifth that fails: the subset $Y$ consisting of $0$ and the counting numbers holds $0$ , and holds $y + 1$ whenever it holds $y$ , yet $Y \neq X$ .

The fifth condition is the principle of induction, and Peano’s contribution was to place it inside the structure of the numbers rather than treat it as a proof technique arriving from outside. Its predicate form is the theorem proved above, transported to an arbitrary Peano system by the same passage from a predicate to the subset it cuts out.

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

$(\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 \cup \{x\}$ , not about smallness. The fourth is quick, since $s(x)$ always holds $x$ and so is never empty. The third asks that $x \cup \{x\} = y \cup \{y\}$ force $x = y$ , and the route to it runs through the observation that every element of $\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 \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) \neq \emptyset$ for every set $x$ , which is the fourth condition for $(\mathbb{N}_0, 0, s)$ .

Problem 5.3.

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

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

Problem 5.4.

Let $A = \{0, 1, 2, 3\}$ with $0$ distinguished, and define $s(0) \defeq 1$ , $s(1) \defeq 2$ , $s(2) \defeq 3$ and $s(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-looking facts about them have to be earned from the five conditions. The next three propositions earn the first of them.

Proposition 5.15 (Three is a natural number).

$3 \in X$ .

Discussion.

There is nothing to do but walk along the chain. The first condition puts $0$ in $X$ , and the second carries membership from any element to its successor, so we apply it three times, at $0$ , at $1$ and at $2$ . Nothing else is available and nothing else is needed.

Proof.

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

Proposition 5.16 (Four is not zero).

$4 \neq 0$ .

Discussion.

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

Proof.

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

Proposition 5.17 (Six is not two).

$6 \neq 2$ .

Discussion.

Here the fourth condition does not apply directly, since neither number is $0$ . Instead we work backwards down the chain with the third condition, which strips a successor from both sides of an equation: assuming $6 = 2$ gives $s(5) = s(1)$ , hence $5 = 1$ , hence $s(4) = s(0)$ , hence $4 = 0$ . That is what the previous proposition forbids, so the assumption cannot stand. This is the pattern promised earlier, that repeated use of the third condition drives any coincidence down to a contradiction with the fourth.

Proof.

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

Predecessors

Theorem 5.18 (Predecessors).

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

Discussion.

We prove the equality by two inclusions. The fourth condition gives $s(X) \subset X \setminus \{0\}$ at once, since no successor is $0$ . 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 \defeq \{0\} \cup s(X)$ and let induction do the work. This $Y$ holds $0$ by construction and is closed under $s$ because every $s(y)$ lies in $s(X)$ , so the fifth condition forces $Y = X$ , and every non-zero element is therefore a successor. The uniqueness of the predecessor is then the third condition.

Proof.

Let $Y \defeq \{0\} \cup s(X)$ . Then $0 \in Y$ , and if $y \in Y$ then $s(y) \in s(X) \subset Y$ , so $Y = X$ by the fifth condition. Thus every $x \neq 0$ lies in $s(X)$ , while $0$ does not by the fourth, and so $s(X) = X \setminus \{0\}$ .

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

The pairs of $s$ can therefore be read backwards. Regarded as a map onto $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 \setminus \{0\} \to X,

the predecessor map, satisfying $s^{-1} \circ s = \operatorname{id}_X$ and $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 \to X \setminus \{0\}$ be a bijection.

Corollary 5.19 (No element is its own successor).

In a Peano system, $s(x) \neq x$ for every $x \in X$ .

Proof.

Let $Y \defeq \{x \in X \mid s(x) \neq x\}$ . By the fourth condition $s(0) \neq 0$ , so $0 \in Y$ . Suppose $x \in Y$ . If $s(s(x)) = s(x)$ , then $s(x) = x$ by the third condition, contradicting $x \in Y$ ; hence $s(x) \in Y$ . By the fifth condition, $Y = 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 said without one: a non-empty subset ought to hold an element that the subset cannot reach by a successor step, an element where it starts.

Theorem 5.20 (Induction without order).

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

The only subset of $X$ holding $0$ and closed under $s$ is $X$ itself.
Every non-empty subset $M \subset X$ holds an element $m$ with $m \notin s(M)$ .

Discussion.

We prove both implications by contradiction, since each hypothesis is a statement about all subsets and offers nothing to build with directly. Suppose the first holds and the second fails. Then some non-empty $M$ satisfies $M \subset s(M)$ , and we pass to the complement $Y \defeq X \setminus M$ : the codomain of $s$ excludes $0$ , which puts $0$ in $Y$ , and injectivity shows $Y$ is closed under $s$ , so the first condition makes $Y = X$ and $M$ empty. Conversely, suppose the second holds and some proper $Y$ holds $0$ and is closed under $s$ . The complement $M$ is non-empty, so it has a starting element $m$ , which is not $0$ and is therefore $s(n)$ for some $n$ by surjectivity. Asking where $n$ lives contradicts the choice of $m$ either way.

Proof.

Suppose the second statement fails for the non-empty set $M \subset X$ , so $M \subset s(M)$ , and put $Y \defeq X \setminus M$ . If $0 \in M$ , then $0 \in s(M) \subset s(X)$ , which is impossible since the codomain of $s$ is $X \setminus \{0\}$ ; hence $0 \in Y$ . Let $y \in Y$ and suppose $s(y) \notin Y$ . Then $s(y) \in M \subset s(M)$ , so $s(y) = s(m)$ for some $m \in M$ , and injectivity gives $y = m \in M$ , contradicting $y \in Y$ . Thus $Y$ holds $0$ and is closed under $s$ , so $Y = X$ by the first statement and $M = \emptyset$ , a contradiction.

Conversely, let $Y \subset X$ hold $0$ and be closed under $s$ , and suppose $Y \neq X$ . Then $M \defeq X \setminus Y$ is non-empty, and the second statement provides $m \in M$ with $m \notin s(M)$ . Since $0 \in Y$ we have $m \neq 0$ , so surjectivity gives $m = s(n)$ for some $n \in X$ . If $n \in M$ , then $m \in s(M)$ , against the choice of $m$ ; if $n \in Y$ , then $m = s(n) \in Y$ by closure, against $m \in M$ . Neither is possible, so no such $Y$ exists.

Problem 5.5 (Informal).

Note that

\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/2$ , that $1 + 1/2 + 1/4 = 2 - 1/4$ , and that $1 + 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/2$ , that $(1 - 1/2)(1 - 1/3) = 1/3$ , and that $(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 \in \mathbb{N}$ with $n \geqslant 2$ , guess a general law which simplifies the product

\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

We now turn to a deeper question: in what sense are the natural numbers unique? The elements of two Peano systems may look completely different, yet the conditions pin down everything except the names. Any two are linked by a relabelling that respects the only structure present, the zero and the successor:

\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 $0$ to $0'$ , hence $s(0)$ to $s'(0')$ , and so on down the ladder. What the picture does not show is that the instruction “start at $0'$ and keep applying $s'$ ” genuinely defines a map on all of $X$ . Turning such an instruction into a function is called recursion, or inductive definition.

One piece of language first. Given maps $\alpha : A \to B$ , $\beta : B \to D$ , $\gamma : A \to C$ and $\delta : C \to D$ , we draw

\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 $A$ to $D$ 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)$ be a Peano system, let $A$ be a set with an element $a \in A$ , and let $g : A \to A$ . Then there is exactly one map $\alpha : X \to A$ with $\alpha(0) = a$ and $\alpha \circ s = g \circ \alpha$ ; that is, exactly one $\alpha$ sending $0$ to $a$ and making the square

\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 $\alpha(s(n)) = g(\alpha(n))$ , so the map is prescribed at $0$ 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 $0$ and is closed under $s$ , so the fifth condition makes it all of $X$ . 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 \subset X \times A$ admissible when it holds $(0, a)$ and sends each $(n, c) \in C$ to $(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 \in X$ occurs in exactly one pair of $\Gamma$ , and both halves of that are inductions. The second half turns on 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 are what make the two deletions legitimate.

Proof.

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

For existence, call $C \subset X \times A$ admissible if $(0, a) \in C$ and $(s(n), g(c)) \in C$ whenever $(n, c) \in C$ . The whole of $X \times A$ is admissible, so the admissible sets form a non-empty collection, carved from $\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 \in X$ appears in exactly one pair of $\Gamma$ ; by the definition of a function the claim makes $\Gamma$ a function $\alpha : X \to A$ , and admissibility then reads $\alpha(0) = a$ and $\alpha(s(n)) = g(\alpha(n))$ .

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

That no $n$ appears twice is an induction on $Z \defeq \{n \in X \mid n \text{ appears in exactly one pair of } \Gamma\}$ . The move throughout is that 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) \in \Gamma$ with $c \neq a$ , and delete it. The set $\Gamma \setminus \{(0, c)\}$ still holds $(0, a)$ , and it is still closed, since every pair the rule produces has first coordinate $s(n)$ , which is never $0$ by the fourth condition. Hence no such $c$ exists and $0 \in Z$ .

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

Theorem 5.22 (Uniqueness of Peano systems).

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

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

commute.

Discussion.

The recursion theorem does the work, applied with $A = X'$ , $a = 0'$ and $g = s'$ : it hands us a unique map $\alpha$ with $\alpha(0) = 0'$ and $\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 $\alpha' : X' \to X$ , and the composite $\alpha' \circ \alpha$ sends $0$ to $0$ and commutes with $s$ , so it solves the same recursion problem on $X$ 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 = 0'$ and $g = s'$ gives exactly one map $\alpha : X \to X'$ with $\alpha(0) = 0'$ and $\alpha \circ s = s' \circ \alpha$ ; it remains to prove $\alpha$ bijective. Exchanging the systems gives likewise a unique $\alpha' : X' \to X$ with $\alpha'(0') = 0$ and $\alpha' \circ s' = s \circ \alpha'$ .

Put $\iota \defeq \alpha' \circ \alpha : X \to X$ . Then $\iota(0) = \alpha'(0') = 0$ , and associativity of composition lets us compute without brackets:

\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 $X$ with $a = 0$ and $g = s$ ; so does $\operatorname{id}_X$ ; and by the uniqueness clause $\iota = \operatorname{id}_X$ . The same argument with the systems exchanged gives $\alpha \circ \alpha' = \operatorname{id}_{X'}$ . Hence $\alpha'$ is an inverse of $\alpha$ , and $\alpha$ is bijective by invertibility.

The condition $\alpha(0) = 0'$ costs nothing, incidentally: any bijection $\beta : X \to X'$ with $\beta \circ s = s' \circ \beta$ already sends $0$ to $0'$ . Otherwise surjectivity would provide some $n \neq 0$ with $\beta(n) = 0'$ , the theorem on predecessors would write $n = s(m)$ , and then $0' = \beta(s(m)) = s'(\beta(m))$ would exhibit $0'$ as a successor in $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, \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.

Anything worth calling addition should satisfy $m + 1 = s(m)$ , should be associative, and should have $0$ as an identity. Those demands leave no room to manoeuvre, since the first two give

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

which determines $m + n$ for every $n$ once $m + 0 = m$ is fixed. Whether anything satisfies them is a separate question, and recursion answers it.

Definition 5.23 (Addition).

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

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

The wish is granted: $m + 1 = m + s(0) = s(m + 0) = s(m)$ . The defining clauses absorb a $0$ or an $s$ on the right of a sum; the laws of addition will need the same moves on the left.

Proposition 5.24 (Addition from the left).

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

Discussion.

We induct on the right-hand variable $n$ in both, since that is the position the defining clauses speak about. For the first, the base case is the clause $m + 0 = m$ read at $m = 0$ , and the step uses the other clause: $0 + s(n) = s(0 + n) = s(n)$ . For the second, fix $m$ and take the statement $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) + n$ by $s(m + n)$ using the hypothesis, and apply the clause once more. As $m$ was arbitrary throughout, the result holds for all $m$ and $n$ .

Proof.

Let $Y \defeq \{n \in X \mid 0 + n = n\}$ . Since $0 + 0 = 0$ we have $0 \in Y$ , and if $n \in Y$ then $0 + s(n) = s(0 + n) = s(n)$ , so $s(n) \in Y$ . By the fifth condition $Y = X$ .

Now fix $m \in X$ and let $Z \defeq \{n \in X \mid s(m) + n = s(m + n)\}$ . Since $s(m) + 0 = s(m) = s(m + 0)$ we have $0 \in Z$ . If $n \in Z$ , then

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) \in Z$ . By the fifth condition $Z = X$ , and since $m$ was arbitrary the identity holds throughout.

Theorem 5.25 (Laws of addition).

For all $m, n, p \in X$ , we have $(m + n) + p = m + (n + p)$ and $m + 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 $m$ and $n$ and take the statement $(m + n) + p = m + (n + p)$ ; its base case reduces both sides by $r + 0 = r$ , and its step rewrites the left as $s((m+n)+p)$ , applies the hypothesis, and uses the successor clause twice to arrive at $m + (n + s(p))$ . For commutativity, fix $m$ and take $m + n = n + m$ ; the base case is $m + 0 = m = 0 + m$ , which needs the first identity of the preceding proposition, and the step turns $m + s(n)$ into $s(m + n)$ , applies the hypothesis, and then uses the second identity to reach $s(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 \in X$ and let $Y \defeq \{p \in X \mid (m + n) + p = m + (n + p)\}$ . Both $(m + n) + 0$ and $m + (n + 0)$ equal $m + n$ , so $0 \in Y$ . If $p \in Y$ , then

(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) \in Y$ , and $Y = X$ by the fifth condition.

Next fix $m \in X$ and let $Z \defeq \{n \in X \mid m + n = n + m\}$ . The preceding proposition gives $0 + m = m = m + 0$ , so $0 \in Z$ . If $n \in Z$ , then

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

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

Definition 5.26 (Positive elements).

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

Proposition 5.27 (Positivity is absorbing).

If $a$ is positive and $b \in X$ , then $a + b$ is positive.

Discussion.

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

Proof.

Let $Y \defeq \{b \in X \mid a + b \text{ is positive}\}$ . Since $a + 0 = a$ and $a$ is positive, $0 \in Y$ . If $b \in Y$ , then $a + s(b) = s(a + b)$ , which is not $0$ by the fourth condition, so $s(b) \in Y$ . By the fifth condition $Y = X$ .

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

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

Proof.

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

Problem 5.9.

Define multiplication in a Peano system by the clauses $m \cdot 0 \defeq 0$ and $m \cdot s(n) \defeq m \cdot n + m$ . Show that these clauses do define a map from $X \times X$ to $X$ .

Problem 5.10.

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

$m \cdot (n + p) = m \cdot n + m \cdot p$ ;
$m \cdot n = n \cdot m$ ;
$1 \cdot m = m \cdot 1 = m$ ;
$0 \cdot m = m \cdot 0 = 0$ ;
$(m \cdot n) \cdot p = m \cdot (n \cdot p)$ .

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

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

Discussion.

The sum is Proposition 5.27 read at a positive $b$ , which asked no more of $b$ than that it be an element at all. The product needs one further move. Being positive, $b$ is not $0$ , so the theorem on predecessors writes it as $s(c)$ for a unique $c$ , and the second clause of the multiplication problem turns $a \cdot s(c)$ into $a \cdot c + a$ . That is a sum whose left part we know nothing about and whose right part is positive, which is exactly the situation Proposition 5.27 handles, once commutativity puts the positive part in front. No induction is needed: the predecessor supplies the single step the definition wants.

Proof.

That $a + b$ is positive is Proposition 5.27 , since $a$ is positive.

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

Problem 5.11.

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

Problem 5.12.

Let $a \in X$ . Use the recursion theorem, with a starting element and a map $g : X \to X$ of your choosing, to produce a unique map $\exp_a : X \to X$ satisfying

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

written $a^n$ for $\exp_a(n)$ . Prove directly from the clauses that $a^{s(0)} = a$ , and, writing $2 \defeq s(1)$ , compute $1 + 1$ , $2 \cdot 2$ and $2^2$ from the definitions alone.

Problem 5.13.

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

Problem 5.14.

Let $x, y, z \in X$ .

Prove that if $x \neq y$ , then $x + z \neq y + z$ .
Deduce that $x + z = y + z$ implies $x = y$ .
Show that if $n = m + b$ with $b$ positive, then $n \neq m$ .

Problem 5.15.

Prove that $(a^m)^n = a^{m \cdot n}$ for all $a, m, n \in X$ , and that the map sending $n$ to $a^n$ is the unique one with $\varphi(0) = 1$ , $\varphi(1) = a$ and $\varphi(m + n) = \varphi(m) \cdot \varphi(n)$ for all $m, n \in X$ .

Sums

Induction has so far done the necessary work of establishing properties of the natural numbers. Before going further, it is worth seeing the recursion theorem carry a load it cannot quite manage as it stands.

Imagine defining the running totals $\sigma_n$ , the sum of everything up to $n$ . Once $\sigma_n$ is found, the next total should be $\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 gap is easily closed by carrying the index along.

Proposition 5.30 (Parametrised recursion).

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

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

Discussion.

The recursion theorem hands the next value a single argument, the previous value, while $G$ wants two. So we make the previous value carry its own index: apply the theorem on $X \times A$ rather than on $A$ , starting at $(0, a)$ and stepping by $(n, c) \mapsto \bigl(s(n), G(n, c)\bigr)$ . That gives a map $\beta : X \to X \times A$ , and an induction shows its first coordinate at $n$ is always $n$ 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 \times A$ and is therefore $\beta$ by the uniqueness already proved.

Proof.

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

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

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

If $\alpha'$ is another map with these two properties, let $\beta'(n) \defeq \bigl(n, \alpha'(n)\bigr)$ . Then $\beta'(0) = (0, a)$ and $\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

a_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: $a_1 + a_7 + \cdots + a_{41}$ determines nothing without further context. What follows replaces the convention by a recursion, so that the expression means something whether or not the pattern is visible.

Proposition 5.31 (The summation symbol).

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

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

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

\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 = X$ , initial element $0$ , and $G(n, c) \defeq c + a_{s(n)}$ , which is a map from $X \times X$ to $X$ 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 = X$ , initial element $0$ , and $G : X \times X \to X$ given by $G(n, c) \defeq c + a_{s(n)}$ . It supplies exactly one map $\Sigma : X \to X$ with $\Sigma(0) = 0$ and $\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 $i$ runs through the elements between $1$ and $n$ , only that the recursion starts at $0$ and steps by $s$ . 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

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

while $n$ may not be renamed, since the value depends on it. The value $\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 $a_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 $\Pi : X \to X$ with $\Pi(0) = 1$ and $\Pi(s(n)) = \Pi(n) \cdot a_{s(n)}$ for every $n \in X$ , where multiplication is as defined in the problems above, and write $\displaystyle\prod_{i=1}^{n} a_i$ for $\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.

Let $a_i \defeq 1$ for every $i$ . Prove that $\displaystyle\sum_{i=1}^{n} a_i = n$ and $\displaystyle\prod_{i=1}^{n} a_i = 1$ for every $n \in X$ .
Let $a_i \defeq i$ for every $i$ , so that the sum is the running total of everything up to $n$ . Prove that

\sum_{i=1}^{n} i \;+\; \sum_{i=1}^{n} i \;=\; n \cdot s(n).

Problem 5.18.

Prove that

\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)$ and $(X', 0', s')$ be Peano systems, each carrying the addition of Definition 5.23 and the multiplication of Problem 5.9 , and let $\alpha : X \to X'$ be the bijection of Theorem 5.22 . Prove that $\alpha(m + n) = \alpha(m) + \alpha(n)$ and $\alpha(m \cdot n) = \alpha(m) \cdot \alpha(n)$ for all $m, n \in X$ .

Problem 5.20.

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

Produce a map $F : X \to X$ with $F(0) = 1$ and $F(s(n)) = s(n) \cdot F(n)$ for every $n \in X$ .
Show that there is no $g : X \to X$ with $F(s(n)) = g\bigl(F(n)\bigr)$ for every $n \in X$ , and deduce that Theorem 5.21 taken with $A = X$ cannot produce $F$ .

Problem 5.21.

Let $S$ be a non-empty set and let $H : S \to S$ . Taking for $A$ the set $S^S$ of all maps from $S$ to itself, use Theorem 5.21 to produce the iterates $H^n$ of $H$ , characterised by $H^0 = \operatorname{id}_S$ and $H^{s(n)} = H \circ H^n$ for every $n \in \mathbb{N}_0$ .

Suppose $H\bigl(H(y)\bigr) = y$ for some $y \in S$ . Determine $H^{80}(y)$ and $H^{81}(y)$ , with proof.
Suppose instead that $H\bigl(H(y)\bigr) = H(y)$ . Determine $H^{80}(y)$ , with proof.
Find a map $H : \mathbb{N}_0 \to \mathbb{N}_0$ with $H \circ H = H$ , $H(1) = 36$ , $H(2) = 5$ and $H(13) = 47$ .
Decide whether there is a map $H : \mathbb{N}_0 \to \mathbb{N}_0$ with $H \circ H = H$ , $H(1) = 7$ and $H(7) = 18$ .

Problem 5.22.

Let $a, b : X \to X$ be maps, written $a_i$ for $a(i)$ and $b_i$ for $b(i)$ , and let $c \in X$ . Prove that for every $n \in X$ :

$\displaystyle\sum_{i=1}^{n} (a_i + b_i) = \sum_{i=1}^{n} a_i + \sum_{i=1}^{n} b_i$ ;
$\displaystyle\sum_{i=1}^{n} c \cdot a_i = c \cdot \sum_{i=1}^{n} a_i$ ;
if $a_{s(i)} = a_i + b_{s(i)}$ for every $i \in X$ , then $\displaystyle a_0 + \sum_{i=1}^{n} b_i = a_n$ .

Problem 5.23.

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

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

Problem 5.24.

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

Prove that $4 \cdot \displaystyle\sum_{i=1}^{n} i^3 = n^2 \cdot s(n)^2$ for every $n \in \mathbb{N}$ .
Deduce that $\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, \ldots$ , each after the second being the sum of the two before it.

Produce exactly one map $a : X \to X$ with $a_0 = a_{s(0)} = 1$ and $a_{s(s(n))} = a_{s(n)} + a_n$ for every $n \in X$ , writing $a_n$ for $a(n)$ .
Prove that for every $n \in X$ exactly one of

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.

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.

Example.

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

Exercise 5.9.

The first half of Proposition 5.10 .

Exercise 5.10.

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

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

4  sorry

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 $\mathbb{N}_0$ transitive.

Exercise 5.13.

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

Exercise 5.14.

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

A Peano system

ℕ is now read as the carrier $X$ , with 0 its distinguished element and succ its successor. Nothing about the sets $0 = \emptyset$ and $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 $n$ 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.

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.

Exercise 5.15.

One is not zero.

Exercise 5.16.

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

Addition cancels.

Nothing but zero can be added without moving.

Exercise 5.21.

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

Exercise 5.22.

Multiplication from the left, at zero.

Exercise 5.23.

And one is an identity on the right.

Exercise 5.24.

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

Exercise 5.25.

Multiplication distributes over addition.

Exercise 5.26.

And it commutes, once both sides can be peeled.

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