Natural Numbers

Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk

Leopold Kronecker

Henrich Weber quoted Kronecker saying, “God made the integers, all else is the work of man”. Following this procalamtion, we begin by defining God’s natural numbers using Lean’s inductive type definition. This specifies the only way to construct terms of the type of natural numbers.

inductive ℕ where
  | zero : ℕ
  | succ : ℕ → ℕ

This definition is a type theoretic version of the axiomatisaion written by Giuseppe Peano. In a modern formulation, Peano’s work defines a first-order theory with the following signature:

\[L = \{0,s,+,\times,=\}\]

Stating that 0 is a term in the theory of natural numbers and that the only other way to build terms are with the function symbols s(ucc), + (addition), and $\times$ (multiplication). We will return to addition and multiplication. Starting with zero, further terms are constructed by finitely many applications of the unary succ(essor) function.

  1. zero : ℕ
  2. succ zero : ℕ
  3. succ (succ zero) : ℕ
  4. succ (succ (succ zero)) : ℕ

Ad infinitum. After defining the signature of the first-order theory one would write down some axioms in order to impose the desired (natural number) structure on these terms. Typically one would see the following two axioms first:

$\forall x : ℕ, \ \lnot(succ \ x = 0)$

$\forall x : ℕ, \ \forall y : ℕ, \ succ \ x = succ \ y \to x = y$

One reads the first axiom as saying that there is no number before zero and the second that the unary term generator succ is injective. In Lean, these two axioms are (somewhat) hidden in the properties of inductive definitions. However, we can bring them out as theorems as follows:

theorem succ_not_zero :
  ∀ x : ℕ, succ x ≠ zero :=
  by
    intro m
    intro h₁
    injection h₁

Proof of this negation requires a proof of $\bot$ from the assumption that succ x = zero. This is obtained by calling the (in built) injection function of Lean which says that terms of an inductive type with different sequences of the constructors (zero, succ) are by definition not equal. This same program encoding the fact that inductive term constructors are injective proves the theorem corresponding to the second axiom.

theorem succ_injective :
  ∀ m n : ℕ, succ m = succ n → m = n :=
  by
    intro m n
    intro h₁
    injection h₁

Proof Structure

Some comments should be made about the above proofs. These theorems are both universally quantified statements. Following the “propositions-as-types” (or BHK) interpretation of universal quantification, we must provide a program that takes in an arbitrary (pair of) natural number(s) as input and returns a proof of the claim instantiated at those numbers. That is, the lines intro m and intro m n are akin to writing “Let a be an arbitrary natural number” and “Let m n be arbitrary natural numbers” as one would write in a traditional blackboard proof.

In each of these cases, once instantiated at m n, one is required to prove an implication. In the case of the first theorem, succ x ≠ zero is syntactic sugar for the proposition succ x = zero → ⊥. In order to prove a hypothetical claim, propositions-as-types requires a program that takes evidence of the antecedent (e.g. succ x = zero) and returns evidence of the consequent (e.g. ⊥). The second line of the first proof can be read “Suppose succ m = zero…” and the second line of the second proof can be read “Suppose succ m = succ n…”, as one would write on a traditional blackboard style proof. In both cases evidence of the antecedent is provided by the injectivity of the constructors in an inductive definition.

Proof Result

Lean’s proof checker verifies the type of the proof-term written by the programmer. These proof-terms can be written directly, or by the use of meta-programs (also known as tactics) as in the above proof. Explicit proof-terms are difficult (if not impossible) to write for even some of the most modest theorems. The distinction between tactic proofs vs. explicit proof-terms is similar to that of higher-order programming languages vs. assembly or binary code; it can be done, but why? Meta-programs are here to make authoring formal proofs easier. That being said, the proof terms corresponding to these theorems are relatively short:

theorem succ_not_zero : ∀ (x : ℕ), succ x ≠ zero :=
λ a h₁ => ℕ.noConfusion h₁

theorem succ_injective : ∀ (m n : ℕ), succ m = succ n → m = n :=
λ m n h₁ => ℕ.noConfusion h₁ λ a_eq => a_eq

These are printed on the console by writing #print <theorem_name> e.g. #print succ_not_zero.

Arithmetic on the Natural Numbers

Further to the succ(essor) function, one can construct new terms of the first-order theory of Peano arithmetic by the use of the binary function symbols addition (+) and multiplication ($\times$). In first-order logic a distinction is (perhaps implicitly) made between the construction of terms with $+, \times$ and the computation done with such terms. Recipes for term construction are given in the signature, whereas computation is not specified until the relevant axioms are stated. In Lean these steps are brought together in a single function definition.

