feat(Modal): Arithmetical Soundness of 𝐆𝐋

Logic.lean

@@ -66,6 +66,7 @@ import Logic.FirstOrder.Arith.Nonstandard
 
 import Logic.FirstOrder.Arith.EA.Basic
 
+import Logic.FirstOrder.Incompleteness.ProvabilityCondition
 import Logic.FirstOrder.Incompleteness.FirstIncompleteness
 import Logic.FirstOrder.Incompleteness.SelfReference
 

Logic/FirstOrder/Incompleteness/ProvabilityCondition.lean

@@ -1,4 +1,6 @@
 import Logic.FirstOrder.Arith.Theory
+import Logic.Logic.HilbertStyle.Gentzen
+import Logic.Logic.HilbertStyle.Supplemental
 
 namespace LO.FirstOrder
 
@@ -18,25 +20,143 @@ notation "⦍" β "⦎" σ:80 => pr β σ
 class Conservative (β : ProvabilityPredicate L₀ L) (T₀ : Theory L₀) (T : outParam (Theory L)) where
   iff (σ : Sentence L) : T ⊢! σ ↔ T₀ ⊢! ⦍β⦎ σ
 
+def consistency (β : ProvabilityPredicate L₀ L) : Sentence L₀ := ~⦍β⦎⊥
+notation "Con⦍" β "⦎" => consistency β
+
 end
 
-section HilbertBernays
+section Conditions
 
 variable [Semiterm.Operator.GoedelNumber L (Sentence L)]
 
 class HilbertBernays₁ (β : ProvabilityPredicate L L) (T₀ : Theory L) (T : outParam (Theory L)) where
-  D1 (σ : Sentence L) : T ⊢! σ → T₀ ⊢! ⦍β⦎σ
+  D1 {σ : Sentence L} : T ⊢! σ → T₀ ⊢! ⦍β⦎σ
+
+
+class HilbertBernays₂ (β : ProvabilityPredicate L L) (T₀ : Theory L) (T : outParam (Theory L)) where
+  D2 {σ τ : Sentence L} : T₀ ⊢! ⦍β⦎(σ ⟶ τ) ⟶ ⦍β⦎σ ⟶ ⦍β⦎τ
 
-class HilbertBernays₂ (β : ProvabilityPredicate L L) (T₀ : Theory L) where
-  D2 (σ τ : Sentence L) : T₀ ⊢! ⦍β⦎(σ ⟶ τ) ⟶ ⦍β⦎σ ⟶ ⦍β⦎τ
 
-class HilbertBernays₃ (β : ProvabilityPredicate L L) (T₀ : Theory L) where
-  D3 (σ : Sentence L) : T₀ ⊢! ⦍β⦎σ ⟶ ⦍β⦎⦍β⦎σ
+class HilbertBernays₃ (β : ProvabilityPredicate L L) (T₀ : Theory L) (T : outParam (Theory L)) where
+  D3 {σ : Sentence L} : T₀ ⊢! ⦍β⦎σ ⟶ ⦍β⦎⦍β⦎σ
+
 
 class HilbertBernays (β : ProvabilityPredicate L L) (T₀ : Theory L) (T : outParam (Theory L))
