Proof theory and Gentzen's consistency proof in assistants

Stream: general

[Tlön Uqbar]

https://proofassistants.stackexchange.com/questions/6462/how-far-is-gentzens-consistency-proof-of-peano-arithmetic-from-being-formalized Hope it's ok to crosspost this question here. I have not extensively used proof assistants, but I'm curious about how architecture exists around results in proof theory. I don't think Gentzen's consistency proof of Peano Arithmetic has ever been formalized in an assistant, and I'm curious if it's harder than other important logic results like the incompleteness theorems or independence of the continuum hypothesis, which have been formalized in proof assistents.

[James E Hanson]

It's a little bit ambiguous what it means to formalize Gentzen's theorem in a proof assistant like Lean. As you said in your question, what Gentzen showed, in modern language, is that primitive recursive arithmetic together with induction for quantifier-free predicates on the ordinal $\varepsilon_0$ proves the consistency of Peano arithmetic.

The issue is that part of the content of the theorem is the weakness of the metatheory in which it is proven. It's relatively straightforward to verify that Lean proves the consistency of PA outright by checking that Nat is a model of the axioms of Peano arithmetic (including in particular induction for first-order formulas).

In order to really verify Gentzen's theorem in a proof assistant, you have to do one of two things:

• Work in a proof assistant that can accommodate a weak metatheory like PRA + $\varepsilon_0$-induction.
• Prove in a stronger proof assistant (like Lean) that PRA + $\varepsilon_0$-induction proves $\mathrm{Con}(\mathsf{PA})$ (by, e.g., proving a statement of the form 'every model of PRA + $\varepsilon_0$-induction satisfies $\mathrm{Con}(\mathsf{PA})$').

