Axiomatic definition of the natural numbers

Stream: Is there code for X?

[shortc1rcuit]

I'm learning about the Peano Axioms and I wanted to see if I could create a version of them in Lean. I know you can also do it using inductive but how would I define the natural numbers like this?
image.png

[Joël Riou]

In Lean, the natural numbers are defined like this:

inductive Nat where
  | zero : Nat
  | succ (n : Nat) : Nat

Then axioms 1/2/3 are true almost by construction, and 4 can be shown by induction (induction tactic).

(Note that the Peano axioms are not a definition of ℕ: these are axioms)

[Eric Rodriguez]

Joel, they're asking if it's possible to define them from the axioms - they seem to understand that it is possible with an inductive type already.

[Joël Riou]

(I have added a note accordingly.)

[Joël Riou]

It is certainly possible to formulate that a Type N equipped with 0 : N and succ : N → N satisfy the Peano axioms. We know that Lean's Nat (ie. ℕ) satisfy these. Then, the interesting question is, can you show that there is a bijection ℕ ≃ N that is compatible with the zero and the successor?

[Kevin Buzzard]

Defining them via axioms would not be idiomatic Lean (in mathlib there are no axioms at all), but there's nothing stopping you writing down constant N : Type, constant one : N , axiom ind : \forall S : Set N... etc.

[Adam Topaz]

You could also do something like this:

class IsPeanoNat (X : Type*) extends Zero X where
  succ : X → X
  succ_inj : ∀ {x y : X}, succ x = succ y → x = y
  succ_ne_zero : ∀ x : X, succ x ≠ zero
  induction : ∀ {motive : X → Prop} (x : X), motive zero → (∀ x, motive x → motive (succ x)) → motive x

[Kevin Buzzard]

s/zero/one

[Kevin Buzzard]

(the source seems to be using the British Natural Numbers)

[shortc1rcuit]

Adam Topaz said:

You could also do something like this:

class IsPeanoNat (X : Type*) extends Zero X where
  succ : X → X
  succ_inj : ∀ {x y : X}, succ x = succ y → x = y
  succ_ne_zero : ∀ x : X, succ x ≠ zero
  induction : ∀ {motive : X → Prop} (x : X), motive zero → (∀ x, motive x → motive (succ x)) → motive x

Yeah I was thinking of using something like that but then it might get difficult later on when I'm trying to contruct the integers from the naturals

[Kevin Buzzard]

Your principle of recursion wouldn't be computable but I don't see why it would be hard to define the integers.

[shortc1rcuit]

That might just be a case of me not knowing enough about Lean

[Joël Riou]

It depends on how you want to define the type of integers ℤ. In Lean/mathlib it is defined in a quite interesting way: an element of ℤ is either "+n" for some n : ℕ or "-(1+n)" for some n : ℕ. You could certainly do the same using the IsPeanoNat X definition.

However, if you want to define ℤ as equivalence classes of formal differences "x - y" with x and y in X, you need to know a few things about the addition on X. For that: you would obviously need to have a definition of the addition on X. In Lean, it is easy to define the addition ℕ → ℕ → ℕ using a native Lean inductive definition, but it is not clear to me how we would define the addition X → X → X using only [IsPeanoNat X].

[Ruben Van de Velde]

It seems like the induction (or "recursion") field needs to support eliminating into Sort*

[Timo Carlin-Burns]

or IsPeanoNat could include a field for an addition function and some axioms describing it

[Timo Carlin-Burns]

including a recursion principle which could be used to construct data would look something like this

universe u v

class IsPeanoNat (X : Type u) extends Zero X where
  succ : X → X
  succ_inj : ∀ {x y : X}, succ x = succ y → x = y
  succ_ne_zero : ∀ x : X, succ x ≠ zero
  recursion : ∀ {motive : X → Sort v} (x : X), motive zero → (∀ x, motive x → motive (succ x)) → motive x
  rec_zero : ∀ {motive : X → Sort v} (z : motive zero) (step : ∀ x, motive x → motive (succ x)), recursion zero z step = z
  rec_succ : ∀ {motive : X → Sort v} (x : X) (z : motive zero) (step : ∀ x, motive x → motive (succ x)), recursion (succ x) z step = step x (recursion x z step)

