add(Incompleteness): Add Jeroslow's Sentence and Formalized Law of Noncontradiction

Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean

@@ -35,11 +35,12 @@ theorem provable_D2 {σ π} : 𝗜𝚺₁ ⊢ □(σ ➝ π) ➝ □σ ➝ □π
 
 variable (T)
 
-noncomputable abbrev _root_.LO.FirstOrder.Theory.standardProvability : Provability 𝗜𝚺₁ T := ⟨T.provable⟩
+noncomputable abbrev _root_.LO.FirstOrder.Theory.standardProvability : Provability 𝗜𝚺₁ T where
+  prov := T.provable
+  prov_def := provable_D1
 
 variable {T}
 
-instance : T.standardProvability.HBL1 := ⟨provable_D1⟩
 instance : T.standardProvability.HBL2 := ⟨provable_D2⟩
 
 lemma standardProvability_def (σ : Sentence L) : T.standardProvability σ = T.provabilityPred σ := rfl

Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean

@@ -21,7 +21,8 @@ namespace ProvabilityAbstraction
 
 structure Provability [L.ReferenceableBy L₀] (T₀ : Theory L₀) (T : Theory L) where
   prov : Semisentence L₀ 1
-
+  /-- Derivability condition `D1` -/
+  prov_def {σ : Sentence L} : T ⊢ σ → T₀ ⊢ prov/[⌜σ⌝]
 
 namespace Provability
 
@@ -43,9 +44,7 @@ variable
   {L₀ L : Language} [L.ReferenceableBy L₀]
   {T₀ : Theory L₀} {T : Theory L}
 
-class Provability.HBL1 (𝔅 : Provability T₀ T) where
-  D1 {σ : Sentence L} : T ⊢ σ → T₀ ⊢ 𝔅 σ
-export Provability.HBL1 (D1)
+lemma D1 {𝔅 : Provability T₀ T} {σ : Sentence L} : T ⊢ σ → T₀ ⊢ 𝔅 σ := fun h ↦ 𝔅.prov_def h
 
 class Provability.HBL2 [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} (𝔅 : Provability T₀ T) where
   D2 {σ τ : Sentence L} : T₀ ⊢ 𝔅 (σ ➝ τ) ➝ 𝔅 σ ➝ 𝔅 τ
