Expressing PA in Lean

Stream: general

[Daniel Weber]

Daniel Weber said:

I'm not quite sure what you mean by expressing a theory in Lean

What would expressing PA mean, for instance?

axiom N : Type
axiom zero : N
axiom succ : N → N
axiom add : N → N → N
axiom mul : N → N → N
axiom succ_ne_zero : ∀ x : N, zero ≠ succ x
axiom succ_inj : ∀ x y : N, succ x = succ y → x = y
axiom add_zero : ∀ x : N, add x zero = x
axiom add_succ : ∀ x y : N, add x (succ y) = succ (add x y)
axiom mul_zero : ∀ x : N, mul x zero = zero
axiom mul_succ : ∀ x y : N, mul x (succ y) = add (mul x y) x
axiom induction : ∀ p : N → Prop, (p zero ∧ ∀ x : N, p x → p (succ x)) → ∀ x : N, p x

Is this an expression?

[Daniel Weber]

I'm quite certain this is stronger than PA, i.e. there are theorems which are true on this N but aren't provable in PA

[Martin Dvořák]

Daniel Weber said:

Daniel Weber said:

I'm not quite sure what you mean by expressing a theory in Lean

What would expressing PA mean, for instance?

I didn't get that far. I was thinking about finitely-axiomatized theories (i.e., no schemas).
For finitely-axiomatized theories, I can certainly assert that an arbitrary proposition holds in given theory by writing an example where arguments contain all of function symbols, relational symbols, and axioms.

[Martin Dvořák]

Daniel Weber said:

I'm quite certain this is stronger than PA, i.e. there are theorems which are true on this N but aren't provable in PA

Even with Robinson arithmetic, I believe, if you make the idiomatic thing in Lean, you enforce the standard model of natural numbers, which is not what the FOL theory does.

[Martin Dvořák]

I should look into Mathlib/ModelTheory because I hope I will find a way how to axiomatize theories of arithmetic without the use of inductive types.

[Martin Dvořák]

Daniel Weber said:

I'm quite certain this is stronger than PA, i.e. there are theorems which are true on this N but aren't provable in PA

Is there any theorem without preconditions that you can prove in your file but not in FOL PA?

[Daniel Weber]

Martin Dvořák said:

Daniel Weber said:

Daniel Weber said:

I'm not quite sure what you mean by expressing a theory in Lean

What would expressing PA mean, for instance?

I didn't get that far. I was thinking about finitely-axiomatized theories (i.e., no schemas).
For finitely-axiomatized theories, I can certainly assert that an arbitrary proposition holds in given theory by writing an example where arguments contain all of function symbols, relational symbols, and axioms.

I may be talking nonsense, but IIRC there is an important distinction between internal models, where the symbols of the theory are directly interpreted as Lean objects, which is what you're describing here, and external models, which I believe Mathlib/ModelTheory is, where the semantics given to the objects of the theory may be different then the one Lean gives

[Martin Dvořák]

