kuniga.me > NP-Incompleteness > Peano's Axioms in Lean
Peano's Axioms in Lean
26 Jan 2022
Giuseppe Peano was a Italian mathematician who also studied historical linguistics. Peano is known for a defining a set of axioms from which many properties about natural numbers can be derived. Peano’s work was built on Hermann Grassmann, Charles Sanders Peirce and Richard Dedekind.
In this post we’ll explore some of Giuseppe Peano’s axioms and derive lemmas from them. The goal of this post is to provide a practical introduction to Lean without getting too specific on the details.
This post borrows heavily on Kevin Buzzard’s Natural Number Game [1] which I highly recommend! It has been tested on Lean 3.38 (community fork). One of the easiest ways to play with Lean is using the online editor, to which you can paste the code from the post as we go along.
The Natural Numbers
The first thing we have to do is define the natural numbers.
namespace sandbox
inductive Nat
| zero : Nat
| succ (n : Nat) : Nat
open Nat
end sandboxIn Lean the syntax inductive Nat describe a inductive type, and according to [5]:
Intuitively, an inductive type is built up from a specified list of constructors
If you’re familiar with Haskell, this is similar to the concept of recursive data types.
To reference the constructors zero and succ, we need to qualify them with Nat: Nat.zero and Nat.succ. The open Nat line “imports” definitions from Nat, so we can refer to zero and succ directly.
In Lean you can create named scopes by wrapping the code within:
namespace my_name
-- code
end my_nameIf you’re familiar with C++, this is very similar to C++ namespaces. The reason to create a new scope here is that Nat is already defined and included (in the prelude library), so if we want to reuse that name it has to be inside a scope.
Alternatively we could name is something else, like my_nat.
Peano Axioms
Axiom 1. The constant 0 is a natural number.
The first axiom states that the constant 0 is a natural number. This is implicit in the fact that zero is a constructor for Nat.
For convenience we can also associate Nat.zero with the symbol 0:
instance : has_zero Nat := ⟨zero⟩Note that ⟨zero⟩ is not parenthesis but angle brackets (unicodes: U+27E8, U+27E9)! The has_zero is a known as a typeclass, which in OOP roughly maps to an interface with the method has_zero that must be implemented by classes, Nat in this case.
If you’re familiar with Haskell, you might have seen typeclasses before.
Equality Relations
This set of axioms establish the properties of the $=$ operator. According to Wikipedia [2]:
Since they are logically valid in first-order logic with equality, they are not considered to be part of “the Peano axioms” in modern treatments.
In fact, Lean incorporate these axioms in its $=$ operator but we’ll discuss them for completeness.
Axiom 2. For every natural number $x$, $x = x$.
Lean already has the so-called tactic [4] refl which is short for reflexivity, so we don’t need to define this explicitly, but this is how we could have done it:
axiom reflexivity (n : Nat) : n = nAxiom 3. For all natural numbers $x$ and $y$, if $x = y$, then $y = x$.
Lean has a tactic called symmetry that encodes this axiom. This is one way we can express it otherwise:
axiom symmetry (n m: Nat) : n = m <-> m = nHere the <-> represents “if and only if”.
Axiom 4. For all natural numbers $x$, $y$ and $z$, if $x = y$ and $y = z$, then $x = z$.
The corresponding tactic in Lean is transitivity, which we can define as:
axiom trans (a b c: Nat) : a = b ∧ b = c -> a = cHere the ∧ represents and. The -> means “implies”.
Axiom 5. For all $a$ and $b$, if $b$ is a natural number and $a = b$, then $a$ is also a natural number.
I don’t really know how to express this as a Lean axiom, but my hunch is that Lean’s type system implicitly incorporates this since both sides of = must have the same type. For example, if we try to write a axiom starting from instances of different types being equal:
inductive Unnat
axiom nope (a: Nat) (b: Unnat) : a = bLean will throw an error:
type mismatch at application
a = b
term
b
has type
Unnat
but is expected to have type
NatArithmetical Properties
Axiom 6. For every natural number $n$, $S(n)$ is a natural number.
Like Axiom 1, this is implicit in the fact that succ (n : Nat) : Nat is a constructor for Nat.
Axiom 7. For all natural numbers $m$ and $n$, $m = n$ if and only if $S(m) = S(n)$.
This says that a natural number cannot have multiple successors nor can it be the successor of multiple numbers.
axiom injection (m n: Nat) : m = n <-> succ(m) = succ(n)Axiom 8. For every natural number $n$, $S(n) = 0$ is false.
This means that 0 is not the successor of any other number or $S(n) \neq 0$.
axiom non_zero_succ (n : Nat) : succ(n) = 0 -> falseRecall that if we have an implication $P \implies Q$, for it to be valid either $P$ must be false or both $P$ and $Q$ must be true. Thus if we “hard-code” $Q$ as false like above, $P$ is also false and it must be that $succ(n) \neq 0$.
Axiom 9. Let $K$ be a set such that: $0 \in K$ and for every natural number $n$, if $n \in K$ then $S(n) \in K$. Then $K$ contains every natural number.
The axioms up to Axiom 8 only described things that are naturals numbers but did not say anything about things that are not.
For example, if we take the set of numbers $\mathbb{N} = \curly{0, 1, \cdots}$ and union with the set $\curly{0.5, 1.5, 2.5, \cdots}$, we’ll see that they satisfy all the axioms above, including Axiom 6, for which we can think of two lines of succession, one starting from 0 and one starting from 0.5.
If we include Axiom 9 however, we’ll see that $\mathbb{N}$ is a possible candidate for $K$, and thus $\mathbb{N}$ contains all natural numbers, meaning that $\curly{0.5, 1.5, 2.5, \cdots}$ are not in it.
Maybe a more intuitive way to phrase this axiom is that the set of natural numbers is the smallest set such that its elements satisfy Axioms 1-8. But this relies on being able to compare sizes of infinite sets which doesn’t seem like a good idea for an axiom.
Addition Axioms
We can define the add as a recursive function:
def add : Nat → Nat → Nat
| m 0 := m
| m (succ n) := succ (m + n)Note how we only use the available constructors from Nat and rely on pattern matching to “extract” the n from (succ n). For convenience, we can implement the has_add typeclass so the operator + maps to add.
instance : has_add Nat := ⟨add⟩We need to encode the definitions in add as axioms so that we can explicitly use them when writing proofs.
Axiom 10. For every natural number $n$, $n + 0 = n$.
In other words, it says $0$ is the identity element for sum. But it’s worth noting this is only when $0$ is on the right-hand side of $+$. We haven’t proved commutativity yet. This encodes the first constructor of add.
axiom add_zero (n : Nat) : n + 0 = nAxiom 11. For all natural numbers $m$ and $n$, $m + S(n) = S(m + n)$.
This seems like a useless rewrite at first but because we’re “extracting” $n$ from $S(n)$, we can rely on the inductive nature of Nat and assume that function m + n is defined. This encodes the second constructor of add.
axiom add_succ (m n: Nat) : m + succ n = succ (m + n)We’re not finally able to write out first Lemma!
Lemma 1. For all natural numbers $a, b$ and $c$, $(a + b) + c = a + (b + c)$.
In other words, that addition is associative. We can prove this by induction on $c$.
axiom zero_is_nat : zero = 0
lemma add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) :=
begin
induction c with d hd,
-- base
rw zero_is_nat,
repeat {rw add_zero},
-- inductive step
repeat {rw add_succ},
rw hd,
endThe lemma looks a lot like a axiom, but this time we need to prove it by providing the “implementation” to the right of the := operator.
The general idea of proving a lemma consists in achieving a goal. We initially start with a single goal which is to prove the original lemma but we can use constructs known as tactics to help us which might end up splitting the goal into multiple ones as we’ll see next.
Let’s analyze some of the lines. Ignore axiom zero_is_nat for now, we’ll get back to it soon.
First, consider induction c with d hd. This will split the lemma into two goals: one where c is replaced with zero (base) and another where c is replaced with succ(d) but we’ll have the inductive hypothesis hd which we assume is true for a, b, d, that is (a + b) + d = a + (b + d).
Let’s consider the base case. We need to show that (a + b) + zero = a + (b + zero). The unfortunate thing is that the induction tactic doesn’t seem to understand that Nat.zero = 0 even though we implemented has_zero [3], so we need to define the zero_is_nat axiom to make this explicit.
The rw is a short for rewrite and the way it works is as follows:
- You give an axiom/lemma that states an equality of the form
expr1 = expr2. - It will try to find the first expression that matches
expr1 - It will replace that expression everywhere in the current state.
In our example, we start with (a + b) + zero = a + (b + zero). By applying rw zero_is_nat we get (a + b) + 0 = a + (b + 0). Note that it replaced both zeros with 0, because they’re the same expression.
Now we rewrite using add_zero. If we do rw add_zero we’ll not have (a + b) = a + (b + 0). Note that it’s smart to match (a + b) + 0 because it knows (a + b) is Nat. Note also that it didn’t replace (b + 0) because it’s a different expression than the first match (a + b) + 0.
This subtle behavior is confusing, but this answer clarifies things.
We need to then apply rw add_zero again. There’s a shorthand for “apply X while there’s a match”, which is repeat {X}, and it is what we use in: repeat {rw add_zero}. This will get us to a + b = a + b and since equality is reflexive, Lean will consider this proved.
Now to the induction step. We have (a + b) + succ(d) = a + (b + succ(d)). By applying rw add_succ we get succ(a + b + d) = a + (b + succ(d)) and applying once more we get succ(a + b + d) = a + (succ(b + d)) and then succ((a + b) + d) = succ(a + (b + d)).
The (a + b) + d is in the form of our inductive hypothesis so we can use it rw hd to obtain succ(a + (b + d)) = succ(a + (b + d)), which proves the second goal.
Multiplication Axioms
We can define the mul as a recursive function:
def mul : Nat → Nat → Nat
| m 0 := 0
| m (succ n) := m + (mul m n)For convenience, we can implement the has_mul typeclass so the operator * maps to mul.
instance : has_mul Nat := ⟨mul⟩Axiom 12. For every natural number $n$, $n * 0 = 0$.
It’s worth noting this is only when $0$ is on the right-hand side of $+$. We haven’t proved commutativity yet. This encodes the first constructor of mul.
axiom mul_zero (m : Nat) : m * 0 = 0Axiom 13. For all natural numbers $m$ and $n$, $m S(n) = m + mn$.
As it was the case with add we’re “extracting” $n$ from $S(n)$, so we can rely on the inductive nature of Nat and assume that function mn is defined. This encodes the second constructor of mul.
axiom mul_succ (m n: Nat) : m * (succ n) = m + m * nWe won’t overextend the post with other proofs besides that of Lemma 1, but with these axioms it’s possible to show for example that addition is commutative and multiplication is associative and commutative.
The code is available on Github.
Conclusion
In this post we covered basic aspects of the Lean language and revisited the Peano axioms.
My initial plan was to write this in Lean 4, which is in active development by Microsoft. I started reading the tutorial but got lost quickly and wasn’t finding the abstract examples intuitive.
I decided to try The Natural Number Game [1] which is a much more friendly introduction and suitable for people who are not familiar with formal methods. There are a couple of quirks from the language that the game hides from us to make it easier, and I only ran into them while trying to write a standalone version.
The Natural Number Game uses Lean 3.38 which is incompatible with Lean 4 as I quickly learned. It seems like the community fork is much more active and there are a lot more resources so I’ll stick with it for now.
Overall I was very happy to finally write some proofs using a theorem prover. I had tried Agda before but I ended up dropping the ball for some reason. I keep hearing about Lean and the Xena project and that encourage me to try theorem provers again. I’m really hoping to stick with learning more about it this time.
Related Posts
An Introduction to Agda was my previous attempt at getting started with theorem proving. At first glance Agda and Lean look similar in syntax and both are functional languages based on dependent types. Lean seems to have a more thriving community, better tooling and interestingly a big company (Microsoft) doing active development on it.