but I think this runs into universe issues because the universe you can eliminate into, v, is fixed for a given IsPeanoNat instance

[Adam Topaz]

With the prop version you can construct a bijection from the usual Nat to X and use that to define a general recursion principle

[Kevin Buzzard]

Yes, but it would be noncomputable (not that this would matter) because to get the map from X to N+ you need to invert a bijection.

[Timo Carlin-Burns]

I suppose if you just want Peano Arithmetic, you only need to be able to use recursion to define natural number-valued functions:

class IsPeanoNat (X : Type u) extends Zero X where
  succ : X → X
  succ_inj : ∀ {x y : X}, succ x = succ y → x = y
  succ_ne_zero : ∀ x : X, succ x ≠ 0
  induction : ∀ {motive : X → Prop} (x : X), motive 0 → (∀ x, motive x → motive (succ x)) → motive x
  recursion (base : X) (step : X → X) : X → X
  rec_zero (base step) : recursion base step 0 = base
  rec_succ (base step x) : recursion base step (succ x) = step (recursion base step x)

[Adam Topaz]

If you want a computable recursor you can just eliminate into Type. That will let you define a computable equivalence with Nat, and you can get the general thing using that.

[Kevin Buzzard]

And if you allow the full recursor that lean's nat has them you don't need succ_inj and succ_ne_zero, you can prove them using pred and is_zero

[Trebor Huang]

Wouldn't this be actually too strong because motive can involve arbitrarily high order expressions instead of being restricted to first order predicates?

[Bulhwi Cha]

This is a very unidiomatic way to define the natural numbers in Lean:

import Mathlib.Data.Set.Basic

axiom N : Type
axiom succ : N → N
axiom one : N

noncomputable instance : OfNat N 1 where
  ofNat := one

#check (1 : N)

axiom one_ne_succ (n : N) : 1 ≠ succ n
axiom succ_inj (a b : N) : succ a = succ b → a = b
axiom induction (S : Set N) (h1 : 1 ∈ S) (ih : ∀ k ∈ S, succ k ∈ S) : S = N

Correction: S = N in the axiom induction should be S = ⊤, where ⊤ is @Set.univ (Set N).

Corrected axioms

import Mathlib.Data.Set.Basic

axiom N : Type
axiom succ : N → N
axiom one : N

noncomputable instance : OfNat N 1 where
  ofNat := one

#check (1 : N)

axiom one_ne_succ (n : N) : 1 ≠ succ n
axiom succ_inj (a b : N) : succ a = succ b → a = b
axiom induction (S : Set N) (h1 : 1 ∈ S) (ih : ∀ k ∈ S, succ k ∈ S) : S = ⊤

[shortc1rcuit]

So far I've done this

import Mathlib.Data.Set.Basic

class IsPeanoNat (N : Type) where
  succ : N → N
  one : N
  one_ne_succ : ∀ x : N, succ x ≠ one
  succ_inj : ∀ x y : N, succ x = succ y ↔ x = y
  induction (S : Set N) (h1 : one ∈ S) (ih : ∀ k ∈ S, succ k ∈ S) : S = N

theorem prop_induction [IsPeanoNat N] (P : N → Prop) (h_one: P one) (h_succ: ∀ k, P k ⇒ P (succ k)): ∀ n, P n :=
  sorry

But h_succ seems to be incorrect in some way.
image.png
What am I doing wrong?

[Adam Topaz]

Your induction field shouldn’t type check

[Kevin Buzzard]

Lean for "implies" is \to not (whatever symbol you have used there). And you need to open IsPeanoNat to ensure that succ means the succ in your class.

