axiomatize natural numbers

Stream: new members

[Yusuke Inoue]

I tried to define a type class to represent Peano axioms.

class PeanoAxioms (N : Type) extends Zero N where
  succ : N -> N
  zeroNoSucc : ∀n : N, ¬ succ n = 0
  succCancel : ∀a b : N, succ a = succ b → a = b
  induction : ∀f : N → Sort*, f 0 → (∀n : N, f n → f (succ n)) → ∀n : N, f n

postfix:100 "++" => PeanoAxioms.succ

I use Sort* here because (at least so far) I don't think proof irrelevance is a good idea.

However, it seems that computing on the abstract natural numbers is impossible (take the following as an example).

namespace PeanoAxioms

variable {N : Type}[PeanoAxioms N]

theorem conv0 {f : N → Sort*} (base : f 0) (succ : ∀n : N, f n → f (n++)) : induction f base succ 0 = base := by sorry

But for any instance of the type class, the computing process seems always possible.

What's wrong?

[Kenny Lau]

It's working as intended :upside_down:

When you axiomatise something you're just requiring a type (+structure) to satisfy those extra rules. there's certainly no requirements that those equalities should be defeq.

Maybe this is where your confusion is. Lean's defeq is not mathematician's defeq!

[Kenny Lau]

btw please add import Mathlib so that your code compiles; and actually I'm confused here, what do you mean that it's impossible? you just added by sorry to your code, I don't know what that's supposed to mean.

[Kenny Lau]

Can you explain what you mean by "impossible"?

[Yusuke Inoue]

Kenny Lau said:

btw please add import Mathlib so that your code compiles; and actually I'm confused here, what do you mean that it's impossible? you just added by sorry to your code, I don't know what that's supposed to mean.

Thanks for your advice! I use 'by sorry' just as a placeholder here :).

[Kenny Lau]

yes, but what do you mean by "impossible"?

[Kenny Lau]

oh, now I understand

[Kenny Lau]

yeah there's certainly nothing in your axioms saying that the induction has to produce what you think it would produce!

[Kenny Lau]

I can certainly build a function that swaps the output for 0 and 1 and it will still satisfy your axioms!

[Jz Pan]

Kenny Lau said:

I can certainly build a function that swaps the output for 0 and 1 and it will still satisfy your axioms!

Or constant function

[Yusuke Inoue]

I think any instance that satisfies the axioms has to use something derived from the type's recursor or something like that to satisfy 'induction'.

[Yusuke Inoue]

and that makes computing possible

[Yusuke Inoue]

I guess maybe in meta language can prove 'for all N : Type , PeanoAxioms N -> conv0', but conv0 cannot be proved in Lean itself

[Aaron Liu]

It's actually inconsistent with the axiom of choice:

import Mathlib

class PeanoAxioms (N : Type) extends Zero N where
  succ : N -> N
  zeroNoSucc : ∀n : N, ¬ succ n = 0
  succCancel : ∀a b : N, succ a = succ b → a = b
  induction : ∀f : N → Sort*, f 0 → (∀n : N, f n → f (succ n)) → ∀n : N, f n

postfix:100 "++" => PeanoAxioms.succ

namespace PeanoAxioms

variable {N : Type}[PeanoAxioms N]

theorem conv0 {f : N → Sort*} (base : f 0) (succ : ∀n : N, f n → f (n++)) : induction f base succ 0 = base := by sorry

example : False := by
  have := @conv0 Nat {
    zero := Nat.zero
    succ := Nat.succ
    zeroNoSucc := Nat.succ_ne_zero
    succCancel := @Nat.succ.inj
    induction f z s n := by classical exact if hf : f = fun _ => Bool then hf ▸ false else @Nat.rec f z s n
  } (fun _ => Bool) true fun _ _ => true
  simp at this

[Kenny Lau]

Yusuke Inoue said:

I guess maybe in meta language can prove 'for all N : Type , PeanoAxioms N -> conv0', but conv0 cannot be proved in Lean itself

yes, that's a meta theorem, so not a theorem

[Kenny Lau]

for your purposes I think you should instead make conv0 and conv_succ part of the axioms

[Aaron Liu]

I think you can still computably derive an induction' that has the same signature but also additionally satisfies conv0 and conv_succ

[Kenny Lau]

In that case please swap the names, induction' for the provided one and induction for the derived one

[Yusuke Inoue]

Aaron Liu said:

I think you can still computably derive an induction' that has the same signature but also additionally satisfies conv0 and conv_succ

Could you please make it clearer? I'm afraid I can't fully understand.

[Aaron Liu]

import Mathlib

class PeanoAxioms (N : Type) extends Zero N where
  succ : N -> N
  zeroNoSucc : ∀n : N, ¬ succ n = 0
  succCancel : ∀a b : N, succ a = succ b → a = b
  induction' : ∀f : N → Sort*, f 0 → (∀n : N, f n → f (succ n)) → ∀n : N, f n

namespace PeanoAxioms
variable {N : Type} [PeanoAxioms N]

scoped postfix:100 "++" => PeanoAxioms.succ

variable (N) in
def ofNat (n : Nat) : N :=
  match n with
  | 0 => 0
  | n + 1 => (ofNat n)++

