Peano axioms

Stream: new members

[KK]

I am just playing around with Lean. I wrote this, but I have no clue what is wrong.

inductive natural : Type
| zero : natural
| succ : natural → natural
| add : natural → natural → natural
| mul : natural → natural → natural

open natural
namespace natural

axiom add_zero {a : natural} : (add a zero) = a
axiom add_succ {a b : natural} : add a (succ b) = succ (add a b)

lemma zero_add (n : natural) : add zero n = n :=
begin
  induction n with i hi,
  rw add_zero,
  rw add_succ,
  rw hi,
end

[Ruben Van de Velde]

Well, what is wrong?

[KK]

tactic failed, there are unsolved goals
state:
2 goals
case natural.add
n_ᾰ n_ᾰ_1 : natural,
n_ih_ᾰ : zero.add n_ᾰ = n_ᾰ,
n_ih_ᾰ_1 : zero.add n_ᾰ_1 = n_ᾰ_1
⊢ zero.add (n_ᾰ.add n_ᾰ_1) = n_ᾰ.add n_ᾰ_1

case natural.mul
n_ᾰ n_ᾰ_1 : natural,
n_ih_ᾰ : zero.add n_ᾰ = n_ᾰ,
n_ih_ᾰ_1 : zero.add n_ᾰ_1 = n_ᾰ_1
⊢ zero.add (n_ᾰ.mul n_ᾰ_1) = n_ᾰ.mul n_ᾰ_1

[KK]

and an error at the end:

invalid end of module, expecting 'end'

[Ruben Van de Velde]

The second one is easy: you need to close the namespace with end natural

[Ruben Van de Velde]

The first one is because inductive types don't work like that - in fact, your axioms are inconsistent.

example : false :=
begin
  have := @add_zero zero,
  injection this,
end

[Ruben Van de Velde]

Your code says that the numbers created by add expressions are distinct from the ones created by zero or succ

[KK]

I figured that add and mul should not be part of the natural type.

[Bolton Bailey]

Indeed the type you defined might be described as the type of expressions in Peano arithmetic.

[KK]

Is it possible to do something else than this:

inductive natural : Type
| zero : natural
| succ : natural → natural

open natural

definition add (m n : natural) : natural :=
  natural.rec_on n m (λ n e, succ e)

definition mul (m n : natural) : natural :=
  natural.rec_on n m (λ n e, succ e)

axiom add_zero {a : natural} : (add a zero) = a
axiom add_succ {a b : natural} : add a (succ b) = succ (add a b)
axiom mul_zero (a : natural) : mul a zero = zero
axiom mul_succ (a b : natural) : mul a (succ b) = add (mul a b) a

lemma zero_add (n : natural) : add zero n = n :=
begin
  induction n with i hi,
  rw add_zero,
  rw add_succ,
  rw hi,
end

lemma zero_mul (m : natural) : mul zero m = zero :=
begin
  induction m with i hd,
  rw mul_zero,
  rw mul_succ,
  rw hd,
  rw add_zero,
end

I mean avoiding the fact that add and mul are "functions".

[Bolton Bailey]

If you are asking if there's another way to define the naturals inductively, one thing you can do is the zero/bit0/bit1 definition, which essentially defines naturals as binary strings. This is convenient because it means you can represent large naturals efficiently. But I don't think there's any way to have succ be one of the constructors without doing this exact definition.

[KK]

I did not mean that. Also, it would still require functions add and mul. I would like to work directly on Peano arithmetic expressions, where add and mul do not have a special function type (if this even makes sense).

[Eric Rodriguez]

I'm confused what you mean about add and mul being functions. They are also functions in peano arithmetic..

[KK]

Fair enough, thank you everyone.

[Junyan Xu]

Maybe you are looking for something like this and this

[KK]

Nice find.

[Junyan Xu]

Flypitch is probably the largest project on mathematical logic / model theory so far in Lean, so I'd always look there when people ask questions in these areas. Some of flypitch is slowly being moved to mathlib.