Peano arithmetic specifies the following axioms for computation with natural numbers. These provide a recursive definition for addition, by defining addition (on the right) by zero as the base case, and addition (on the right) by a successor as the inductive step.

Base case for addition

$\forall x : ℕ, (x + 0 = x)$

Recursive call for addition

$\forall x : ℕ, \ \forall y : ℕ, \ x + succ \ y = succ \ (x + y)$

These axioms are implemented by defining a recursive function using pattern matching on the second argument, following the pattern matching in the statement of the axioms.

def add (m n : ℕ) : ℕ :=
  match n with
    | zero    => m
    | succ x  => succ (add m x)

In order to maintain readibility and familiar blackboard notation, one would like to write e.g. succ zero + zero instead of add (succ zero) zero. Happily, Lean allows for such uses of notation by using in-built typeclasses. By including the following two lines the type ℕ is made an instance of the typeclass Add so that Lean knows to use our function add in place of the infix + notation.

instance : Add ℕ where
  add := add

Simiarly, term creation and computation for multiplication are combined into a single step. With the pattern matching in function definition following the pattern matching in the statement of the axioms.

Base case for multiplication

$\forall x : ℕ, \ x \times 0 = 0$

Recursive call for multiplication

$\forall x : ℕ, \ \forall y : ℕ, \ x \times (succ \ y) = (x \times y) + x$

def mul (m n : ℕ) : ℕ :=
  match n with
    | zero    => zero
    | succ x  => (mul m x) + m

Typeclasses again allow for the use of infix * in place of prefix mul for multiplication. Infix × is already in use for the product type, so we are forced to use another symbol for multiplication.

instance : HMul ℕ ℕ ℕ where
  hMul := mul

Definition, Axiom, or Theorem?

As with the first two axioms of Peano arithmetic, our approach has somewhat hidden the axioms controlling addition and multiplication. We may now bring these out explicitly as theorems about these functions.

 theorem add_zero :
  ∀ x : ℕ, x + zero = x :=
    by
      intro x
      rfl

 theorem add_succ :
  ∀ x y : ℕ, x + succ y = succ (x + y) :=
    by
      intro x y
      rfl

 theorem mul_zero :
  ∀ x : ℕ, x * zero = zero :=
    by
      intro x
      rfl

 theorem mul_succ :
  ∀ x y : ℕ, x * succ y = x * y + x :=
  by
    intro x y
    rfl

Each of these proofs have the same structure. We say “Let x (and y) be an arbitrary (pair of) natural number(s)…” and then provide a proof that the identities hold. This proof comes by way of the tactic rfl which can be read as “this equation is true by definition”. Perhaps more accurately, this identity holds by “merely carrying out the computation”. Unfold the terms according to the definitions of addition and multiplication and the two sides of the equation will be seen to be exactly the same, and hence by reflexivity of equality, the identity holds.

Again, despite prior warnings, the proof-terms for these theorems are relatively small and easy to write directly. For example, here is the proof-term for add_zero

theorem add_zero : ∀ (x : ℕ), x + zero = x :=
λ x => Eq.refl (x + zero)

In the next entry on induction we will begin to see the utility of meta-programs for authoring proofs. Those one would not want to write explicitly.

Mere Computation v. Induction

While some theorems are proved by merely carrying out computation. Other theorems require more to prove them. For example, computation alone does not prove the following theorem about addition:

 theorem zero_add :
  ∀ x : ℕ, zero + x = x :=
    by
      intro x
      rfl     -- Type mismatch error!

Look carefully, this is different to the theorem above! Here we have zero on the left of an addition, whereas addition is defined by pattern matching on the right hand variable. “Come on! Addition is commutative, what is going on!?” Yes, addition is commutative, but that is a theorem to be proven later. Mere computation does not provide any help here, because we don’t know whether x is zero, or a successor.

What is required is to consider both the cases that x = 0 and x = succ y for some natural number y, then tie these together using induction to prove the theorem. Induction is the final first-order axiom (schema) of Peano arithmetic which will be covered in the next entry of Babel.

Acknowledgments and Code

I came to terms with this content by playing the Natural Number Game, read Theorem Proving in Lean 4, browsing Mathlib, and asking questions on Proof Assistants Stack Exchange. Thank you to everyone involved in each of those projects.

All of the code covered in this entry of Babel can be found here on my GitHub account.