Do I understand correctly that, if you use external models, the Lean theorem is
example : FOL_encode T ⊢ FOL_encode P
(and you can manually check that nothing in the environment can allow you to prove things that shouldn't be possible to prove in FOL) whereäs, if you use internal models, you can write theorem
example (T) : P
but the entire environment can be used to prove it (alternatively, you can use prelude and put T into axiom).

[Daniel Weber]

Martin Dvořák said:

Daniel Weber said:

I'm quite certain this is stronger than PA, i.e. there are theorems which are true on this N but aren't provable in PA

Is there any theorem without preconditions that you can prove in your file but not in FOL PA?

I'm fairly certain that you can prove Goodstein's theorem there, for instance, by showing the equivalence to ℕ and proving it there

[Martin Dvořák]

Daniel Weber said:

I'm fairly certain that you can prove Goodstein's theorem there, for instance, by showing the equivalence to ℕ and proving it there

I am really confused. Do your axioms enforce the standard model of natural numbers?

[Daniel Weber]

Yes, applying induction to fun n ↦ ∃ m : ℕ, succ^[m] zero = n

[Martin Dvořák]

I think that ∀ n : N, ∃ m : ℕ, succ^[m] zero = n is not among your axioms and I don't see a way to obtain in from them off top of my head.

[Daniel Weber]

It's not, but it can be proved from induction

[Daniel Weber]

But an example in a finitely-axiomatized theorem might be more satisfying

[Daniel Weber]

Wait, I'm confused

[Martin Dvořák]

Daniel Weber said:

It's not, but it can be proved from induction

induction on what?

[Notification Bot]

17 messages were moved here from #general > Theories without equality by Martin Dvořák.

[Notification Bot]

14 messages were moved here from #general > Expressing PA in Lean by Martin Dvořák.

[Notification Bot]

14 messages were moved here from #general > Theories without equality by Martin Dvořák.

[Daniel Weber]

import Mathlib.Logic.Function.Iterate

axiom N : Type
axiom zero : N
axiom succ : N → N
axiom add : N → N → N
axiom mul : N → N → N
axiom succ_ne_zero : ∀ x : N, zero ≠ succ x
axiom succ_inj : ∀ x y : N, succ x = succ y → x = y
axiom add_zero : ∀ x : N, add x zero = x
axiom add_succ : ∀ x y : N, add x (succ y) = succ (add x y)
axiom mul_zero : ∀ x : N, mul x zero = zero
axiom mul_succ : ∀ x y : N, mul x (succ y) = add (mul x y) x
axiom induction : ∀ p : N → Prop, (p zero ∧ ∀ x : N, p x → p (succ x)) → ∀ x : N, p x

lemma lemm : ∀ n : N, ∃ m : Nat, succ^[m] zero = n := by
  apply induction
  constructor
  · exact ⟨0, rfl⟩
  · intro x hx
    have ⟨m, hm⟩ := hx
    exists m+1
    rw [Function.iterate_succ_apply', hm]

#print axioms lemm

I thought this works, but Function.iterate_succ_apply' depends on Quot.sound and propext (probably for funext). However, I think it can still be proved without those

[Martin Dvořák]

My bad, I thought you meant the induction tactic!

[Martin Dvořák]

Martin Dvořák said:

Do I understand correctly that, if you use external models, the Lean theorem is
example : FOL_encode T ⊨ FOL_encode P
whereäs, if you use internal models, you can write theorem
example {T} : P
but the entire environment can be used to prove it (alternatively, you can use prelude and put T into axiom).

Do I understand it right? Not every FOL theory can be expressed using internal models, but you can express every FOL theory using external models?

[Metin Ersin Arıcan]

Daniel Weber said:

Daniel Weber said:

I'm not quite sure what you mean by expressing a theory in Lean

What would expressing PA mean, for instance?

axiom N : Type
axiom zero : N
axiom succ : N → N
axiom add : N → N → N
axiom mul : N → N → N
axiom succ_ne_zero : ∀ x : N, zero ≠ succ x
axiom succ_inj : ∀ x y : N, succ x = succ y → x = y
axiom add_zero : ∀ x : N, add x zero = x
axiom add_succ : ∀ x y : N, add x (succ y) = succ (add x y)
axiom mul_zero : ∀ x : N, mul x zero = zero
axiom mul_succ : ∀ x y : N, mul x (succ y) = add (mul x y) x
axiom induction : ∀ p : N → Prop, (p zero ∧ ∀ x : N, p x → p (succ x)) → ∀ x : N, p x

Is this an expression?

Isn't this a second order axiomatization instead of first order?

[François G. Dorais]

It is much stronger. For example, we can prove that every number is standard from these axioms:

noncomputable def stdval : Nat → N
| 0 => zero
| n+1 => succ (stdval n)

theorem stdall : ∀ x, ∃ n, x = stdval n := by
  apply induction
  constructor
  · exists 0
  · intro
    | x, ⟨y, h⟩ =>
      exists y+1
      unfold stdval
      rw [h]

[Violeta Hernández]

What's the thing avoiding a more faithful PA implementation? Is it just that Lean already comes preloaded with a stronger logic?

[Kevin Buzzard]

Surely you can just implement PA using the model theory we have. The issue is that you need to write the first order induction principle so you need to be able to say "this predicate can be expressed in a first order way" but that's exactly what all this Language and Term stuff lets you do, if I've understood correctly.

[Bjørn Kjos-Hanssen]

An easier approach (which may be enough, depending on what you want to do), is to "work in PA" by just stating the instances of axiom induction you use as you go along and writing "Clearly, all induction axioms in this file are first order".