Why are proofs of object theories done in Lean ?

[ruplet]

Dear developers,

I am really happy to have found your project! I am working on formalizing some results from bounded arithmetic and most importantly, from Cook and Nguyen's work. For this I need, similarly to you, e.g. prove in PA- that some function terminates. I look at your proofs, e.g. in the PeanoMinus.lean file and notice that you conduct your proofs not strictly in PA-, but in the Lean model of the PA- theory. Does it not constitute for a slightly weaker result than a proof done purely in proof theory? For my purposes, I really need to convince reverse mathematicians that I can provide them a convenient way to formalize their results on computer. So I was thinking of using a deep embedding of the logic and re-proving all the deduction theorems etc. I see that you are doing it in another way and am curious - would it not be better to write down the formalized proofs inside of PA- instead of inside a model in Lean? Thank you!

[iehality]

Hi eerio,

Glad you are interested in the project.

Yes, it is a weaker result than writing a formalized proof in the constructive sense, but they are equivalent when working in classical logic since one can prove the existence of such a proof using the completeness theorem (e.g.

Foundation/Foundation/FirstOrder/Arith/Model.lean

Lines 238 to 239 in f3833ad

	lemma oRing_provable₀_of (T : Theory ℒₒᵣ) [𝐄𝐐 ⪯ T] (σ : Sentence ℒₒᵣ) (H : ∀ (M : Type*) [ORingStruc M] [M ⊧ₘ* T], M ⊧ₘ₀ σ) :
	T ⊢!. σ := complete (T := T) <| oRing_consequence_of _ _ H

).

Once I tried a purely syntactic approach (see https://github.com/FormalizedFormalLogic/Foundation/tree/principia/Logic/Predicate/FirstOrder/Principia), but soon found it is torturous. First, expansion by definition is difficult. It is impractical to change the language itself with each new function or relation definition. It is also painful not being able to use basic tactics such as simp or rw. This is not the case with model-based approach. Arguments themselves are language-independent, so new functions can be added easily, and proof automations are available.