Counting

The natural numbers from nothing but a zero and a successor: Peano's axioms, addition by recursion, mathematical induction, and the gnomon of the Pythagoreans, which joins the odd numbers into squares.

“God made the integers, all else is the work of man,” Leopold Kronecker is said to have remarked in 1886. At the end of the nineteenth century mathematicians wanted to know more precisely. What exactly is a natural number, and what must we assume about it so that everything else follows? The answer that Richard Dedekind found in 1888 and Giuseppe Peano in 1889 is astonishingly brief: you need a first number and the possibility of always counting one further.

Peano’s axioms

Like Lean, we start at zero and write $S(n)$ for the successor of $n$ , the number that comes next when counting.

Axiom 1 to 5

There is a set $\mathbb{N}_0$ , an element $0 \in \mathbb{N}_0$ and a map $S : \mathbb{N}_0 \to \mathbb{N}_0$ with

$0 \in \mathbb{N}_0$ ,
$n \in \mathbb{N}_0 \Rightarrow S(n) \in \mathbb{N}_0$ ,
$S(n) \neq 0$ for all $n$ ,
$S(m) = S(n) \Rightarrow m = n$ ,
If $A \subseteq \mathbb{N}_0$ with $0 \in A$ and $n \in A \Rightarrow S(n) \in A$ , then $A = \mathbb{N}_0$ .

What the five statements say in words:

There is a beginning, zero.
After every number comes another.
The chain never runs back to zero. A clock that starts again at 0 after 11 does not satisfy this axiom.
Two different numbers have different successors. The chain neither branches nor merges.
Whoever starts at zero and keeps counting reaches every number. There are no numbers outside the chain.

The fifth axiom is the axiom of induction, the row of dominoes from Chapter 1. It is the reason why proofs by induction are valid: the set $A$ of numbers for which a statement holds contains zero and, with every number, its successor, so by Axiom 5 it contains all numbers.

The familiar names are just abbreviations: $1 := S(0)$ , $2 := S(1)$ , $3 := S(2)$ and so on. In this language the tetractys is counting on ten times:

10 = S(S(S(S(S(S(S(S(S(S(0)))))))))).

Calculating from counting

Addition need not be assumed either. It is defined by recursion, by saying how to add 0 and how to get one step further.

Definition

For $a, b \in \mathbb{N}_0$ let

a + 0 := a, \qquad a + S(b) := S(a + b).

Likewise for multiplication:

a \cdot 0 := 0, \qquad a \cdot S(b) := a \cdot b + a.

With this every calculation can be traced back to counting on, for example

\begin{aligned} 2 + 2 &= 2 + S(1) = S(2 + 1) \\ &= S(2 + S(0)) = S(S(2 + 0)) \\ &= S(S(2)) = S(3) = 4. \end{aligned}

That looks laborious, and it is meant to. It shows that there is nothing in $2 + 2 = 4$ that does not follow from the axioms. Even things every child knows must now be proven, because the definition only says something about $a + 0$ , not about $0 + a$ .

Theorem 1

For all $a \in \mathbb{N}_0$ , $0 + a = a$ .

Proof

By induction on $a$ . Base case: $0 + 0 = 0$ by definition. Step: If $0 + a = a$ , then $0 + S(a) = S(0 + a) = S(a)$ , the first equation by definition, the second by assumption.

∎

Theorem 2

Addition is commutative: $a + b = b + a$ for all $a, b \in \mathbb{N}_0$ .

Proof

First a lemma: $S(a) + b = S(a + b)$ . It follows by induction on $b$ : for $b = 0$ both sides are $S(a)$ , and from the assumption for $b$ it follows that

\begin{aligned} S(a) + S(b) &= S(S(a) + b) \\ &= S(S(a + b)) = S(a + S(b)). \end{aligned}

Now induction on $b$ for the theorem itself. Base case: $a + 0 = a = 0 + a$ by definition and Theorem 1. Step: If $a + b = b + a$ , then

\begin{aligned} a + S(b) &= S(a + b) \\ &= S(b + a) = S(b) + a, \end{aligned}

the last equation by the lemma.

∎

Following the same pattern one proves that addition is associative, that multiplication is commutative and that the distributive law holds. All the rules of school arithmetic follow from the five axioms.

Checked by computer: the proof in Lean

