Formalized Formal Logic

2. Arithmetic🔗

In this formalization, we prefer developing arithmetic model theoretic, i.e. show T \models \sigma instead of T \vdash \sigma (They are equivalent thanks to the completeness theorem.).

variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝗜𝚺₁]

This procedure is done as follows. Suppose we wish to prove that the totality of an exponential function can be proved in \mathsf{I}\Sigma_1 First, the graph of the exponential function must be defined. This is achieved by the following two definitions.

1 By working in model of \mathsf{I}Σ_1, declare the semantic definition of the graph of the exponential function.

def

LO.ISigma0.Exponential.{u_1} {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝗜𝚺₀]
  (x y : V) : Prop
LO.ISigma0.Exponential.{u_1}
  {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₀] (x y : V) : Prop

The graph of the exponential function

2 Declare the syntactic definition of the semantic definition.

theorem

LO.ISigma0.Exponential.defined.{u_1} {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₀] : 𝚺₀-Relation Exponential via exponentialDef
LO.ISigma0.Exponential.defined.{u_1}
  {V : Type u_1} [ORingStruc V]
  [V ⊧ₘ* 𝗜𝚺₀] :
  𝚺₀-Relation Exponential via
    exponentialDef

The graph of the exponential function can be defined by the $\Delta_0$-formula.

Then prove the totality.

lemma range_exists (x : V) : ∃ y, Exponential x y := byV:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁x:V⊢ ∃ y, Exponential x y
  induction x using ISigma1.sigma1_succ_inductionhPV:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁⊢ 𝚺₁-Predicate fun x ↦ ∃ y, Exponential x yzeroV:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁⊢ ∃ y, Exponential 0 ysuccV:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁x✝:Va✝:∃ y, Exponential x✝ y⊢ ∃ y, Exponential (x✝ + 1) y
  ·hPV:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁⊢ 𝚺₁-Predicate fun x ↦ ∃ y, Exponential x y definabilityAll goals completed! 🐙
  case zero =>V:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁⊢ ∃ y, Exponential 0 y
    exact ⟨1, byV:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁⊢ Exponential 0 1 simpAll goals completed! 🐙⟩
  case succ x IH =>V:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁x:VIH:∃ y, Exponential x y⊢ ∃ y, Exponential (x + 1) y
    rcases IH with ⟨y, IH⟩V:Type u_1inst✝¹:ORingStruc Vinst✝:V ⊧ₘ* 𝗜𝚺₁x:Vy:VIH:Exponential x y⊢ ∃ y, Exponential (x + 1) y
    exact ⟨2 * y, IH.succ⟩All goals completed! 🐙

Since Exponential and Exponential.total are defined in all the model of \mathsf{I}\Sigma_1, 𝐈𝚺₁ ⊢ ∀' ∃' exponentialDef is obtained by the completeness theorem.

lemma exp_total :
    𝗜𝚺₁ ⊢ “∀ x, ∃ y, !↑exponentialDef x y” := by⊢ 𝗜𝚺₁ ⊢ ∀' ∃' ↑exponentialDef/[#1, #0]
  apply oRing_provable_of.{0}H⊢ ∀ (M : Type) [inst : ORingStruc M] [M ⊧ₘ* 𝗜𝚺₁], M ⊧ₘ ∀' ∃' ↑exponentialDef/[#1, #0]
  intro M _HM:Typeinst✝:ORingStruc M⊢ ∀ [M ⊧ₘ* 𝗜𝚺₁], M ⊧ₘ ∀' ∃' ↑exponentialDef/[#1, #0] _HM:Typeinst✝¹:ORingStruc Minst✝:M ⊧ₘ* 𝗜𝚺₁⊢ M ⊧ₘ ∀' ∃' ↑exponentialDef/[#1, #0]
  suffices ∀ x, ∃ y, Exponential x y byM:Typeinst✝¹:ORingStruc Minst✝:M ⊧ₘ* 𝗜𝚺₁this:failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation) := ?_mvar.613⊢ M ⊧ₘ ∀' ∃' ↑exponentialDef/[#1, #0]
    simpa [models_iff]All goals completed! 🐙
  exact range_existsAll goals completed! 🐙

This was the result we wanted to achieve.

This approach has several advantages:

1 In general, writing a formalized proof (in formalized system!) is very tedious. Meta-proofs, on the other hand, tend to be relatively concise. 2 Many definitions and proofs of logic and algebra in Mathlib can be used. 3 Metaprogramming can streamline the proof process (especially definability). 4 It is easy to extend predicates and functions. When adding predicates or functions, it is necessary to extend its language by extension by definition in case of formalized proof, but not in model theoretic approach.