[Kevin Buzzard]

import Mathlib.Data.Set.Basic

class IsPeanoNat (N : Type) where
  succ : N → N
  one : N
  one_ne_succ : ∀ x : N, succ x ≠ one
  succ_inj : ∀ x y : N, succ x = succ y ↔ x = y
  induction (S : Set N) (h1 : one ∈ S) (ih : ∀ k ∈ S, succ k ∈ S) : S = N

open IsPeanoNat

theorem prop_induction [IsPeanoNat N] (P : N → Prop) (h_one: P one)
    (h_succ: ∀ k : N, P k → P (succ k)): ∀ n, P n :=
  sorry

[Kevin Buzzard]

Oh and S = N is not correct (I think this is what Adam was getting at). Equality of types is not a thing. You mean S = ⊤, the "top subset of N". S is a subset, not a type itself.

[Kevin Buzzard]

import Mathlib.Data.Set.Basic

class IsPeanoNat (N : Type) where
  succ : N → N
  one : N
  one_ne_succ : ∀ x : N, succ x ≠ one
  succ_inj : ∀ x y : N, succ x = succ y ↔ x = y
  induction (S : Set N) (h1 : one ∈ S) (ih : ∀ k ∈ S, succ k ∈ S) : S = ⊤

open IsPeanoNat

theorem prop_induction [IsPeanoNat N] (P : N → Prop) (h_one: P one)
    (h_succ: ∀ k : N, P k → P (succ k)): ∀ n, P n := by

my solution

  intro n
  change n ∈ {x | P x}
  rw [induction {x | P x} h_one h_succ]
  trivial

[shortc1rcuit]

Cool.
Now to somehow define addition.
I'm assuming just using inductive won't work.
If there's a need for a proof that addition is defined for all inputs then I have one of those.

[Kevin Buzzard]

Right, you have not got a recursion axiom so you will need to transport to a type with a recursion axiom like Lean's inductively defined nat. This is one of the reasons why what you're trying to do is so painful.

[Kevin Buzzard]

import Mathlib.Data.Set.Basic

class IsPeanoNat (N : Type) where
  succ : N → N
  one : N
  one_ne_succ : ∀ x : N, succ x ≠ one
  succ_inj : ∀ x y : N, succ x = succ y ↔ x = y
  induction (S : Set N) (h1 : one ∈ S) (ih : ∀ k ∈ S, succ k ∈ S) : S = ⊤

namespace IsPeanoNat

variable {N : Type} [IsPeanoNat N]

def ofNat : Nat → N
| 0 => one
| (Nat.succ n) => succ (ofNat n)

lemma ofNat_surjective : {x : N | ∃ m : Nat, ofNat m = x} = ⊤ := by
  refine induction _ ?_ ?_
  · use 0
    rfl
  · rintro k ⟨m, rfl⟩
    use m.succ
    rfl

lemma ofNat_surjective' (x : N) : ∃ m : Nat, ofNat m = x := by
  change x ∈ {x | ∃ m, ofNat m = x}
  rw [ofNat_surjective]
  trivial

noncomputable def toNat (x : N) : Nat := (ofNat_surjective' x).choose

noncomputable def add (x y : N) : N := ofNat (toNat x + toNat y + 1) -- + 1 because you started at 1

Now it will be a pain proving anything about add -- first you'll have to prove ofNat is bijective and toNat is the two-sided inverse. But then all your theorems about add will just be immediately derivable from Nat.add. This is just an awful way to do it. If you want to do it this way you should at least give yourself recursion as an axiom, but even then you won't be able to benefit from Lean's inbuilt support for recursors for inductive types (e.g. what I used for the definition of ofNat).

[shortc1rcuit]

Yeah I see your point.
I might just put in my document "from now on we'll use the normal lean definition of Nat to simplify things", and continue from there. I don't think I'll need anything else from the original rules.