Here Lean builds the natural numbers itself, exactly after Peano: inductive Number says a number is either zero or succ of a number, its successor. Lean derives Axioms 3 to 5 from this by itself. add is addition as defined above, zero_add is Theorem 1, add_comm is Theorem 2 with the lemma succ_add. At the end comes Theorem 3 about the odd numbers, this time with Lean’s built-in numbers Nat. If you want to practise this yourself: the Natural Number Game by Kevin Buzzard (Imperial College London), now hosted by the University of Düsseldorf, leads step by step through exactly these proofs.

/-! Chapter 2: the natural numbers after Peano, built by hand -/

/-- A natural number is either zero or the successor
    of a natural number. -/
inductive Number where
  | zero : Number
  | succ : Number → Number

open Number

/-- Addition, defined from zero and successor alone:
    a + 0 = a and a + succ b = succ (a + b) -/
def add : Number → Number → Number
  | a, zero => a
  | a, succ b => succ (add a b)

/-- Theorem 1: 0 + a = a. This is not part of the definition
    and has to be proven. -/
theorem zero_add (a : Number) : add zero a = a := by
  induction a with
  | zero => rfl
  | succ a ih => simp [add, ih]

/-- Lemma: succ a + b = succ (a + b) -/
theorem succ_add (a b : Number) :
    add (succ a) b = succ (add a b) := by
  induction b with
  | zero => rfl
  | succ b ih => simp [add, ih]

/-- Theorem 2: Addition is commutative, a + b = b + a. -/
theorem add_comm (a b : Number) : add a b = add b a := by
  induction b with
  | zero => simp [add, zero_add]
  | succ b ih => simp [add, succ_add, ih]

/-- The sum of the first n odd numbers
    1 + 3 + … + (2n − 1) -/
def odd_sum : Nat → Nat
  | 0 => 0
  | n + 1 => odd_sum n + (2 * n + 1)

/-- Theorem 3: 1 + 3 + 5 + … + (2n − 1) = n² -/
theorem odd_sum_square (n : Nat) : odd_sum n = n * n := by
  induction n with
  | zero => rfl
  | succ n ih =>
    rw [odd_sum, ih]
    grind

Try it in the browser at live.lean-lang.org ↗How to read Lean

The gnomon of the Pythagoreans

The Pythagoreans laid out numbers with pebbles and saw laws in them that today are proven by induction. The most famous is the gnomon, the carpenter’s square. Laying an angle around a square of pebbles makes the next square, and the angles contain 1, 3, 5, 7 … pebbles in turn, the odd numbers. Aristotle briefly mentions the placing of gnomons around the one in his Physics (III 4) as a teaching of the Pythagoreans, the reading with the odd numbers and the squares comes from later commentators.

Each angle contains two pebbles more than the previous one. Together the first n odd numbers make the square n by n.

Theorem 3

For all $n \in \mathbb{N}$

\begin{gathered} 1 + 3 + 5 + \dots + (2n - 1) \\ = \sum_{i=1}^{n} (2i - 1) = n^2. \end{gathered}

Proof

By induction on $n$ . Base case: for $n = 1$ , $1 = 1^2$ . Step: If the formula holds for $n$ , then

\begin{aligned} \sum_{i=1}^{n+1} (2i - 1) &= n^2 + (2n + 1) \\ &= (n+1)^2. \end{aligned}

That is exactly the angle in the picture: around the square $n \times n$ you lay $n$ pebbles on top, $n$ on the right and one in the corner, $2n + 1$ together.

∎

Here one sees why Pythagorean number lore is often called an origin of mathematics as we know it, even though Babylonians and Egyptians calculated earlier. The pebbles are no game. Whoever sees that the angle is built the same way for every square has understood the inductive step, even if the name for it came two thousand years later. In the same way the even numbers give the oblong numbers $n(n+1)$ , and their halves are the triangular numbers of Chapter 1.

Where this appears on the website

Triangular numbers, tetrahedral numbers and the simplexes with their $T(n-1)$ edges (see The triangle of points and From point to solid) are all defined by such sums, and their formulas are proven by induction. How dividing is gained from counting is shown in the next chapter, Dividing.

Sources and further reading

Sources

Richard Dedekind, Was sind und was sollen die Zahlen?, Brunswick 1888
Giuseppe Peano, Arithmetices principia, nova methodo exposita, Turin 1889
Aristotle, Physics III 4, 203a (the gnomon)
Heinrich Weber, Leopold Kronecker, Jahresbericht der Deutschen Mathematiker-Vereinigung 2, 1893 (the saying about the integers)

Counting

Peano’s axioms

Calculating from counting

The gnomon of the Pythagoreans

Where this appears on the website

Sources

Further reading