These are both kind of tall orders. The only popular proof assistant that can even do the first one is Metamath, but my impression is that RPA + $\varepsilon_0$-induction would actually be somewhat painful to formalize in Metamath. (Metamath's kernel is extremely elegant in its absolute minimality, but it was designed with theories like ZFC and PA in mind.) Likewise, my impression with the second approach is many important quality of life features of a proof assistant like Lean really stop working well in that context.

I would be very interested in seeing a proof assistant aimed towards these kinds of things (e.g., weak arithmetic, weak set theories, and reverse math) because I think it's a fairly different engineering problem from that of ordinary proof assistants, but I do not personally have the large buckets of money that are realistically required to make and maintain a proof assistant with good UX.

[Snir Broshi]

You might be interested in #Formalized Formal Logic

[Jean Abou Samra]

@James E Hanson Are you familiar with higher-order abstract syntax? This does work quite well to formalize things in many different (non-substructural) logics inside proof assistants implementing type theory, to the extent that I think it would have a much higher usability / work invested ratio to develop some libraries of weak theories formalized in this style in existing proof assistants (and probably tactics if it's Lean) than to create a new proof assistant. Basically, the idea is that you work internally in a presheaf model over a category given by the syntax of your logic, and this gives you a system where you can largely paper over the concrete syntax by reusing the contexts and binders of the metatheory. See e.g. Rafaël Bocquet's PhD thesis.

(Anecdotally, over here in Budapest, we teach a course to computer science students with very little math background, where we make them write small programs/proofs in lots of different type systems/logics, like simply typed λ-calculus, system T, inductive and coinductive types, system F… Everything is done inside Rocq and it is simple enough that we manage to make the course mostly about the actual type systems and not the nitty gritty details of their encoding into the proof assistant.)

[Jean Abou Samra]

Here's a toy example proving in Lean that PA proves commutativity of addition:

noncomputable section

-- First-order logic
axiom Tm : Type
axiom For : Type
axiom TT : For
axiom FF : For
axiom For.And : For → For → For
infix:30 " ∧∧ " => For.And
axiom For.Or : For → For → For
infix:20 " ∨∨ " => For.Or
axiom For.Implies : For → For → For
infix:10 " ⇒⇒ " => For.Implies
axiom AA : (Tm → For) → For
axiom EE : (Tm → For) → For
axiom For.Eq : Tm → Tm → For
infix:50 " == " => For.Eq
def For.Not (φ : For) := φ ⇒⇒ FF
-- Not a double negation, just doubled like the rest to avoid conflict with built-in notation
prefix:40 "¬¬" => For.Not
axiom Prf : For → Type
axiom Prf.TrueIntro : Prf TT
axiom Prf.FalseElim : {φ : For} → Prf FF → Prf φ
axiom Prf.AndIntro : {φ ψ : For} → Prf φ → Prf ψ → Prf (φ ∧∧ ψ)
axiom Prf.AndElim1 : {φ ψ : For} → Prf (φ ∧∧ ψ) → Prf φ
axiom Prf.AndElim2 : {φ ψ : For} → Prf (φ ∧∧ ψ) → Prf ψ
axiom Prf.OrIntro1 : {φ ψ : For} → Prf φ → Prf (φ ∨∨ ψ)
axiom Prf.OrIntro2 : {φ ψ : For} → Prf ψ → Prf (φ ∨∨ ψ)
axiom Prf.OrElim : {φ ψ τ : For} → Prf (φ ∨∨ ψ) → (Prf φ → Prf τ) → (Prf ψ → Prf τ) → Prf τ
axiom Prf.ImpliesIntro : {φ ψ : For} → (Prf φ → Prf ψ) → Prf (φ ⇒⇒ ψ)
axiom Prf.ImpliesElim : {φ ψ : For} → Prf (φ ⇒⇒ ψ) → Prf φ → Prf ψ
axiom Prf.ForallIntro : {P : Tm → For} → ((t : Tm) → Prf (P t)) → Prf (AA P)
axiom Prf.ForallElim : {P : Tm → For} → Prf (AA P) → (t : Tm) → Prf (P t)
axiom Prf.ExistsIntro : {P : Tm → For} → (t : Tm) → Prf (P t) → Prf (EE P)
axiom Prf.ExistsElimTm : {P : Tm → For} → Prf (EE P) → Tm
axiom Prf.ExistsElimPrf : {P : Tm → For} → (p : Prf (EE P)) → Prf (P (Prf.ExistsElimTm p))
axiom Prf.Refl : (t : Tm) → Prf (t == t)
axiom Prf.Subst : {t u : Tm} → (P : Tm → For) → Prf (t == u) → Prf (P t) → Prf (P u)
axiom Prf.ExcludedMiddle : (φ : For) → Prf (φ ∨∨ ¬¬φ)
-- Peano arithmetic
axiom zero : Tm
axiom suc : Tm → Tm
axiom plus : Tm → Tm → Tm
infix:60 " ++ " => plus
axiom mul : Tm → Tm → Tm
infix:70 " ** " => mul
axiom zero_not_suc : (t : Tm) → Prf (¬¬(t == zero))
axiom suc_inj : {t u : Tm} → Prf (suc t == suc u) → Prf (t == u)
axiom plus_zero : (t : Tm) → Prf (t ++ zero == t)
axiom plus_suc : (t u : Tm) → Prf (t ++ suc u == suc (t ++ u))
axiom mul_zero : (t : Tm) → Prf (t ** zero == zero)
axiom mul_suc : (t u : Tm) → Prf (t ** (suc u) == t ++ t ** u)
axiom ind : (P : Tm → For) → Prf (P zero) → ((n : Tm) → Prf (P n) → Prf (P (suc n))) → (n : Tm) → Prf (P n)

-- Example: we prove in PA that addition is commutative
def eq_sym {a b : Tm} (h : Prf (a == b)) : Prf (b == a) :=
  Prf.Subst (fun x => x == a) h (Prf.Refl a)

def eq_trans {a b c : Tm} (h1 : Prf (a == b)) (h2 : Prf (b == c)) : Prf (a == c) :=
  Prf.Subst (fun x => a == x) h2 h1

def eq_cong {a b : Tm} (h : Prf (a == b)) (f : Tm → Tm) : Prf (f a == f b) :=
  Prf.Subst (fun x => f a == f x) h (Prf.Refl (f a))

def zero_plus (a : Tm) : Prf (zero ++ a == a) :=
  ind (fun x => zero ++ x == x)
      (plus_zero zero)
      (fun n h => eq_trans (plus_suc zero n) (eq_cong h suc))
      a

def suc_plus (a b : Tm) : Prf (suc a ++ b == suc (a ++ b)) :=
  ind (fun x => suc a ++ x == suc (a ++ x))
      (eq_trans (plus_zero (suc a)) (eq_cong (eq_sym (plus_zero a)) suc))
      (fun n h => eq_trans (plus_suc (suc a) n) (eq_cong (eq_trans h (eq_sym (plus_suc a n))) suc))
      b

def add_comm (a b : Tm) : Prf (a ++ b == b ++ a) :=
  ind (fun x => a ++ x == x ++ a)
      (eq_trans (plus_zero a) (eq_sym (zero_plus a)))
      (fun n h => eq_trans (plus_suc a n) (eq_trans (eq_cong h suc) (eq_sym (suc_plus n a))))
      b

[Jean Abou Samra]

Back to the problem at hand, this would help with the "working in PRA + induction up to ε₀" part, but you would still have to write the arithmetization of proofs in PA within this system, so it would remain annoying.

[James E Hanson]

Jean Abou Samra said:

Are you familiar with higher-order abstract syntax?

I'm not familiar with the specific term, but I feel like I've seen something similar when I looked at work on substructural logic in Isabelle.

To what extent are you able to use existing tactics in this context? That's kind of what I was getting at when I mentioned quality of life features.

[Jean Abou Samra]

I feel like I've seen something similar when I looked at work on substructural logic in Isabelle.

If you can recall more precisely where this is, I'm interested to see it, because as far as I know, substructural logics are exactly the one thing that at least the one logical framework in this style that I'm familiar with (second-order generalized algebraic theories) cannot handle.

To what extent are you able to use existing tactics in this context? That's kind of what I was getting at when I mentioned quality of life features.

You cannot directly reuse exactly the same tactic set, however it should be pretty easy to define tactics for the object theory from those for the metatheory. I don't have the patience to learn how to define tactics in Lean right now but if this was Rocq I would just do, e.g., Ltac fol_intro := apply Prf_ForallIntro; intro., Ltac fol_split := apply Prf_AndIntro., Ltac fol_exfalso := apply Prf_FalseElim., etc. Rewriting is a likely pain point and I don't know how easy it would be in Lean (if I recall correctly, Rocq's support for custom rewriting is relatively powerful but also quite bizarre and sometimes broken). Wait no, I'm talking nonsense since you can probably reuse the meta equality in this case, but I'm too tired to think properly.

[Dexin Zhang]

Jean Abou Samra said:

Here's a toy example proving in Lean that PA proves commutativity of addition:

Seems it's formalizing a proof system of PA inside Lean. I guess this falls into @James E Hanson 's "second approach"?

[Jean Abou Samra]

Seems it's formalizing a proof system of PA inside Lean. I guess this falls into @James E Hanson 's "second approach"?

Sure, it is. Just with a lot less work than the normal way to do it, because you can reuse stuff from the metatheory for free. It's a natural deduction system but you never talk about contexts, substitutions, De Bruijn indices, etc. (e.g., to create a proof that uses the ∀ intro rule, you just write Prf.ForallIntro (fun h => ...), where the fun h => ... is really a metatheoretic function). Of course it also has its limitations, e.g., this lets you construct proofs in PA, but unlike a normal embedding, you cannot prove that something is unprovable in PA. It's also not compatible with excluded middle in the metatheory, but if you can put down your pitchforks for a moment, as long as you're just using the metatheory to build proofs in the object theory, you'll never feel a need for excluded middle (having excluded middle in the object theory is perfectly fine).

[James E Hanson]

Jean Abou Samra said:

It's also not compatible with excluded middle in the metatheory,

On some level is this essentially how Isabelle codes HOL in Isabelle/HOL?

[James E Hanson]

Jean Abou Samra said:

If you can recall more precisely where this is, I'm interested to see it, because as far as I know, substructural logics are exactly the one thing that at least the one logical framework in this style that I'm familiar with (second-order generalized algebraic theories) cannot handle.

I might have stated this in a misleading way. I know that some work on certain paraconsistent logics (although possibly not substructural) have been done in Isabelle, and Zach Weber told me in an email exchange that he has been doing some work (with other people, although I don't remember who) on formalizing some substructural logic (related to his philosophical work) in Isabelle. I also personally tried my hand at formalizing some substructural arithmetic in Isabelle (and actually Metamath before that), although given the way way term substitution works in the particular logic I was thinking about, I'm not 100% sure that the implementation was conservative. I could DM you this if you really want to see it, but it's very rough and incomplete.

[Jean Abou Samra]

James E Hanson said:

Jean Abou Samra said:

It's also not compatible with excluded middle in the metatheory,

On some level is this essentially how Isabelle codes HOL in Isabelle/HOL?

Sorry, I'm not sure, because I've never used or studied Isabelle (all I know about it comes from a quick tutorial at our weekly type theory seminar a few weeks ago). I just downloaded the source code and looked at src/HOL/HOL.thy but I don't really understand how it works.

[Jean Abou Samra]

James E Hanson said:

I might have stated this in a misleading way. I know that some work on certain paraconsistent logics (although possibly not substructural) have been done in Isabelle, and Zach Weber told me in an email exchange that he has been doing some work (with other people, although I don't remember who) on formalizing some substructural logic (related to his philosophical work) in Isabelle. I also personally tried my hand at formalizing some substructural arithmetic in Isabelle (and actually Metamath before that), although given the way way term substitution works in the particular logic I was thinking about, I'm not 100% sure that the implementation was conservative. I could DM you this if you really want to see it, but it's very rough and incomplete.

I see, thanks (no need to send it).

[Palalansoukî]

Instead of a faithful translation of Getzen's consistency proof, how about formalizing a Gentzen's result from an ordinal analysis perspective?

The proof that the proof-theoretic ordinal ($\Pi^1_1$-ordinal) of $\mathsf{PA}(X)$ is $\epsilon_0$ is not significantly different from Gentzen's original proof. Moreover, it would be simpler than formalizing proof theory within arithmetic.