instance decEq (n m : N) : Decidable (n = m) :=
  induction' (fun k => ∀ j, Decidable (j = k))
    (induction' (fun j => Decidable (j = _)) (.isTrue rfl) (fun j _ => .isFalse (zeroNoSucc j)))
    (fun k _ => induction' (fun j => Decidable (j = _)) (.isFalse (Ne.symm (zeroNoSucc k)))
      (fun j _ => decidable_of_iff (j = k) ⟨congrArg (·++), succCancel j k⟩)) m n

variable (N) in
theorem ofNat_injective : (ofNat N).Injective := sorry

variable (N) in
theorem ofNat_surjective : (ofNat N).Surjective := sorry

def toNat (n : N) := Nat.find (p := fun c => ofNat N c = n) (ofNat_surjective N n)

def induction (f : N → Sort*) (zero : f 0) (succ : ∀ n, f n → f (succ n)) (n : N) : f n := sorry

def cov0 (f : N → Sort*) (zero : f 0) (succ : ∀ n, f n → f (succ n)): induction f zero succ 0 = zero := sorry

def cov_succ (f : N → Sort*) (zero : f 0) (succ : ∀ n, f n → f (succ n)) (n : N) : induction f zero succ (n++) = succ n (induction f zero succ n) := sorry

end PeanoAxioms

[Kenny Lau]

induction' should have @[elab_as_elim] (and implicit motive) so you don't need to specify the motive explicitly

[Kenny Lau]

@Yusuke Inoue in words, see how induction above is derived from the axiom induction' and satisfies the conv lemmas you wanted

[Jz Pan]

Aaron Liu said:

It's actually inconsistent with the axiom of choice:

import Mathlib

class PeanoAxioms (N : Type) extends Zero N where
  succ : N -> N
  zeroNoSucc : ∀n : N, ¬ succ n = 0
  succCancel : ∀a b : N, succ a = succ b → a = b
  induction : ∀f : N → Sort*, f 0 → (∀n : N, f n → f (succ n)) → ∀n : N, f n

postfix:100 "++" => PeanoAxioms.succ

namespace PeanoAxioms

variable {N : Type}[PeanoAxioms N]

theorem conv0 {f : N → Sort*} (base : f 0) (succ : ∀n : N, f n → f (n++)) : induction f base succ 0 = base := by sorry

example : False := by
  have := @conv0 Nat {
    zero := Nat.zero
    succ := Nat.succ
    zeroNoSucc := Nat.succ_ne_zero
    succCancel := @Nat.succ.inj
    induction f z s n := by classical exact if hf : f = fun _ => Bool then hf ▸ false else @Nat.rec f z s n
  } (fun _ => Bool) true fun _ _ => true
  simp at this

Because conv0 is not necessarily true for general; it should be a field of PeanoAxioms, as well as conv_succ

[Kenny Lau]

@Jz Pan see alternative route above

[Jz Pan]

Oh amazing. I haven't realized that DecidableEq can be obtained.

[Aaron Liu]

You do get induction, after all. It's just that you don't get any computational properties, but that is irrelevant here since Decidable is a subsingleton.

[Aaron Liu]

although maybe making it an instance isn't the best idea if we also want a PeanoAxioms Nat

[Kenny Lau]

you might as well state N \~- \N as the only axiom

[Kenny Lau]

or better, use actual model theory :upside_down:

[Kenny Lau]

(these aren't constructive feedbacks, please ignore)

[Jz Pan]

What I've tried is at here #general > Lean companion to "Analysis I" - discussion @ 💬 and I've got everything if assuming DecidableEq

[Yusuke Inoue]

Aaron Liu said:

import Mathlib

class PeanoAxioms (N : Type) extends Zero N where
  succ : N -> N
  zeroNoSucc : ∀n : N, ¬ succ n = 0
  succCancel : ∀a b : N, succ a = succ b → a = b
  induction' : ∀f : N → Sort*, f 0 → (∀n : N, f n → f (succ n)) → ∀n : N, f n

namespace PeanoAxioms
variable {N : Type} [PeanoAxioms N]

scoped postfix:100 "++" => PeanoAxioms.succ

variable (N) in
def ofNat (n : Nat) : N :=
  match n with
  | 0 => 0
  | n + 1 => (ofNat n)++

instance decEq (n m : N) : Decidable (n = m) :=
  induction' (fun k => ∀ j, Decidable (j = k))
    (induction' (fun j => Decidable (j = _)) (.isTrue rfl) (fun j _ => .isFalse (zeroNoSucc j)))
    (fun k _ => induction' (fun j => Decidable (j = _)) (.isFalse (Ne.symm (zeroNoSucc k)))
      (fun j _ => decidable_of_iff (j = k) ⟨congrArg (·++), succCancel j k⟩)) m n

variable (N) in
theorem ofNat_injective : (ofNat N).Injective := sorry

variable (N) in
theorem ofNat_surjective : (ofNat N).Surjective := sorry

def toNat (n : N) := Nat.find (p := fun c => ofNat N c = n) (ofNat_surjective N n)

def induction (f : N → Sort*) (zero : f 0) (succ : ∀ n, f n → f (succ n)) (n : N) : f n := sorry

def cov0 (f : N → Sort*) (zero : f 0) (succ : ∀ n, f n → f (succ n)): induction f zero succ 0 = zero := sorry

def cov_succ (f : N → Sort*) (zero : f 0) (succ : ∀ n, f n → f (succ n)) (n : N) : induction f zero succ (n++) = succ n (induction f zero succ n) := sorry

end PeanoAxioms

Wait. If we could prove cov0 here, then we could get False from it as above. However, there are no 'unsafe' operations (like introducing axioms). So maybe it's impossible.
Sorry, I've got something wrong.

[Yusuke Inoue]

I think it's interesting. Types that satisfy the Peano axioms are isomorphic, but they do not have to have the expected computing behaviours. The isomorphism could be used to select a 'standard' way of computing.
Could it be understood as follows: in type theory, proofs can be taken into consideration, but the Peano axioms said nothing about proofs and do not require a standard way of computing proofs.

[Kenny Lau]

Yusuke Inoue said:

Peano axioms said nothing about proofs

The induction in the Peano axioms is about Props, not eliminating to data