-  extends β.HilbertBernays₁ T₀ T, β.HilbertBernays₂ T₀, β.HilbertBernays₃ T₀
+  extends β.HilbertBernays₁ T₀ T, β.HilbertBernays₂ T₀ T, β.HilbertBernays₃ T₀ T
+
+class Diagonalization (T : Theory L) where
+  fixpoint : Semisentence L 1 → Sentence L
+  diag (θ) : T ⊢! fixpoint θ ⟷ θ/[⸢fixpoint θ⸣]
+
+
+class Loeb (β : ProvabilityPredicate L L) (T₀ : Theory L) (T : outParam (Theory L)) where
+  LT {σ : Sentence L} : T ⊢! ⦍β⦎σ ⟶ σ → T ⊢! σ
+
+class FormalizedLoeb (β : ProvabilityPredicate L L) (T₀ : Theory L) (T : outParam (Theory L)) where
+  FLT {σ : Sentence L} : T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ
+
+
+section
+
+variable {T₀ T : Theory L}
+variable [T₀ ≼ T] {σ τ : Sentence L}
+
+def HilbertBernays₁.D1s [HilbertBernays₁ β T₀ T]: T ⊢! σ → T ⊢! ⦍β⦎σ := by
+  intro h;
+  apply System.Subtheory.prf! (𝓢 := T₀);
+  apply HilbertBernays₁.D1 h;
+
+def HilbertBernays₂.D2s [HilbertBernays₂ β T₀ T] : T ⊢! ⦍β⦎(σ ⟶ τ) ⟶ ⦍β⦎σ ⟶ ⦍β⦎τ := by
+  apply System.Subtheory.prf! (𝓢 := T₀);
+  apply HilbertBernays₂.D2;
+
+def HilbertBernays₂.D2' [HilbertBernays β T₀ T] [System.ModusPonens T] : T ⊢! ⦍β⦎(σ ⟶ τ) → T ⊢! ⦍β⦎σ ⟶ ⦍β⦎τ := by
+  intro h;
+  exact (HilbertBernays₂.D2s (T₀ := T₀)) ⨀ h;
+
+def HilbertBernays₃.D3s [HilbertBernays₃ β T₀ T] : T ⊢! ⦍β⦎σ ⟶ ⦍β⦎⦍β⦎σ := by
+  apply System.Subtheory.prf! (𝓢 := T₀);
+  apply HilbertBernays₃.D3;
+
+def Loeb.LT' [Loeb β T₀ T] {σ : Sentence L} : T ⊢! ⦍β⦎σ ⟶ σ → T ⊢! σ := Loeb.LT T₀
+
+end
+
+end Conditions
+
+
+section LoebTheorem
+
+variable [DecidableEq (Sentence L)]
+         [Semiterm.Operator.GoedelNumber L (Sentence L)]
+         (T₀ T : Theory L) [T₀ ≼ T] [Diagonalization T₀]
+open LO.System
+open HilbertBernays₁ HilbertBernays₂ HilbertBernays₃
+open Diagonalization
+
+private lemma loeb_fixpoint
+  (β : ProvabilityPredicate L L) [β.HilbertBernays T₀ T]
+  (σ : Sentence L) : ∃ (θ : Sentence L), T₀ ⊢! ⦍β⦎θ ⟶ ⦍β⦎σ ∧ T₀ ⊢! (⦍β⦎θ ⟶ σ) ⟶ θ := by
+  have hθ := diag (T := T₀) “x | !β.prov x → !σ”;
+  generalize (fixpoint T₀ “x | !β.prov x → !σ”) = θ at hθ;
+
+  have eθ : θ ⟷ (β.prov/[#0] ⟶ σ/[])/[⸢θ⸣] = θ ⟷ (⦍β⦎θ ⟶ σ) := by
+    simp [←Rew.hom_comp_app, Rew.substs_comp_substs]; rfl;
+  replace hθ : T₀ ⊢! θ ⟷ (⦍β⦎θ ⟶ σ) := by simpa [←eθ] using hθ;
+
+  existsi θ;
+  constructor;
+  . exact (imp_trans! (D2 ⨀ (D1 (Subtheory.prf! $ conj₁'! hθ))) D2) ⨀₁ D3;
+  . exact conj₂'! hθ;
+
+variable {β : ProvabilityPredicate L L} [β.HilbertBernays T₀ T]
+
+theorem loeb_theorm (H : T ⊢! ⦍β⦎σ ⟶ σ) : T ⊢! σ := by
+  obtain ⟨θ, hθ₁, hθ₂⟩ := loeb_fixpoint T₀ T β σ;
+
+  have d₁ : T  ⊢! ⦍β⦎θ ⟶ σ := imp_trans! (Subtheory.prf! hθ₁) H;
+  have    : T₀ ⊢! ⦍β⦎θ      := D1 $ Subtheory.prf! hθ₂ ⨀ d₁;
+  have d₂ : T  ⊢! ⦍β⦎θ      := Subtheory.prf! this;
+  exact d₁ ⨀ d₂;
+
+instance : Loeb β T₀ T := ⟨loeb_theorm T₀ T⟩
+
+theorem formalized_loeb_theorem : T₀ ⊢! ⦍β⦎(⦍β⦎σ ⟶ σ) ⟶ ⦍β⦎σ := by
+  obtain ⟨θ, hθ₁, hθ₂⟩ := loeb_fixpoint T₀ T β σ;
+
+  have : T₀ ⊢! (⦍β⦎σ ⟶ σ) ⟶ (⦍β⦎θ ⟶ σ) := imply_left_replace! hθ₁
+  have : T ⊢! (⦍β⦎σ ⟶ σ) ⟶ θ := Subtheory.prf! $ imp_trans! this hθ₂;
+  exact imp_trans! (D2 ⨀ (D1 this)) hθ₁;
+
+instance : FormalizedLoeb β T₀ T := ⟨formalized_loeb_theorem T₀ T⟩
+
+end LoebTheorem
+
+section Second
+
+variable [DecidableEq (Sentence L)]
+         [Semiterm.Operator.GoedelNumber L (Sentence L)]
+         (T₀ T : Theory L) [T₀ ≼ T] [Diagonalization T₀]
+         {β : ProvabilityPredicate L L} [β.Loeb T₀ T]
+open LO.System LO.System.NegationEquiv
+open HilbertBernays₁ HilbertBernays₂ HilbertBernays₃
+open Diagonalization
+
+/-- Second Incompleteness Theorem -/
+lemma unprovable_consistency_of_Loeb : System.Consistent T → T ⊬! ~⦍β⦎⊥ := by
+  contrapose;
+  intro hC; simp [neg_equiv'!] at hC;
+  have : T ⊢! ⊥ := Loeb.LT T₀ hC;
+  apply System.not_consistent_iff_inconsistent.mpr;
+  apply System.inconsistent_of_provable this;
+
+/-- Formalized Second Incompleteness Theorem -/
+lemma formalized_second (H : T ⊬! ~Con⦍β⦎) : T ⊬! Con⦍β⦎ ⟶ ~⦍β⦎(~Con⦍β⦎) := by
+  by_contra hC;
+  have : T ⊢! ~Con⦍β⦎ := Loeb.LT T₀ $ contra₁'! hC;
+  contradiction;
 
-end HilbertBernays
+end Second
 
 end ProvabilityPredicate
 

Logic/FirstOrder/Incompleteness/SelfReference.lean

@@ -31,7 +31,11 @@ noncomputable def fixpoint (θ : Semisentence ℒₒᵣ 1) : Sentence ℒₒᵣ
 
 lemma substs_diag (θ σ : Semisentence ℒₒᵣ 1) :
     “!(diag θ) !!(⸢σ⸣ : Semiterm ℒₒᵣ Empty 0)” = “∀ x, !ssbs x !!⸢σ⸣ !!⸢σ⸣ → !θ x” := by
-  simp [diag, Rew.q_substs, ←Rew.hom_comp_app, Rew.substs_comp_substs]
+  -- simp [diag, Rew.q_substs, ←Rew.hom_comp_app, Rew.substs_comp_substs]
+  simp [diag]
+  simp [Rew.q_substs]
+  simp [←Rew.hom_comp_app]
+  simp [Rew.substs_comp_substs]
 
 lemma fixpoint_eq (θ : Semisentence ℒₒᵣ 1) :
     fixpoint θ = “∀ x, !ssbs x !!⸢diag θ⸣ !!⸢diag θ⸣ → !θ x” := by

Logic/Logic/HilbertStyle/Basic.lean

@@ -199,7 +199,7 @@ namespace NegationEquiv
 
 variable [System.NegationEquiv 𝓢]
 
-lemma neg_equiv! : 𝓢 ⊢! ~p ⟷ (p ⟶ ⊥) := ⟨NegationEquiv.neg_equiv⟩
+@[simp] lemma neg_equiv! : 𝓢 ⊢! ~p ⟷ (p ⟶ ⊥) := ⟨NegationEquiv.neg_equiv⟩
 
 def neg_equiv'.mp : 𝓢 ⊢ ~p → 𝓢 ⊢ p ⟶ ⊥ := λ h => (conj₁' neg_equiv) ⨀ h
 def neg_equiv'.mpr : 𝓢 ⊢ p ⟶ ⊥ → 𝓢 ⊢ ~p := λ h => (conj₂' neg_equiv) ⨀ h

Logic/Logic/HilbertStyle/Gentzen.lean

@@ -42,6 +42,13 @@ instance (𝓣 : S) : Classical 𝓣 where
       (wkL [q ⟶ r, q] (by simp) <| implyLeft (closed q (by simp) (by simp)) (closed r (by simp) (by simp)))
   dne := fun p ↦ of <| implyRight <| negLeft <| negRight <| closed p (by simp) (by simp)
 
+instance (𝓣 : S) : System.NegationEquiv 𝓣 := ⟨
+  λ {p} => of <| andRight
+    (implyRight <| implyRight <| rotateLeft <| negLeft <| closed p (by simp) (by simp))
+    (implyRight <| negRight  <| rotateLeft <| implyLeft (closed p (by simp) (by simp)) (falsum _ _))
+⟩
+
+
 def notContra {𝓣 : S} {p q : F} (b : 𝓣 ⊢ p ⟷ ~q) : 𝓣 ⊢ ~p ⟷ q := by
   have : [p ⟷ ~q] ⊢² [~p ⟷ q] :=
     andRight

Logic/Logic/HilbertStyle/Supplemental.lean

@@ -145,6 +145,7 @@ def dn [HasDNE 𝓢] : 𝓢 ⊢ p ⟷ ~~p := iffIntro dni dne
 @[simp] lemma dn! [HasDNE 𝓢] : 𝓢 ⊢! p ⟷ ~~p := ⟨dn⟩
 
 
+
 def contra₀ : 𝓢 ⊢ (p ⟶ q) ⟶ (~q ⟶ ~p) := by
   apply deduct';
   apply deduct;
@@ -189,8 +190,24 @@ def contra₃ [HasDNE 𝓢] : 𝓢 ⊢ (~p ⟶ ~q) ⟶ (q ⟶ p) :=  deduct' $ c
 @[simp] lemma contra₃! [HasDNE 𝓢] : 𝓢 ⊢! (~p ⟶ ~q) ⟶ (q ⟶ p) := ⟨contra₃⟩
 
 
-def neg_iff' (b : 𝓢 ⊢ p ⟷ q) : 𝓢 ⊢ ~p ⟷ ~q := iffIntro (contra₀' $ conj₂' b) (contra₀' $ conj₁' b)
-lemma neg_iff'! (b : 𝓢 ⊢! p ⟷ q) : 𝓢 ⊢! ~p ⟷ ~q := ⟨neg_iff' b.some⟩
+def negIff' (b : 𝓢 ⊢ p ⟷ q) : 𝓢 ⊢ ~p ⟷ ~q := iffIntro (contra₀' $ conj₂' b) (contra₀' $ conj₁' b)
+lemma neg_iff'! (b : 𝓢 ⊢! p ⟷ q) : 𝓢 ⊢! ~p ⟷ ~q := ⟨negIff' b.some⟩
+
+
+namespace NegationEquiv
+
+variable [System.NegationEquiv 𝓢]
+
+def negneg_equiv : 𝓢 ⊢ ~~p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := by
+  apply iffIntro;
+  . exact impTrans (by apply contra₀'; exact conj₂' NegationEquiv.neg_equiv) (conj₁' NegationEquiv.neg_equiv)
+  . exact impTrans (conj₂' NegationEquiv.neg_equiv) (by apply contra₀'; exact conj₁' NegationEquiv.neg_equiv)
+@[simp] lemma negneg_equiv! : 𝓢 ⊢! ~~p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := ⟨negneg_equiv⟩
+
+def negneg_equiv_dne [HasDNE 𝓢] : 𝓢 ⊢ p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := iffTrans dn negneg_equiv
+lemma negneg_equiv_dne! [HasDNE 𝓢] : 𝓢 ⊢! p ⟷ ((p ⟶ ⊥) ⟶ ⊥) := ⟨negneg_equiv_dne⟩
+
+end NegationEquiv
 
 
 def tne : 𝓢 ⊢ ~(~~p) ⟶ ~p := contra₀' dni

Logic/Logic/System.lean

@@ -335,6 +335,8 @@ def translation [𝓢 ≼ 𝓣] : 𝓢 ↝ 𝓣 where
 
 def ofTranslation (t : 𝓢 ↝ 𝓣) (h : ∀ p, t p = p) : 𝓢 ≼ 𝓣 := ⟨fun {p} b ↦ h p ▸ (t.prf b)⟩
 
+lemma prf! [𝓢 ≼ 𝓣] {f} : 𝓢 ⊢! f → 𝓣 ⊢! f := λ ⟨p⟩ ↦ ⟨Subtheory.prf p⟩
+
 end Subtheory
 
 section

Logic/Modal/Standard.lean

@@ -14,3 +14,5 @@ import Logic.Modal.Standard.Kripke.Geach.Completeness
 import Logic.Modal.Standard.Kripke.Geach.Reducible
 
 import Logic.Modal.Standard.Kripke.ModalCompanion
+
+import Logic.Modal.Standard.Provability.Basic

Logic/Modal/Standard/Deduction.lean

@@ -532,6 +532,12 @@ lemma reducible_K4Henkin_GL : (𝐊𝟒𝐇 : DeductionParameter α) ≤ₛ 𝐆
   . obtain ⟨_, _, e⟩ := hFour; subst_vars; exact axiomFour!;
   . obtain ⟨_, _, e⟩ := hH; subst_vars; exact axiomH!;
 
+lemma equivalent_GL_K4Loeb : (𝐆𝐋 : DeductionParameter α) =ₛ 𝐊𝟒(𝐋) := by
+  apply Equiv.antisymm_iff.mpr;
+  constructor;
+  . exact reducible_GL_K4Loeb;
+  . exact Reducible.trans (reducible_K4Loeb_K4Henkin) $ Reducible.trans reducible_K4Henkin_K4H reducible_K4Henkin_GL
+
 end GL
 
 end LO.Modal.Standard

Logic/Modal/Standard/HilbertStyle.lean

@@ -71,8 +71,6 @@ def multiboxIff' (h : 𝓢 ⊢ p ⟷ q) : 𝓢 ⊢ □^[n]p ⟷ □^[n]q := by
   | succ n ih => simpa using boxIff' ih;
 @[simp] lemma multibox_iff! (h : 𝓢 ⊢! p ⟷ q) : 𝓢 ⊢! □^[n]p ⟷ □^[n]q := ⟨multiboxIff' h.some⟩
 
-def negIff' (h : 𝓢 ⊢ p ⟷ q) : 𝓢 ⊢ (~p ⟷ ~q) := conj₃' (contra₀' $ conj₂' h) (contra₀' $ conj₁' h)
-@[simp] lemma neg_iff! (h : 𝓢 ⊢! p ⟷ q) : 𝓢 ⊢! ~p ⟷ ~q := ⟨negIff' h.some⟩
 
 def diaIff' (h : 𝓢 ⊢ p ⟷ q) : 𝓢 ⊢ (◇p ⟷ ◇q) := by
   simp only [StandardModalLogicalConnective.duality'];
@@ -113,7 +111,7 @@ def multidiaDuality : 𝓢 ⊢ ◇^[n]p ⟷ ~(□^[n](~p)) := by
   | zero => simp; apply dn;
   | succ n ih =>
     simp [StandardModalLogicalConnective.duality'];
-    apply neg_iff';
+    apply negIff';
     apply boxIff';
     exact iffTrans (negIff' ih) (iffComm' dn)
 @[simp] lemma multidiaDuality! : 𝓢 ⊢! ◇^[n]p ⟷ ~(□^[n](~p)) := ⟨multidiaDuality⟩
@@ -410,9 +408,23 @@ private def axiomFour_of_L [HasAxiomL 𝓢] : 𝓢 ⊢ Axioms.Four p := by
     exact conj₃' (FiniteContext.byAxm) (conj₁' (q := □□p) $ FiniteContext.byAxm);
   have : 𝓢 ⊢ p ⟶ (□⊡p ⟶ ⊡p) := impTrans this (implyLeftReplace BoxBoxdot_BoxDotbox);
   exact impTrans (impTrans (implyBoxDistribute' this) axiomL) (implyBoxDistribute' $ conj₂);
-
 instance [HasAxiomL 𝓢] : HasAxiomFour 𝓢 := ⟨fun _ ↦ axiomFour_of_L⟩
 
+def goedel2 [HasAxiomL 𝓢] : 𝓢 ⊢ (~(□⊥) ⟷ ~(□(~(□⊥))) : F) := by
+  apply negIff';
+  apply iffIntro;
+  . apply implyBoxDistribute';
+    exact efq;
+  . exact impTrans (by
+      apply implyBoxDistribute';
+      exact conj₁' NegationEquiv.neg_equiv;
+    ) axiomL;
+lemma goedel2! [HasAxiomL 𝓢] : 𝓢 ⊢! (~(□⊥) ⟷ ~(□(~(□⊥))) : F) := ⟨goedel2⟩
+
+def goedel2'.mp [HasAxiomL 𝓢] : 𝓢 ⊢ (~(□⊥) : F) → 𝓢 ⊢ ~(□(~(□⊥)) : F) := by intro h; exact (conj₁' goedel2) ⨀ h;
+def goedel2'.mpr [HasAxiomL 𝓢] : 𝓢 ⊢ ~(□(~(□⊥)) : F) → 𝓢 ⊢ (~(□⊥) : F) := by intro h; exact (conj₂' goedel2) ⨀ h;
+lemma goedel2'! [HasAxiomL 𝓢] : 𝓢 ⊢! (~(□⊥) : F) ↔ 𝓢 ⊢! ~(□(~(□⊥)) : F) := ⟨λ ⟨h⟩ ↦ ⟨goedel2'.mp h⟩, λ ⟨h⟩ ↦ ⟨goedel2'.mpr h⟩⟩
+
 def axiomH [HasAxiomH 𝓢] : 𝓢 ⊢ □(□p ⟷ p) ⟶ □p := HasAxiomH.H _
 @[simp] lemma axiomH! [HasAxiomH 𝓢] : 𝓢 ⊢! □(□p ⟷ p) ⟶ □p := ⟨axiomH⟩