From 1f873eb6267260fc96df9e0a3c5f6c3db3433317 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Mon, 12 Jan 2026 13:24:17 +0900 Subject: [PATCH 1/4] wip --- Foundation.lean | 1 + .../FirstOrder/Incompleteness/Jeroslow.lean | 159 ++++++++++++++++++ 2 files changed, 160 insertions(+) create mode 100644 Foundation/FirstOrder/Incompleteness/Jeroslow.lean diff --git a/Foundation.lean b/Foundation.lean index 9305f117a..a744332d0 100644 --- a/Foundation.lean +++ b/Foundation.lean @@ -68,6 +68,7 @@ import Foundation.FirstOrder.Incompleteness.Examples import Foundation.FirstOrder.Incompleteness.First import Foundation.FirstOrder.Incompleteness.GödelRosser import Foundation.FirstOrder.Incompleteness.Halting +import Foundation.FirstOrder.Incompleteness.Jeroslow import Foundation.FirstOrder.Incompleteness.Löb import Foundation.FirstOrder.Incompleteness.RestrictedProvability import Foundation.FirstOrder.Incompleteness.Second diff --git a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean new file mode 100644 index 000000000..b992f9461 --- /dev/null +++ b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean @@ -0,0 +1,159 @@ +import Foundation.FirstOrder.Bootstrapping.RosserProvability + +namespace LO + +namespace ProvabilityLogic + +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 + protected R1 {σ : 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 + + +namespace Refutability + +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 := Entailment.WeakerThan.pbl $ jeroslow_def + +class JeroslowIntended (ℜ : Refutability T₀ T) where + jeroslow_intended : T ⊢ ℜ ℜ.jeroslow → T ⊢ ∼ℜ.jeroslow +export JeroslowIntended (jeroslow_intended) + +end Refutability + + +section + +variable + [L.ReferenceableBy L] {T₀ T : Theory L} + [Diagonalization T₀] + {ℜ : Refutability T₀ T} + +lemma unprovable_jeroslow [T₀ ⪯ T] [Consistent T] [ℜ.JeroslowIntended] : T ⊬ ℜ.jeroslow := by + by_contra hC; + apply Entailment.Consistent.not_bot (𝓢 := T); + . infer_instance; + . have : T ⊢ ∼ℜ.jeroslow := Refutability.jeroslow_intended $ (Entailment.iff_of_E! $ Refutability.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} + +-- TODO: Guarantee `x` is sentence. +/-- Formalized Law of Noncontradiction holds on `x` -/ +def safeOn (𝔅 : Provability T₀ T) (ℜ : Refutability T₀ T) : Semisentence L 1 := “x. ¬(!𝔅.prov x ∧ !ℜ.refu x)” + +/-- Formalized Law of Noncontradiction -/ +def safe (𝔅 : Provability T₀ T) (ℜ : Refutability T₀ T) : Sentence L := “∀ x, !(safeOn 𝔅 ℜ) x” + +end + +end ProvabilityLogic + +end LO + + + + +namespace LO.FirstOrder + +open FirstOrder Arithmetic +open PeanoMinus ISigma0 ISigma1 Bootstrapping Derivation + +namespace Theory + +variable {V : Type*} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] +variable {L : Language} [L.Encodable] [L.LORDefinable] + +variable {T U : Theory L} [T.Δ₁] [U.Δ₁] + +def Refutable (T : Theory L) [T.Δ₁] (φ : V) : Prop := T.Provable (neg L φ) + +lemma Refutable.quote_iff {σ : Sentence L} : T.Refutable (V := V) ⌜σ⌝ ↔ T.Provable (V := V) ⌜∼σ⌝ := by + simp [Refutable, Sentence.quote_def, Semiformula.quote_def] + +noncomputable def refutable (T : Theory L) [T.Δ₁] : 𝚷-[2].Semisentence 1 := .mkPi + “φ. ∀ nφ, !(negGraph L) nφ φ → !T.provable nφ” $ by + apply Hierarchy.all_iff.mpr; + apply Hierarchy.imp_iff.mpr; + constructor; + . apply Hierarchy.strict_mono (Γ := 𝚺) (s := 1) <;> simp; + . apply Hierarchy.strict_mono (Γ := 𝚺) (s := 1) <;> simp; + +lemma refutable_defined : 𝚷-[2]-Predicate[V] T.Refutable via T.refutable := .mk fun v ↦ by + simp [Theory.refutable, Theory.Refutable]; + + +noncomputable abbrev jeroslow (T : Theory L) [T.Δ₁] : ArithmeticSentence := fixedpoint (T.refutable.val) + +private noncomputable abbrev jeroslow' (T : Theory L) [T.Δ₁] : ArithmeticSentence := (T.refutable.val)/[⌜T.jeroslow⌝] + +private lemma jeroslow'_piTwo : Hierarchy 𝚷 2 (T.jeroslow') := by definability; + +end Theory + + +namespace Arithmetic + +variable {V : Type} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] +variable {T U : ArithmeticTheory} [T.Δ₁] -- [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] + +lemma def_jeroslow [𝗜𝚺₁ ⪯ U] : U ⊢ T.jeroslow ⭤ T.refutable.val/[⌜T.jeroslow⌝] := diagonal _ + +lemma refutable_quote₀ {σ : ArithmeticSentence} : T.Refutable (V := V) ⌜σ⌝ ↔ T.Provable (V := V) ⌜∼σ⌝ := by + simp [Theory.Refutable, Sentence.quote_def, Semiformula.quote_def]; + +lemma iff_refutable_neg_provable [ℕ ⊧ₘ* U] {σ : ArithmeticSentence} : U ⊢ T.refutable.val/[⌜σ⌝] ↔ U ⊢ T.provable.val/[⌜∼σ⌝] := by + have := refutable_quote₀ (T := T) (σ := σ) (V := ℕ); + dsimp [Theory.Refutable] at this; + constructor; + . intro h; + have := T.refutable_defined (V := ℕ) |>.to_definable; + sorry; + . intro h; + have := models_of_provable (T := U) (M := ℕ) inferInstance h; + have := models_iff.mp this; + simp at this; + sorry; + +lemma jeroslow_unprovable [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ T.jeroslow := by + by_contra hC; + apply Entailment.Consistent.not_bot (𝓢 := T); + . infer_instance; + . have : T ⊢ T.refutable.val/[⌜T.jeroslow⌝] := (Entailment.iff_of_E! $ def_jeroslow) |>.mp hC; + have : T ⊢ T.provable.val/[⌜∼T.jeroslow⌝] := iff_refutable_neg_provable.mp this; + have : ℕ ⊧ₘ T.provable/[⌜∼Theory.jeroslow T⌝] := ArithmeticTheory.soundOnHierarchy T 𝚺 1 this (by definability); + have : T ⊢ ∼T.jeroslow := by simpa [models_iff] using this; + cl_prover [hC, this]; + +end Arithmetic + +end LO.FirstOrder From 13fc23b52489032de33128d6f3588a60102b1529 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Tue, 13 Jan 2026 23:36:35 +0900 Subject: [PATCH 2/4] Refutability Abstraction --- .../Bootstrapping/DerivabilityCondition.lean | 5 +- .../ProvabilityAbstraction/Basic.lean | 41 +++-- .../ProvabilityAbstraction/Refutability.lean | 142 ++++++++++++++++++ .../Bootstrapping/RosserProvability.lean | 2 +- .../FirstOrder/Incompleteness/Jeroslow.lean | 129 ++-------------- .../ProvabilityLogic/GL/Unprovability.lean | 6 +- .../ProvabilityLogic/Grz/Completeness.lean | 2 +- Foundation/ProvabilityLogic/N/Soundness.lean | 2 +- 8 files changed, 183 insertions(+), 146 deletions(-) create mode 100644 Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean diff --git a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean index 51cbcf7c8..93aed4490 100644 --- a/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean +++ b/Foundation/FirstOrder/Bootstrapping/DerivabilityCondition.lean @@ -32,11 +32,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 diff --git a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean index d07e0a411..41baa9e60 100644 --- a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean +++ b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Basic.lean @@ -19,7 +19,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 @@ -41,9 +42,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₀ ⊢ 𝔅 (σ ➝ τ) ➝ 𝔅 σ ➝ 𝔅 τ @@ -53,7 +52,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 ⊢ σ @@ -99,31 +98,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 @@ -134,7 +133,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; @@ -148,13 +147,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 @@ -182,7 +181,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; @@ -198,12 +197,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 @@ -325,12 +324,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 diff --git a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean new file mode 100644 index 000000000..a90765eb8 --- /dev/null +++ b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean @@ -0,0 +1,142 @@ +import Foundation.FirstOrder.Bootstrapping.RosserProvability + +namespace LO.FirstOrder + +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; + have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on; + have h₂ : T ⊢ 𝐉 ⭤ ℜ 𝐉 := jeroslow_def'; + dsimp [flon] at consis; + have : T ⊢ (safe 𝔅 ℜ)/[⌜𝐉⌝] := by + sorry; + have h₃ : T ⊢ ∼(𝔅 𝐉 ⋏ ℜ 𝐉) := by simpa [safe] using this; + 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 diff --git a/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean b/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean index 237406e68..f49f59bd8 100644 --- a/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean +++ b/Foundation/FirstOrder/Bootstrapping/RosserProvability.lean @@ -125,8 +125,8 @@ variable (T) noncomputable abbrev _root_.LO.FirstOrder.Theory.rosserProvability : Provability 𝗜𝚺₁ T where prov := T.rosserProvable + prov_def := rosserProvable_D1 -instance : T.rosserProvability.HBL1 := ⟨rosserProvable_D1⟩ instance : T.rosserProvability.Rosser := ⟨rosserProvable_rosser⟩ lemma rosserProvability_def (σ : Sentence L) : T.rosserProvability σ = T.rosserPred σ := rfl diff --git a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean index b992f9461..d6cb5caff 100644 --- a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean +++ b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean @@ -1,92 +1,10 @@ import Foundation.FirstOrder.Bootstrapping.RosserProvability - -namespace LO - -namespace ProvabilityLogic - -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 - protected R1 {σ : 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 - - -namespace Refutability - -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 := Entailment.WeakerThan.pbl $ jeroslow_def - -class JeroslowIntended (ℜ : Refutability T₀ T) where - jeroslow_intended : T ⊢ ℜ ℜ.jeroslow → T ⊢ ∼ℜ.jeroslow -export JeroslowIntended (jeroslow_intended) - -end Refutability - - -section - -variable - [L.ReferenceableBy L] {T₀ T : Theory L} - [Diagonalization T₀] - {ℜ : Refutability T₀ T} - -lemma unprovable_jeroslow [T₀ ⪯ T] [Consistent T] [ℜ.JeroslowIntended] : T ⊬ ℜ.jeroslow := by - by_contra hC; - apply Entailment.Consistent.not_bot (𝓢 := T); - . infer_instance; - . have : T ⊢ ∼ℜ.jeroslow := Refutability.jeroslow_intended $ (Entailment.iff_of_E! $ Refutability.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} - --- TODO: Guarantee `x` is sentence. -/-- Formalized Law of Noncontradiction holds on `x` -/ -def safeOn (𝔅 : Provability T₀ T) (ℜ : Refutability T₀ T) : Semisentence L 1 := “x. ¬(!𝔅.prov x ∧ !ℜ.refu x)” - -/-- Formalized Law of Noncontradiction -/ -def safe (𝔅 : Provability T₀ T) (ℜ : Refutability T₀ T) : Sentence L := “∀ x, !(safeOn 𝔅 ℜ) x” - -end - -end ProvabilityLogic - -end LO - - - +import Foundation.FirstOrder.Bootstrapping.ProvabilityAbstraction.Refutability namespace LO.FirstOrder open FirstOrder Arithmetic -open PeanoMinus ISigma0 ISigma1 Bootstrapping Derivation +open PeanoMinus ISigma0 ISigma1 Bootstrapping Derivation ProvabilityAbstraction namespace Theory @@ -111,48 +29,25 @@ noncomputable def refutable (T : Theory L) [T.Δ₁] : 𝚷-[2].Semisentence 1 : lemma refutable_defined : 𝚷-[2]-Predicate[V] T.Refutable via T.refutable := .mk fun v ↦ by simp [Theory.refutable, Theory.Refutable]; - -noncomputable abbrev jeroslow (T : Theory L) [T.Δ₁] : ArithmeticSentence := fixedpoint (T.refutable.val) - -private noncomputable abbrev jeroslow' (T : Theory L) [T.Δ₁] : ArithmeticSentence := (T.refutable.val)/[⌜T.jeroslow⌝] - -private lemma jeroslow'_piTwo : Hierarchy 𝚷 2 (T.jeroslow') := by definability; +noncomputable def standardRefutability (T : ArithmeticTheory) [T.Δ₁] : Refutability 𝗜𝚺₁ T where + refu := T.refutable.val + refu_def {σ} h := by sorry; end Theory +open ProvabilityAbstraction + namespace Arithmetic variable {V : Type} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] variable {T U : ArithmeticTheory} [T.Δ₁] -- [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] -lemma def_jeroslow [𝗜𝚺₁ ⪯ U] : U ⊢ T.jeroslow ⭤ T.refutable.val/[⌜T.jeroslow⌝] := diagonal _ - -lemma refutable_quote₀ {σ : ArithmeticSentence} : T.Refutable (V := V) ⌜σ⌝ ↔ T.Provable (V := V) ⌜∼σ⌝ := by - simp [Theory.Refutable, Sentence.quote_def, Semiformula.quote_def]; - -lemma iff_refutable_neg_provable [ℕ ⊧ₘ* U] {σ : ArithmeticSentence} : U ⊢ T.refutable.val/[⌜σ⌝] ↔ U ⊢ T.provable.val/[⌜∼σ⌝] := by - have := refutable_quote₀ (T := T) (σ := σ) (V := ℕ); - dsimp [Theory.Refutable] at this; - constructor; - . intro h; - have := T.refutable_defined (V := ℕ) |>.to_definable; - sorry; - . intro h; - have := models_of_provable (T := U) (M := ℕ) inferInstance h; - have := models_iff.mp this; - simp at this; - sorry; - -lemma jeroslow_unprovable [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ T.jeroslow := by - by_contra hC; - apply Entailment.Consistent.not_bot (𝓢 := T); - . infer_instance; - . have : T ⊢ T.refutable.val/[⌜T.jeroslow⌝] := (Entailment.iff_of_E! $ def_jeroslow) |>.mp hC; - have : T ⊢ T.provable.val/[⌜∼T.jeroslow⌝] := iff_refutable_neg_provable.mp this; - have : ℕ ⊧ₘ T.provable/[⌜∼Theory.jeroslow T⌝] := ArithmeticTheory.soundOnHierarchy T 𝚺 1 this (by definability); - have : T ⊢ ∼T.jeroslow := by simpa [models_iff] using this; - cl_prover [hC, this]; +lemma unprovable_jeroslow [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ jeroslow (T.standardRefutability) := by + apply @ProvabilityAbstraction.unprovable_jeroslow (ℜ := T.standardRefutability) _ _ _ _ _ _ _ (by sorry); + +lemma unprovable_formalized_law_of_noncontradiction [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ flon (T.standardProvability) (T.standardRefutability) := by + apply @ProvabilityAbstraction.unprovable_flon (𝔅 := T.standardProvability) (ℜ := T.standardRefutability) _ _ _ _ _ _ _ (by sorry) (by sorry); end Arithmetic diff --git a/Foundation/ProvabilityLogic/GL/Unprovability.lean b/Foundation/ProvabilityLogic/GL/Unprovability.lean index b59522664..d221cd20d 100644 --- a/Foundation/ProvabilityLogic/GL/Unprovability.lean +++ b/Foundation/ProvabilityLogic/GL/Unprovability.lean @@ -14,7 +14,7 @@ variable {L : Language} [L.ReferenceableBy L] [DecidableEq (Sentence L)] def Provability.indep (𝔅 : Provability T₀ T) (σ : Sentence L) : Sentence L := ∼(𝔅 σ) ⋏ ∼(𝔅 (∼σ)) -lemma indep_distribute [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ 𝔅.indep σ ➝ 𝔅.indep π := by +lemma indep_distribute [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ 𝔅.indep σ ➝ 𝔅.indep π := by apply CKK!_of_C!_of_C!; . apply contra!; apply WeakerThan.pbl (𝓢 := T₀); @@ -25,14 +25,14 @@ lemma indep_distribute [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ apply prov_distribute_imply; cl_prover [h]; -lemma indep_iff_distribute_inside [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : +lemma indep_iff_distribute_inside [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ 𝔅.indep σ ⭤ 𝔅.indep π := by apply K!_intro . exact indep_distribute $ h; . apply indep_distribute; cl_prover [h]; -lemma indep_iff_distribute [𝔅.HBL1] [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : +lemma indep_iff_distribute [𝔅.HBL2] (h : T ⊢ σ ⭤ π) : T ⊢ 𝔅.indep σ ↔ T ⊢ 𝔅.indep π := by constructor; . intro H; exact K!_left (indep_iff_distribute_inside h) ⨀ H; diff --git a/Foundation/ProvabilityLogic/Grz/Completeness.lean b/Foundation/ProvabilityLogic/Grz/Completeness.lean index eddcc6110..e99499a4f 100644 --- a/Foundation/ProvabilityLogic/Grz/Completeness.lean +++ b/Foundation/ProvabilityLogic/Grz/Completeness.lean @@ -33,7 +33,7 @@ variable {L : Language} [L.ReferenceableBy L] [L.DecidableEq] namespace Realization -variable {𝔅 : Provability T₀ T} [𝔅.HBL1] {f : Realization 𝔅} {A B : Modal.Formula _} +variable {𝔅 : Provability T₀ T} {f : Realization 𝔅} {A B : Modal.Formula _} def strongInterpret (f : Realization 𝔅) : Formula ℕ → Sentence L | .atom a => f a diff --git a/Foundation/ProvabilityLogic/N/Soundness.lean b/Foundation/ProvabilityLogic/N/Soundness.lean index e38449e00..d3815c9dc 100644 --- a/Foundation/ProvabilityLogic/N/Soundness.lean +++ b/Foundation/ProvabilityLogic/N/Soundness.lean @@ -12,7 +12,7 @@ open FirstOrder.ProvabilityAbstraction variable {L : FirstOrder.Language} [L.ReferenceableBy L] [L.DecidableEq] {T U : FirstOrder.Theory L} [T ⪯ U] - {𝔅 : Provability T U} [𝔅.HBL1] + {𝔅 : Provability T U} lemma N.arithmetical_soundness (h : Modal.N ⊢ A) {f : Realization 𝔅} : U ⊢ f A := by induction h using Hilbert.Normal.rec! with From cbab8504000e7bf9027c5f351d0517c64bcea62e Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Wed, 14 Jan 2026 11:34:02 +0900 Subject: [PATCH 3/4] =?UTF-8?q?`=E2=84=9C`=20to=20`=F0=9D=94=9A`?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- .../ProvabilityAbstraction/Refutability.lean | 52 +++++++++---------- .../FirstOrder/Incompleteness/Jeroslow.lean | 4 +- 2 files changed, 28 insertions(+), 28 deletions(-) diff --git a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean index a90765eb8..497a5b6f9 100644 --- a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean +++ b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean @@ -16,7 +16,7 @@ namespace Refutability variable [L.ReferenceableBy L₀] {T₀ : Theory L₀} {T : Theory L} -@[coe] def rf (ℜ : Refutability T₀ T) (σ : Sentence L) : Sentence L₀ := ℜ.refu/[⌜σ⌝] +@[coe] def rf (𝔚 : Refutability T₀ T) (σ : Sentence L) : Sentence L₀ := 𝔚.refu/[⌜σ⌝] instance : CoeFun (Refutability T₀ T) (fun _ ↦ Sentence L → Sentence L₀) := ⟨rf⟩ end Refutability @@ -28,10 +28,10 @@ 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 {𝔚 : 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 ↦ + {𝔚 : Refutability T₀ T} {σ : Sentence L} [T₀ ⪯ T] : T ⊢ ∼σ → T ⊢ 𝔚 σ := fun h ↦ WeakerThan.pbl $ R1 h end @@ -42,14 +42,14 @@ section variable [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] - {ℜ : Refutability T₀ T} + {𝔚 : Refutability T₀ T} /-- This sentence is refutable. -/ -def jeroslow (ℜ : Refutability T₀ T) [Diagonalization T₀] : Sentence L := fixedpoint T₀ ℜ.refu +def jeroslow (𝔚 : Refutability T₀ T) [Diagonalization T₀] : Sentence L := fixedpoint T₀ 𝔚.refu -lemma jeroslow_def : T₀ ⊢ jeroslow ℜ ⭤ ℜ (jeroslow ℜ) := Diagonalization.diag _ +lemma jeroslow_def : T₀ ⊢ jeroslow 𝔚 ⭤ 𝔚 (jeroslow 𝔚) := Diagonalization.diag _ -lemma jeroslow_def' [T₀ ⪯ T] : T ⊢ jeroslow ℜ ⭤ ℜ (jeroslow ℜ) := WeakerThan.pbl $ jeroslow_def +lemma jeroslow_def' [T₀ ⪯ T] : T ⊢ jeroslow 𝔚 ⭤ 𝔚 (jeroslow 𝔚) := WeakerThan.pbl $ jeroslow_def /-- Abstraction of formalized `𝚺₁`-completeness -/ @@ -61,8 +61,8 @@ 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 ⊢ ∼σ +class Refutability.SoundOn (𝔚 : Refutability T₀ T) (σ : Sentence L) where + sound_on : T ⊢ 𝔚 σ → T ⊢ ∼σ alias Refutability.sound_on := Refutability.SoundOn.sound_on end @@ -73,13 +73,13 @@ section variable [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] - {ℜ : Refutability T₀ T} + {𝔚 : Refutability T₀ T} -lemma unprovable_jeroslow [T₀ ⪯ T] [Consistent T] [Refutability.SoundOn ℜ (jeroslow ℜ)] : T ⊬ jeroslow ℜ := by +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; + . have : T ⊢ ∼(jeroslow 𝔚) := Refutability.sound_on $ (Entailment.iff_of_E! $ jeroslow_def') |>.mp hC; exact (N!_iff_CO!.mp this) ⨀ hC; end @@ -90,13 +90,13 @@ section variable [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] - {𝔅 : Provability T₀ T} {ℜ : Refutability T₀ 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)” +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” +def flon (𝔅 : Provability T₀ T) (𝔚 : Refutability T₀ T) : Sentence L := “∀ x, !(safe 𝔅 𝔚) x” end @@ -106,31 +106,31 @@ section variable [L.DecidableEq] [L.ReferenceableBy L] {T₀ T : Theory L} [Diagonalization T₀] [T₀ ⪯ T] - {𝔅 : Provability T₀ T} {ℜ : Refutability T₀ T} + {𝔅 : Provability T₀ T} {𝔚 : Refutability T₀ T} -local notation "𝐉" => jeroslow ℜ +local notation "𝐉" => jeroslow 𝔚 -lemma jeroslow_not_safe [𝔅.FormalizedCompleteOn 𝐉] : T ⊢ 𝐉 ➝ (𝔅 𝐉 ⋏ ℜ 𝐉) := by +lemma jeroslow_not_safe [𝔅.FormalizedCompleteOn 𝐉] : T ⊢ 𝐉 ➝ (𝔅 𝐉 ⋏ 𝔚 𝐉) := by have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on; - have h₂ : T ⊢ 𝐉 ⭤ ℜ 𝐉 := jeroslow_def'; + 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 +lemma unprovable_flon [consis : Consistent T] [𝔅.FormalizedCompleteOn 𝐉] : T ⊬ flon 𝔅 𝔚 := by contrapose! consis; have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on; - have h₂ : T ⊢ 𝐉 ⭤ ℜ 𝐉 := jeroslow_def'; + have h₂ : T ⊢ 𝐉 ⭤ 𝔚 𝐉 := jeroslow_def'; dsimp [flon] at consis; - have : T ⊢ (safe 𝔅 ℜ)/[⌜𝐉⌝] := by + have : T ⊢ (safe 𝔅 𝔚)/[⌜𝐉⌝] := by sorry; - have h₃ : T ⊢ ∼(𝔅 𝐉 ⋏ ℜ 𝐉) := by simpa [safe] using this; - have h₄ : T ⊢ ∼(𝔅 𝐉 ⋏ ℜ 𝐉) ➝ ∼𝐉 := contra! $ by cl_prover [h₁, h₂]; + have h₃ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) := by simpa [safe] using this; + 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 ⊢ 𝔚 𝐉 := 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₈; diff --git a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean index d6cb5caff..1e791bb15 100644 --- a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean +++ b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean @@ -44,10 +44,10 @@ variable {V : Type} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] variable {T U : ArithmeticTheory} [T.Δ₁] -- [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] lemma unprovable_jeroslow [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ jeroslow (T.standardRefutability) := by - apply @ProvabilityAbstraction.unprovable_jeroslow (ℜ := T.standardRefutability) _ _ _ _ _ _ _ (by sorry); + apply @ProvabilityAbstraction.unprovable_jeroslow (𝔚 := T.standardRefutability) _ _ _ _ _ _ _ (by sorry); lemma unprovable_formalized_law_of_noncontradiction [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ flon (T.standardProvability) (T.standardRefutability) := by - apply @ProvabilityAbstraction.unprovable_flon (𝔅 := T.standardProvability) (ℜ := T.standardRefutability) _ _ _ _ _ _ _ (by sorry) (by sorry); + apply @ProvabilityAbstraction.unprovable_flon (𝔅 := T.standardProvability) (𝔚 := T.standardRefutability) _ _ _ _ _ _ _ (by sorry) (by sorry); end Arithmetic From 9580bec7422562e0617846beea59566b282a0b18 Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Wed, 14 Jan 2026 12:48:50 +0900 Subject: [PATCH 4/4] wip --- .../ProvabilityAbstraction/Refutability.lean | 43 +++++++++++++++---- .../FirstOrder/Incompleteness/Jeroslow.lean | 40 +++++++++++++---- 2 files changed, 65 insertions(+), 18 deletions(-) diff --git a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean index 497a5b6f9..4c64debff 100644 --- a/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean +++ b/Foundation/FirstOrder/Bootstrapping/ProvabilityAbstraction/Refutability.lean @@ -2,6 +2,33 @@ 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 @@ -121,16 +148,14 @@ lemma jeroslow_not_safe [𝔅.FormalizedCompleteOn 𝐉] : T ⊢ 𝐉 ➝ (𝔅 -/ lemma unprovable_flon [consis : Consistent T] [𝔅.FormalizedCompleteOn 𝐉] : T ⊬ flon 𝔅 𝔚 := by contrapose! consis; - have h₁ : T ⊢ 𝐉 ➝ 𝔅 𝐉 := Provability.formalized_complete_on; - have h₂ : T ⊢ 𝐉 ⭤ 𝔚 𝐉 := jeroslow_def'; - dsimp [flon] at consis; - have : T ⊢ (safe 𝔅 𝔚)/[⌜𝐉⌝] := by - sorry; - have h₃ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) := by simpa [safe] using this; - have h₄ : T ⊢ ∼(𝔅 𝐉 ⋏ 𝔚 𝐉) ➝ ∼𝐉 := contra! $ by cl_prover [h₁, h₂]; - have h₅ : T ⊢ ∼𝐉 := h₄ ⨀ h₃; + 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 ⊢ 𝔚 𝐉 ➝ 𝐉 := 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₈; diff --git a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean index 1e791bb15..697d96613 100644 --- a/Foundation/FirstOrder/Incompleteness/Jeroslow.lean +++ b/Foundation/FirstOrder/Incompleteness/Jeroslow.lean @@ -18,20 +18,24 @@ def Refutable (T : Theory L) [T.Δ₁] (φ : V) : Prop := T.Provable (neg L φ) lemma Refutable.quote_iff {σ : Sentence L} : T.Refutable (V := V) ⌜σ⌝ ↔ T.Provable (V := V) ⌜∼σ⌝ := by simp [Refutable, Sentence.quote_def, Semiformula.quote_def] -noncomputable def refutable (T : Theory L) [T.Δ₁] : 𝚷-[2].Semisentence 1 := .mkPi +noncomputable def refutable (T : Theory L) [T.Δ₁] : 𝚺₁.Semisentence 1 := .mkSigma “φ. ∀ nφ, !(negGraph L) nφ φ → !T.provable nφ” $ by - apply Hierarchy.all_iff.mpr; + sorry; + /- + -- apply Hierarchy.all_iff.mpr; apply Hierarchy.imp_iff.mpr; constructor; . apply Hierarchy.strict_mono (Γ := 𝚺) (s := 1) <;> simp; . apply Hierarchy.strict_mono (Γ := 𝚺) (s := 1) <;> simp; + -/ -lemma refutable_defined : 𝚷-[2]-Predicate[V] T.Refutable via T.refutable := .mk fun v ↦ by +lemma refutable_defined :𝚺₁-Predicate[V] T.Refutable via T.refutable := .mk fun v ↦ by simp [Theory.refutable, Theory.Refutable]; noncomputable def standardRefutability (T : ArithmeticTheory) [T.Δ₁] : Refutability 𝗜𝚺₁ T where refu := T.refutable.val - refu_def {σ} h := by sorry; + refu_def {σ} h := by + sorry; end Theory @@ -43,11 +47,29 @@ namespace Arithmetic variable {V : Type} [ORingStructure V] [V ⊧ₘ* 𝗜𝚺₁] variable {T U : ArithmeticTheory} [T.Δ₁] -- [𝗜𝚺₁ ⪯ T] [𝗜𝚺₁ ⪯ U] -lemma unprovable_jeroslow [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ jeroslow (T.standardRefutability) := by - apply @ProvabilityAbstraction.unprovable_jeroslow (𝔚 := T.standardRefutability) _ _ _ _ _ _ _ (by sorry); - -lemma unprovable_formalized_law_of_noncontradiction [ℕ ⊧ₘ* T] [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] : T ⊬ flon (T.standardProvability) (T.standardRefutability) := by - apply @ProvabilityAbstraction.unprovable_flon (𝔅 := T.standardProvability) (𝔚 := T.standardRefutability) _ _ _ _ _ _ _ (by sorry) (by sorry); +@[simp] +lemma jeroslow_sigmaOne : Hierarchy 𝚺 1 (jeroslow (Theory.standardRefutability T)) := by + dsimp [jeroslow, Diagonalization, Diagonalization.fixedpoint, fixedpoint]; + sorry; + +instance : T.standardRefutability.SoundOn (jeroslow T.standardRefutability) := by + constructor; + intro h; + simp [Theory.standardRefutability, Refutability.rf] at h; + sorry; + +instance [𝗜𝚺₁ ⪯ T] : T.standardProvability.FormalizedCompleteOn (jeroslow T.standardRefutability) := by + constructor; + apply Entailment.WeakerThan.pbl (𝓢 := 𝗜𝚺₁); + apply provable_sigma_one_complete; + simp; + +theorem unprovable_jeroslow [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] + : T ⊬ jeroslow (T.standardRefutability) := ProvabilityAbstraction.unprovable_jeroslow + +theorem unprovable_formalized_law_of_noncontradiction + [𝗜𝚺₁ ⪯ T] [T.SoundOnHierarchy 𝚺 1] + : T ⊬ flon (T.standardProvability) (T.standardRefutability) := ProvabilityAbstraction.unprovable_flon end Arithmetic