@@ -55,7 +54,7 @@ class Provability.HBL3 [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provabi
   D3 {σ : Sentence L} : T₀ ⊢ 𝔅 σ ➝ 𝔅 (𝔅 σ)
 export Provability.HBL3 (D3)
 
-class Provability.HBL [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) extends 𝔅.HBL1, 𝔅.HBL2, 𝔅.HBL3
+class Provability.HBL [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) extends 𝔅.HBL2, 𝔅.HBL3
 
 class Provability.Löb [L.ReferenceableBy L] {T₀ T : Theory L} (𝔅 : Provability T₀ T) where
   LT {σ : Sentence L} : T ⊢ 𝔅 σ ➝ σ → T ⊢ σ
@@ -101,31 +100,31 @@ lemma D2' [𝔅.HBL2] : T₀ ⊢ 𝔅 (σ ➝ τ) → T₀ ⊢ 𝔅 σ ➝ 𝔅
   intro h;
   exact D2 ⨀ h;
 
-lemma prov_distribute_imply [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := D2' $ D1 h
+lemma prov_distribute_imply [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ := D2' $ D1 h
 
-lemma prov_distribute_iff [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ τ) : T₀ ⊢ 𝔅 σ ⭤ 𝔅 τ := by
+lemma prov_distribute_iff [𝔅.HBL2] (h : T ⊢ σ ⭤ τ) : T₀ ⊢ 𝔅 σ ⭤ 𝔅 τ := by
   apply E!_intro;
   . exact prov_distribute_imply $ K!_left h;
   . exact prov_distribute_imply $ K!_right h;
 
-lemma dia_distribute_imply [L₀.DecidableEq] [L.DecidableEq] [𝔅.HBL1] [𝔅.HBL2]
+lemma dia_distribute_imply [L₀.DecidableEq] [L.DecidableEq] [𝔅.HBL2]
   (h : T ⊢ σ ➝ τ) : T₀ ⊢ 𝔅.dia σ ➝ 𝔅.dia τ := by
   have : T₀ ⊢ 𝔅 (∼τ) ➝ 𝔅 (∼σ) := prov_distribute_imply $ by cl_prover [h];
   cl_prover [this]
 
-lemma prov_distribute_and [𝔅.HBL1] [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ ⋏ 𝔅 τ := by
+lemma prov_distribute_and [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ ⋏ 𝔅 τ := by
   have h₁ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 σ := D2' $ D1 and₁!;
   have h₂ : T₀ ⊢ 𝔅 (σ ⋏ τ) ➝ 𝔅 τ := D2' $ D1 and₂!;
   cl_prover [h₁, h₂];
 
-lemma prov_distribute_and' [𝔅.HBL1] [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) → T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ := λ h => prov_distribute_and ⨀ h
+lemma prov_distribute_and' [𝔅.HBL2] [L₀.DecidableEq] : T₀ ⊢ 𝔅 (σ ⋏ τ) → T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ := λ h => prov_distribute_and ⨀ h
 
-lemma prov_collect_and [𝔅.HBL1] [𝔅.HBL2] [L₀.DecidableEq] [L.DecidableEq] : T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := by
+lemma prov_collect_and [𝔅.HBL2] [L₀.DecidableEq] [L.DecidableEq] : T₀ ⊢ 𝔅 σ ⋏ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := by
   have h₁ : T₀ ⊢ 𝔅 σ ➝ 𝔅 (τ ➝ σ ⋏ τ) := prov_distribute_imply $ by cl_prover
   have h₂ : T₀ ⊢ 𝔅 (τ ➝ σ ⋏ τ) ➝ 𝔅 τ ➝ 𝔅 (σ ⋏ τ) := D2;
   cl_prover [h₁, h₂];
 
-lemma sound_iff₀ [𝔅.HBL1] [𝔅.Sound₀] : T₀ ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound₀, D1⟩
+lemma sound_iff₀ [𝔅.Sound₀] : T₀ ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound₀, D1⟩
 
 end
 
@@ -136,7 +135,7 @@ variable
   {𝔅 : Provability T₀ T}
   {σ τ : Sentence L}
 
-lemma D1_shift [𝔅.HBL1] : T ⊢ σ → T ⊢ 𝔅 σ := by
+lemma D1_shift : T ⊢ σ → T ⊢ 𝔅 σ := by
   intro h;
   apply Entailment.WeakerThan.pbl (𝓢 := T₀);
   apply D1 h;
@@ -150,13 +149,13 @@ lemma D3_shift [𝔅.HBL3] : T ⊢ 𝔅 σ ➝ 𝔅 (𝔅 σ) := by
 lemma FLT_shift [𝔅.FormalizedLöb] : T ⊢ 𝔅 (𝔅 σ ➝ σ) ➝ 𝔅 σ := by
   apply Entailment.WeakerThan.pbl (𝓢 := T₀) $ FLT;
 
-lemma prov_distribute_imply' [𝔅.HBL1] [𝔅.HBL2] (h : T₀ ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ :=
+lemma prov_distribute_imply' [𝔅.HBL2] (h : T₀ ⊢ σ ➝ τ) : T₀ ⊢ 𝔅 σ ➝ 𝔅 τ :=
   prov_distribute_imply $ WeakerThan.pbl h
 
-lemma prov_distribute_imply'' [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T ⊢ 𝔅 σ ➝ 𝔅 τ :=
+lemma prov_distribute_imply'' [𝔅.HBL2] (h : T ⊢ σ ➝ τ) : T ⊢ 𝔅 σ ➝ 𝔅 τ :=
   WeakerThan.pbl $ prov_distribute_imply h
 
-lemma sound_iff [𝔅.HBL1] [𝔅.Sound] : T ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound, fun h ↦ WeakerThan.pbl (D1 h)⟩
+lemma sound_iff [𝔅.Sound] : T ⊢ 𝔅 σ ↔ T ⊢ σ := ⟨sound, fun h ↦ WeakerThan.pbl (D1 h)⟩
 
 end
 
@@ -184,7 +183,7 @@ section First
 variable [L.DecidableEq]
 variable [T₀ ⪯ T] [Consistent T]
 
-theorem unprovable_gödel [𝔅.HBL1] : T ⊬ (gödel 𝔅) := by
+theorem unprovable_gödel : T ⊬ (gödel 𝔅) := by
   intro h;
   have h₁ : T ⊢ 𝔅 (gödel 𝔅) := D1_shift h;
   have h₂ : T ⊢ (gödel 𝔅) ⭤ ∼𝔅 (gödel 𝔅) := WeakerThan.pbl $ gödel_spec;
@@ -200,12 +199,12 @@ theorem unrefutable_gödel [GödelSound 𝔅] : T ⊬ ∼(gödel 𝔅) := by
   have : ¬Consistent T := not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr this
   contradiction;
 
-theorem gödel_independent [𝔅.HBL1] [GödelSound 𝔅] : Independent T (gödel 𝔅) := by
+theorem gödel_independent [GödelSound 𝔅] : Independent T (gödel 𝔅) := by
   constructor
   . apply unprovable_gödel
   . apply unrefutable_gödel
 
-theorem first_incompleteness [𝔅.HBL1] [GödelSound 𝔅] : Incomplete T :=
+theorem first_incompleteness [GödelSound 𝔅] : Incomplete T :=
   incomplete_def.mpr ⟨(gödel 𝔅), gödel_independent⟩
 
 end First
@@ -327,12 +326,12 @@ theorem unrefutable_rosser [𝔅.Rosser] : T ⊬ ∼𝐑 := by
     (N!_iff_CO!.mp hnρ) ⨀ hρ;
   contradiction
 
-theorem rosser_independent [L.DecidableEq] [𝔅.HBL1] [𝔅.Rosser] : Independent T 𝐑 := by
+theorem rosser_independent [L.DecidableEq] [𝔅.Rosser] : Independent T 𝐑 := by
   constructor
   . apply unprovable_gödel
   . apply unrefutable_rosser
 
-theorem rosser_first_incompleteness [L.DecidableEq] (𝔅 : Provability T₀ T) [𝔅.HBL1] [𝔅.Rosser] : Incomplete T :=
+theorem rosser_first_incompleteness [L.DecidableEq] (𝔅 : Provability T₀ T) [𝔅.Rosser] : Incomplete T :=
   incomplete_def.mpr ⟨gödel 𝔅, rosser_independent⟩
 
 omit [Diagonalization T₀] [Consistent T] in

Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean

@@ -0,0 +1,167 @@
+import Foundation.FirstOrder.Bootstrapping.RosserProvability
+
+namespace LO.FirstOrder
+
+namespace Derivation
+
+variable {𝓢 : SyntacticFormulas L} {φ : SyntacticSemiformula L 1}
+
+def specialize'! (t : SyntacticTerm L) (b : 𝓢 ⊢! ∀' φ) : 𝓢 ⊢! φ/[t] := by simpa using specialize (Γ := []) t b;
+
+def specialize' (t : SyntacticTerm L) (b : 𝓢 ⊢ ∀' φ) : 𝓢 ⊢ φ/[t] := ⟨specialize'! t b.get⟩
+
+end Derivation
+
+
+namespace Theory
+
+variable {T : Theory L} {φ : Semisentence L 1}
+
+def specialize! (t) (b : T ⊢! ∀' φ) : T ⊢! (φ/[t]) := by
+  apply ofSyntacticProof;
+  sorry;
+
+def specialize (t) (b : T ⊢ ∀' φ) : T ⊢ (φ/[t]) := by
+  have := Derivation.specialize' t $ provable_def.mp b;
+  apply provable_def.mpr;
+  sorry;
+
+end Theory
+
+
+namespace ProvabilityAbstraction
+
+open LO.Entailment FirstOrder Diagonalization Provability
+
+variable {L₀ L : Language}
+
+structure Refutability [L.ReferenceableBy L₀] (T₀ : Theory L₀) (T : Theory L) where
+  refu : Semisentence L₀ 1
+  refu_def {σ : Sentence L} : T ⊢ ∼σ → T₀ ⊢ refu/[⌜σ⌝]
+
+namespace Refutability
+
+variable [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L}
+
+@[coe] def rf (𝔚 : Refutability T₀ T) (σ : Sentence L) : Sentence L₀ := 𝔚.refu/[⌜σ⌝]
+instance : CoeFun (Refutability T₀ T) (fun _ ↦ Sentence L → Sentence L₀) := ⟨rf⟩
+
+end Refutability
+
+
+section
+
+variable
+  {L₀ L : Language} [L.ReferenceableBy L₀]
+  {T₀ : Theory L₀} {T : Theory L}
+
+lemma R1 {𝔚 : Refutability T₀ T} {σ : Sentence L} : T ⊢ ∼σ → T₀ ⊢ 𝔚 σ := fun h ↦ 𝔚.refu_def h
+
+lemma R1' {L : Language} [L.ReferenceableBy L] {T₀ T : Theory L}
+  {𝔚 : Refutability T₀ T} {σ : Sentence L} [T₀ ⪯ T] : T ⊢ ∼σ → T ⊢ 𝔚 σ := fun h ↦
+  WeakerThan.pbl $ R1 h
+
+end
+
+
+section
+
+variable
+  [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀]
+  {𝔚 : Refutability T₀ T}
+
+/-- This sentence is refutable. -/
+def jeroslow (𝔚 : Refutability T₀ T) [Diagonalization T₀] : Sentence L := fixedpoint T₀ 𝔚.refu
+
+lemma jeroslow_def : T₀ ⊢ jeroslow 𝔚 ⭤ 𝔚 (jeroslow 𝔚) := Diagonalization.diag _
+
+lemma jeroslow_def' [T₀ ⪯ T] : T ⊢ jeroslow 𝔚 ⭤ 𝔚 (jeroslow 𝔚) := WeakerThan.pbl $ jeroslow_def
+
+
+/-- Abstraction of formalized `𝚺₁`-completeness -/
+class Provability.FormalizedCompleteOn (𝔅 : Provability T₀ T) (σ : Sentence L) where
+  formalized_complete_on : T ⊢ σ ➝ 𝔅 σ
+alias Provability.formalized_complete_on := Provability.FormalizedCompleteOn.formalized_complete_on
+
+class Provability.SoundOn (𝔅 : Provability T₀ T) (σ : Sentence L) where
+  sound_on : T ⊢ 𝔅 σ → T ⊢ σ
+alias Provability.sound_on := Provability.SoundOn.sound_on
+
+class Refutability.SoundOn (𝔚 : Refutability T₀ T) (σ : Sentence L) where
+  sound_on : T ⊢ 𝔚 σ → T ⊢ ∼σ
+alias Refutability.sound_on := Refutability.SoundOn.sound_on
+
+end
+
+
+section
+
+variable
+  [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀]
+  {𝔚 : Refutability T₀ T}
+
+lemma unprovable_jeroslow [T₀ ⪯ T] [Consistent T] [Refutability.SoundOn 𝔚 (jeroslow 𝔚)] : T ⊬ jeroslow 𝔚 := by
+  by_contra hC;
+  apply Entailment.Consistent.not_bot (𝓢 := T);
+  . infer_instance;
+  . have : T ⊢ ∼(jeroslow 𝔚) := Refutability.sound_on $ (Entailment.iff_of_E! $ jeroslow_def') |>.mp hC;
+    exact (N!_iff_CO!.mp this) ⨀ hC;
+
+end
+
+
+section
+
+variable
+  [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀]
+  {𝔅 : Provability T₀ T} {𝔚 : Refutability T₀ T}
+
+/-- Formalized Law of Noncontradiction holds on `x` -/
+def safe (𝔅 : Provability T₀ T) (𝔚 : Refutability T₀ T) : Semisentence L 1 := “x. ¬(!𝔅.prov x ∧ !𝔚.refu x)”
+
+/-- Formalized Law of Noncontradiction -/
+def flon (𝔅 : Provability T₀ T) (𝔚 : Refutability T₀ T) : Sentence L := “∀ x, !(safe 𝔅 𝔚) x”
+
+end
+
+
+section
+
+variable
+  [L.DecidableEq] [L.ReferenceableBy L] {T₀ T : Theory L}
+  [Diagonalization T₀] [T₀ ⪯ T]
+  {𝔅 : Provability T₀ T} {𝔚 : Refutability T₀ T}
+
+local notation "𝐉" => jeroslow 𝔚
+
+lemma jeroslow_not_safe [𝔅.FormalizedCompleteOn 𝐉] : T ⊢ 𝐉 ➝ (𝔅 𝐉 ⋏ 𝔚 𝐉) := by
+  have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on;
+  have h₂ : T ⊢ 𝐉 ⭤ 𝔚 𝐉 := jeroslow_def';
+  cl_prover [h₁, h₂];
+
+/--
+  Formalized law of noncontradiction cannot be proved.
+  Alternative form of Gödel's second incompleteness theorem.
+-/
+lemma unprovable_flon [consis : Consistent T] [𝔅.FormalizedCompleteOn 𝐉] : T ⊬ flon 𝔅 𝔚 := by
+  contrapose! consis;
+  replace consis : T ⊢ ∀' safe 𝔅 𝔚 := by simpa [flon] using consis;
+  have h₁ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) := by simpa [safe] using FirstOrder.Theory.specialize _ $ consis;
+  have h₂ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on;
+  have h₃ : T ⊢ 𝐉 ⭤ 𝔚 𝐉 := jeroslow_def';
+  have h₄ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) ➝ ∼𝐉 := contra! $ by cl_prover [h₂, h₃];
+  have h₅ : T ⊢ ∼𝐉 := h₄ ⨀ h₁;
+  have h₆ : T ⊢ 𝔚 𝐉 := R1' h₅;
+  have h₇ : T ⊢ 𝔚 𝐉 ➝ 𝐉 := by cl_prover [h₃];
+  have h₈ : T ⊢ 𝐉 := h₇ ⨀ h₆;
+  exact not_consistent_iff_inconsistent.mpr <| inconsistent_iff_provable_bot.mpr $ (N!_iff_CO!.mp h₅) ⨀ h₈;
+
+end
+
+
+end ProvabilityAbstraction
+
+end LO.FirstOrder

Foundation/FirstOrder/Bootstrapping/RosserProvability.lean

@@ -128,10 +128,9 @@ variable (T)
 
 noncomputable abbrev _root_.LO.FirstOrder.Theory.rosserProvability : Provability 𝗜𝚺₁ T where
   prov := T.rosserProvable
+  prov_def := rosserProvable_D1
 
-instance [Entailment.Consistent T] : T.rosserProvability.HBL1 := ⟨rosserProvable_D1⟩
-
-instance [Entailment.Consistent T] : T.rosserProvability.Rosser := ⟨rosserProvable_rosser⟩
+instance : T.rosserProvability.Rosser := ⟨rosserProvable_rosser⟩
 
 lemma rosserProvability_def (σ : Sentence L) : T.rosserProvability σ = T.rosserPred σ := rfl