diff --git a/Incompleteness/Arith/D3.lean b/Incompleteness/Arith/D3.lean index 0c56f0e..4b4cd81 100644 --- a/Incompleteness/Arith/D3.lean +++ b/Incompleteness/Arith/D3.lean @@ -63,7 +63,7 @@ def toNumVec {n} (e : Fin n → V) : (Language.codeIn ℒₒᵣ V).SemitermVec n namespace TProof -open Language.Theory.TProof System +open Language.Theory.TProof Entailment variable (T) diff --git a/Incompleteness/Arith/DC.lean b/Incompleteness/Arith/DC.lean index c3fa2d7..1829438 100644 --- a/Incompleteness/Arith/DC.lean +++ b/Incompleteness/Arith/DC.lean @@ -10,9 +10,9 @@ namespace LO.FirstOrder.Arith open LO.Arith LO.Arith.Formalized -variable (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] +variable (T : Theory ℒₒᵣ) [𝐈𝚺₁ ⪯ T] -variable (U : Theory ℒₒᵣ) [U.Delta1Definable] [ℕ ⊧ₘ* U] [𝐑₀ ≼ U] +variable (U : Theory ℒₒᵣ) [U.Delta1Definable] [ℕ ⊧ₘ* U] [𝐑₀ ⪯ U] instance : Diagonalization T where fixpoint := fixpoint diff --git a/Incompleteness/Arith/First.lean b/Incompleteness/Arith/First.lean index ef5eaf3..257b672 100644 --- a/Incompleteness/Arith/First.lean +++ b/Incompleteness/Arith/First.lean @@ -16,7 +16,7 @@ namespace LO.FirstOrder namespace Arith -open LO.Arith LO.System LO.Arith.Formalized +open LO.Arith LO.Entailment LO.Arith.Formalized lemma re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P := by constructor @@ -28,10 +28,10 @@ lemma re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P := by (f := fun x : ℕ ↦ x ::ᵥ List.Vector.nil) (Primrec.to_comp <| Primrec.vector_cons.comp .id (.const _)) exact this.of_eq <| by intro x; symm; simpa [List.Vector.cons_get] using hφ ![x]; -variable (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable] +variable (T : Theory ℒₒᵣ) [𝐑₀ ⪯ T] [Sigma1Sound T] [T.Delta1Definable] /-- Gödel's First Incompleteness Theorem-/ -theorem goedel_first_incompleteness : ¬System.Complete T := by +theorem goedel_first_incompleteness : ¬Entailment.Complete T := by let D : ℕ → Prop := fun n : ℕ ↦ ∃ φ : SyntacticSemiformula ℒₒᵣ 1, n = ⌜φ⌝ ∧ T ⊢! ∼φ/[⌜φ⌝] have D_re : RePred D := by have : 𝚺₁-Predicate fun φ : ℕ ↦ @@ -49,13 +49,13 @@ theorem goedel_first_incompleteness : ¬System.Complete T := by simpa [Semiformula.coe_substs_eq_substs_coe₁] using re_complete (T := T) (D_re) (x := n) have : T ⊢! ∼ρ ↔ T ⊢! ρ := by simpa [D, goedelNumber'_def, quote_eq_encode] using this ⌜σ⌝ - have con : System.Consistent T := consistent_of_sigma1Sound T - refine LO.System.incomplete_iff_exists_undecidable.mpr ⟨↑ρ, ?_, ?_⟩ + have con : Entailment.Consistent T := consistent_of_sigma1Sound T + refine LO.Entailment.incomplete_iff_exists_undecidable.mpr ⟨↑ρ, ?_, ?_⟩ · intro h have : T ⊢! ∼↑ρ := by simpa [provable₀_iff] using this.mpr h - exact LO.System.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable h this) inferInstance + exact LO.Entailment.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable h this) inferInstance · intro h have : T ⊢! ↑ρ := this.mp (by simpa [provable₀_iff] using h) - exact LO.System.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable this h) inferInstance + exact LO.Entailment.not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable this h) inferInstance end LO.FirstOrder.Arith diff --git a/Incompleteness/Arith/FormalizedArithmetic.lean b/Incompleteness/Arith/FormalizedArithmetic.lean index fc20661..8989db7 100644 --- a/Incompleteness/Arith/FormalizedArithmetic.lean +++ b/Incompleteness/Arith/FormalizedArithmetic.lean @@ -58,7 +58,7 @@ variable (T : LOR.TTheory (V := V)) namespace TProof -open Language.Theory.TProof System System.FiniteContext +open Language.Theory.TProof Entailment Entailment.FiniteContext section R₀Theory @@ -295,7 +295,7 @@ noncomputable def bexIntro (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i T ⊢ φ.bex ↑n := by apply ex i suffices T ⊢ i <' n ⋏ φ^/[(i : ⌜ℒₒᵣ⌝.Term).sing] by simpa - exact System.andIntro (ltComplete T hi) b + exact Entailment.andIntro (ltComplete T hi) b lemma bex_intro! (φ : ⌜ℒₒᵣ⌝.Semiformula (0 + 1)) (n : V) {i} (hi : i < n) (b : T ⊢! φ ^/[(i : ⌜ℒₒᵣ⌝.Term).sing]) : diff --git a/Incompleteness/Arith/Second.lean b/Incompleteness/Arith/Second.lean index d06035b..319b260 100644 --- a/Incompleteness/Arith/Second.lean +++ b/Incompleteness/Arith/Second.lean @@ -83,7 +83,7 @@ namespace LO.FirstOrder.Arith open LO.Arith LO.Arith.Formalized -variable {T : Theory ℒₒᵣ} [𝐈𝚺₁ ≼ T] +variable {T : Theory ℒₒᵣ} [𝐈𝚺₁ ⪯ T] section Diagonalization @@ -101,9 +101,9 @@ lemma fixpoint_eq (θ : Semisentence ℒₒᵣ 1) : theorem diagonal (θ : Semisentence ℒₒᵣ 1) : T ⊢!. fixpoint θ ⭤ θ/[⌜fixpoint θ⌝] := - haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance + haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by - haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance inferInstance + haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance simp [models_iff] let Θ : V → Prop := fun x ↦ Semiformula.Evalbm V ![x] θ calc @@ -125,9 +125,9 @@ def multifixpoint (θ : Fin k → Semisentence ℒₒᵣ k) (i : Fin k) : Senten theorem multidiagonal (θ : Fin k → Semisentence ℒₒᵣ k) : T ⊢!. multifixpoint θ i ⭤ (Rew.substs fun j ↦ ⌜multifixpoint θ j⌝) ▹ (θ i) := - haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance + haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by - haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance inferInstance + haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance suffices V ⊧/![] (multifixpoint θ i) ↔ V ⊧/(fun i ↦ ⌜multifixpoint θ i⌝) (θ i) by simpa [models_iff] let t : Fin k → V := fun i ↦ ⌜multidiag (θ i)⌝ have ht : ∀ i, substNumerals (t i) t = ⌜multifixpoint θ i⌝ := by @@ -157,24 +157,24 @@ variable {U : Theory ℒₒᵣ} [U.Delta1Definable] theorem provableₐ_D1 {σ} : U ⊢!. σ → T ⊢!. U.bewₐ σ := by intro h - haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance + haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance apply complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by - haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance + haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance simpa [models_iff] using provableₐ_of_provable (T := U) (V := V) h theorem provableₐ_D2 {σ π} : T ⊢!. U.bewₐ (σ ➝ π) ➝ U.bewₐ σ ➝ U.bewₐ π := - haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance + haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by - haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance + haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance simp [models_iff] intro hσπ hσ exact provableₐ_iff.mpr <| (by simpa using provableₐ_iff.mp hσπ) ⨀ provableₐ_iff.mp hσ lemma provableₐ_sigma₁_complete {σ : Sentence ℒₒᵣ} (hσ : Hierarchy 𝚺 1 σ) : T ⊢!. σ ➝ U.bewₐ σ := - haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance + haveI : 𝐄𝐐 ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by - haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance inferInstance + haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V _ T inferInstance simpa [models_iff] using sigma₁_complete (T := U) (V := V) hσ theorem provableₐ_D3 {σ : Sentence ℒₒᵣ} : @@ -183,16 +183,16 @@ theorem provableₐ_D3 {σ : Sentence ℒₒᵣ} : lemma goedel_iff_unprovable_goedel : T ⊢!. U.goedelₐ ⭤ ∼U.bewₐ U.goedelₐ := by simpa [Theory.goedelₐ, Theory.bewₐ] using diagonal (∼U.provableₐ) -open LO.System LO.System.FiniteContext +open LO.Entailment LO.Entailment.FiniteContext lemma provableₐ_D2_context {Γ σ π} (hσπ : Γ ⊢[T.alt]! (U.bewₐ (σ ➝ π))) (hσ : Γ ⊢[T.alt]! U.bewₐ σ) : Γ ⊢[T.alt]! U.bewₐ π := of'! provableₐ_D2 ⨀ hσπ ⨀ hσ lemma provableₐ_D3_context {Γ σ} (hσπ : Γ ⊢[T.alt]! U.bewₐ σ) : Γ ⊢[T.alt]! U.bewₐ (U.bewₐ σ) := of'! provableₐ_D3 ⨀ hσπ -variable [ℕ ⊧ₘ* T] [𝐑₀ ≼ U] +variable [ℕ ⊧ₘ* T] [𝐑₀ ⪯ U] -omit [𝐈𝚺₁ ≼ T] in +omit [𝐈𝚺₁ ⪯ T] in lemma provableₐ_sound {σ} : T ⊢!. U.bewₐ σ → U ⊢! ↑σ := by intro h have : U.Provableₐ (⌜σ⌝ : ℕ) := by simpa [models₀_iff] using consequence_iff.mp (sound! (T := T) h) ℕ inferInstance @@ -209,7 +209,7 @@ variable (T) variable [T.Delta1Definable] -open LO.System LO.System.FiniteContext +open LO.Entailment LO.Entailment.FiniteContext local notation "𝗚" => T.goedelₐ @@ -217,15 +217,15 @@ local notation "𝗖𝗼𝗻" => T.consistentₐ local prefix:max "□" => T.bewₐ -lemma goedel_unprovable [System.Consistent T] : T ⊬ ↑𝗚 := by +lemma goedel_unprovable [Entailment.Consistent T] : T ⊬ ↑𝗚 := by intro h have hp : T ⊢! ↑□𝗚 := provableₐ_D1 h have hn : T ⊢! ∼↑□𝗚 := by simpa [provable₀_iff] using and_left! goedel_iff_unprovable_goedel ⨀ h exact not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable hp hn) inferInstance lemma not_goedel_unprovable [ℕ ⊧ₘ* T] : T ⊬ ∼↑𝗚 := fun h ↦ by - haveI : 𝐑₀ ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance - have : T ⊢!. □𝗚 := System.contra₂'! (and_right! goedel_iff_unprovable_goedel) ⨀ (by simpa [provable₀_iff] using h) + haveI : 𝐑₀ ⪯ T := Entailment.WeakerThan.trans (𝓣 := 𝐈𝚺₁) inferInstance inferInstance + have : T ⊢!. □𝗚 := Entailment.contra₂'! (and_right! goedel_iff_unprovable_goedel) ⨀ (by simpa [provable₀_iff] using h) have : T ⊢! ↑𝗚 := provableₐ_sound this exact not_consistent_iff_inconsistent.mpr (inconsistent_of_provable_of_unprovable this h) (Sound.consistent_of_satisfiable ⟨_, (inferInstance : ℕ ⊧ₘ* T)⟩) @@ -248,13 +248,13 @@ lemma consistent_iff_goedel : T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚 := by simpa [provable₀_iff] using contra₁'! (deduct'! this) /-- Gödel's Second Incompleteness Theorem-/ -theorem goedel_second_incompleteness [System.Consistent T] : T ⊬ ↑𝗖𝗼𝗻 := fun h ↦ +theorem goedel_second_incompleteness [Entailment.Consistent T] : T ⊬ ↑𝗖𝗼𝗻 := fun h ↦ goedel_unprovable T <| and_left! (consistent_iff_goedel T) ⨀ h theorem inconsistent_unprovable [ℕ ⊧ₘ* T] : T ⊬ ∼↑𝗖𝗼𝗻 := fun h ↦ not_goedel_unprovable T <| contra₀'! (and_right! (consistent_iff_goedel T)) ⨀ h -theorem inconsistent_undecidable [ℕ ⊧ₘ* T] : System.Undecidable T ↑𝗖𝗼𝗻 := by +theorem inconsistent_undecidable [ℕ ⊧ₘ* T] : Entailment.Undecidable T ↑𝗖𝗼𝗻 := by haveI : Consistent T := Sound.consistent_of_satisfiable ⟨_, (inferInstance : ℕ ⊧ₘ* T)⟩ constructor · exact goedel_second_incompleteness T diff --git a/Incompleteness/Arith/Theory.lean b/Incompleteness/Arith/Theory.lean index 97acb50..d4eb5bc 100644 --- a/Incompleteness/Arith/Theory.lean +++ b/Incompleteness/Arith/Theory.lean @@ -89,7 +89,7 @@ lemma mul_ext {a₁ a₂ b₁ b₂ : M} (ha : eql a₁ a₂) (hb : eql b₁ b₂ have := by simpa [operator_eq_eq] using ModelsTheory.models M (Theory.CobhamR0'.replace “x. &0 * &1 = &2 * x”) (a₁ :>ₙ b₁ :>ₙ fun _ ↦ a₂) exact this b₁ b₂ hb e -noncomputable instance : 𝐄𝐐 ≼ 𝐑₀' := System.Subtheory.ofAxm! <| by { +noncomputable instance : 𝐄𝐐 ⪯ 𝐑₀' := Entailment.WeakerThan.ofAxm! <| by { intro φ hp cases hp · apply complete (consequence_iff.mpr fun M _ _ s f ↦ ?_) @@ -141,29 +141,29 @@ noncomputable instance : 𝐄𝐐 ≼ 𝐑₀' := System.Subtheory.ofAxm! <| by open LO.Arith -noncomputable instance CobhamR0'.subtheoryOfCobhamR0 : 𝐑₀' ≼ 𝐑₀ := System.Subtheory.ofAxm! <| by +noncomputable instance CobhamR0'.subtheoryOfCobhamR0 : 𝐑₀' ⪯ 𝐑₀ := Entailment.WeakerThan.ofAxm! <| by intro φ hp rcases hp · apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff] · apply complete <| oRing_consequence_of.{0} _ _ <| fun M _ _ => by simp [models_iff] - case Ω₁ n m => exact System.by_axm _ (Theory.CobhamR0.Ω₁ n m) - case Ω₂ n m => exact System.by_axm _ (Theory.CobhamR0.Ω₂ n m) - case Ω₃ n m h => exact System.by_axm _ (Theory.CobhamR0.Ω₃ n m h) - case Ω₄ n => exact System.by_axm _ (Theory.CobhamR0.Ω₄ n) + case Ω₁ n m => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₁ n m) + case Ω₂ n m => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₂ n m) + case Ω₃ n m h => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₃ n m h) + case Ω₄ n => exact Entailment.by_axm _ (Theory.CobhamR0.Ω₄ n) -variable {T : Theory ℒₒᵣ} [𝐑₀ ≼ T] +variable {T : Theory ℒₒᵣ} [𝐑₀ ⪯ T] lemma add_cobhamR0' {φ} : T ⊢! φ ↔ T + 𝐑₀' ⊢! φ := by constructor - · intro h; exact System.wk! (by simp [Theory.add_def]) h + · intro h; exact Entailment.wk! (by simp [Theory.add_def]) h · intro h - exact System.StrongCut.cut! + exact Entailment.StrongCut.cut! (by rintro φ (hp | hp) - · exact System.by_axm _ hp - · have : 𝐑₀' ⊢! φ := System.by_axm _ hp - have : 𝐑₀ ⊢! φ := System.Subtheory.prf! this - exact System.Subtheory.prf! this) h + · exact Entailment.by_axm _ hp + · have : 𝐑₀' ⊢! φ := Entailment.by_axm _ hp + have : 𝐑₀ ⊢! φ := Entailment.WeakerThan.pbl this + exact Entailment.WeakerThan.pbl this) h end Arith diff --git a/Incompleteness/DC/Basic.lean b/Incompleteness/DC/Basic.lean index 6e54873..8602c3a 100644 --- a/Incompleteness/DC/Basic.lean +++ b/Incompleteness/DC/Basic.lean @@ -8,9 +8,9 @@ namespace Theory.Alt variable {L : Language} {T U : Theory L} -instance [s : T ≼ U] : T ≼ U.alt.thy := s +instance [s : T ⪯ U] : T ⪯ U.alt.thy := s -instance [s : T ≼ U] : T.alt ≼ U.alt := ⟨fun b ↦ s.prf b⟩ +instance [s : T ⪯ U] : T.alt ⪯ U.alt := ⟨fun _ b ↦ s.pbl b⟩ end Theory.Alt @@ -62,10 +62,10 @@ class Rosser (𝔅 : ProvabilityPredicate T₀ T) where section -open LO.System +open LO.Entailment variable [L.DecidableEq] - {T₀ T : Theory L} [T₀ ≼ T] + {T₀ T : Theory L} [T₀ ⪯ T] {𝔅 : ProvabilityPredicate T₀ T} [𝔅.HBL] {σ τ : Sentence L} @@ -78,22 +78,22 @@ alias Ro := Rosser.Ro def D1_shift : T ⊢!. σ → T ⊢!. (𝔅 σ) := by intro h; - apply System.Subtheory.prf! (𝓢 := T₀); + apply Entailment.WeakerThan.pbl (𝓢 := T₀.alt); apply D1 h; def D2_shift [𝔅.HBL2] : T ⊢!. 𝔅 (σ ➝ τ) ➝ (𝔅 σ) ➝ (𝔅 τ) := by - apply System.Subtheory.prf! (𝓢 := T₀); + apply Entailment.WeakerThan.pbl (𝓢 := T₀.alt); apply D2; def D3_shift [𝔅.HBL3] : T ⊢!. (𝔅 σ) ➝ 𝔅 (𝔅 σ) := by - apply System.Subtheory.prf! (𝓢 := T₀); + apply Entailment.WeakerThan.pbl (𝓢 := T₀.alt); apply D3; def FLT_shift [𝔅.FormalizedLoeb] : T ⊢!. 𝔅 ((𝔅 σ) ➝ σ) ➝ (𝔅 σ) := by - apply System.Subtheory.prf! (𝓢 := T₀); + apply Entailment.WeakerThan.pbl (𝓢 := T₀.alt); apply 𝔅.FLT; -def D2' [𝔅.HBL2] [System.ModusPonens T] : T₀ ⊢!. 𝔅 (σ ➝ τ) → T₀ ⊢!. (𝔅 σ) ➝ (𝔅 τ) := by +def D2' [𝔅.HBL2] [Entailment.ModusPonens T] : T₀ ⊢!. 𝔅 (σ ➝ τ) → T₀ ⊢!. (𝔅 σ) ➝ (𝔅 τ) := by intro h; exact D2 ⨀ h; @@ -123,7 +123,7 @@ end ProvabilityPredicate variable {T₀ T : Theory L} {𝔅 : ProvabilityPredicate T₀ T} -open LO.System +open LO.Entailment open Diagonalization open ProvabilityPredicate @@ -141,9 +141,9 @@ lemma goedel_spec : T₀ ⊢!. γ ⭤ ∼𝔅 γ := by simp [goedel, ← TransitiveRewriting.comp_app, Rew.substs_comp_substs]; rfl; -variable [T₀ ≼ T] +variable [T₀ ⪯ T] -private lemma goedel_specAux₁ : T ⊢!. γ ⭤ ∼𝔅 γ := Subtheory.prf! (𝓢 := T₀) goedel_spec +private lemma goedel_specAux₁ : T ⊢!. γ ⭤ ∼𝔅 γ := WeakerThan.pbl (𝓢 := T₀.alt) goedel_spec private lemma goedel_specAux₂ [L.DecidableEq] : T ⊢!. ∼γ ➝ 𝔅 γ := contra₂'! $ and₂'! goedel_specAux₁ @@ -156,11 +156,11 @@ open GoedelSound section First -variable [T₀ ≼ T] [Diagonalization T₀] +variable [T₀ ⪯ T] [Diagonalization T₀] local notation "γ" => 𝔅.goedel -variable [System.Consistent T] +variable [Entailment.Consistent T] theorem unprovable_goedel : T ⊬. γ := by intro h; @@ -179,14 +179,14 @@ theorem unrefutable_goedel [(k : ℕ) → DecidableEq (L.Func k)] [(k : ℕ) → inconsistent_iff_provable_bot.mpr (by simpa [provable₀_iff] using this); contradiction; -theorem goedel_independent [L.DecidableEq] [𝔅.GoedelSound] : System.Undecidable T ↑γ := by - suffices T ⊬. γ ∧ T ⊬. ∼γ by simpa [System.Undecidable, not_or, unprovable₀_iff] using this +theorem goedel_independent [L.DecidableEq] [𝔅.GoedelSound] : Entailment.Undecidable T ↑γ := by + suffices T ⊬. γ ∧ T ⊬. ∼γ by simpa [Entailment.Undecidable, not_or, unprovable₀_iff] using this constructor . apply unprovable_goedel . apply unrefutable_goedel theorem first_incompleteness [L.DecidableEq] [𝔅.GoedelSound] - : ¬System.Complete T := System.incomplete_iff_exists_undecidable.mpr ⟨γ, goedel_independent⟩ + : ¬Entailment.Complete T := Entailment.incomplete_iff_exists_undecidable.mpr ⟨γ, goedel_independent⟩ end First @@ -198,14 +198,14 @@ local notation "γ" => 𝔅.goedel lemma formalized_consistent_of_existance_unprovable : T₀ ⊢!. ∼(𝔅 σ) ➝ 𝔅.con := contra₀'! $ 𝔅.D2 ⨀ (D1 efq!) -private lemma consistency_lemma_1 [T₀ ≼ U] : (U ⊢!. 𝔅.con ➝ ∼(𝔅 σ)) ↔ (U ⊢!. (𝔅 σ) ➝ 𝔅 (∼σ)) := by +private lemma consistency_lemma_1 [T₀ ⪯ U] : (U ⊢!. 𝔅.con ➝ ∼(𝔅 σ)) ↔ (U ⊢!. (𝔅 σ) ➝ 𝔅 (∼σ)) := by constructor; . intro H; - exact contra₃'! $ imp_trans''! (Subtheory.prf! (𝓢 := T₀) formalized_consistent_of_existance_unprovable) H; + exact contra₃'! $ imp_trans''! (WeakerThan.pbl (𝓢 := T₀.alt) formalized_consistent_of_existance_unprovable) H; . intro H apply contra₀'! have : T₀ ⊢!. (𝔅 σ) ⋏ 𝔅 (∼σ) ➝ 𝔅 ⊥ := imp_trans''! prov_collect_and $ prov_distribute_imply lac!; - have : U ⊢!. (𝔅 σ) ➝ 𝔅 (∼σ) ➝ 𝔅 ⊥ := Subtheory.prf! $ and_imply_iff_imply_imply'!.mp $ this; + have : U ⊢!. (𝔅 σ) ➝ 𝔅 (∼σ) ➝ 𝔅 ⊥ := WeakerThan.pbl $ and_imply_iff_imply_imply'!.mp $ this; exact this ⨀₁ H; private lemma consistency_lemma_2 : T₀ ⊢!. ((𝔅 σ) ➝ 𝔅 (∼σ)) ➝ (𝔅 σ) ➝ 𝔅 ⊥ := by @@ -220,22 +220,22 @@ private lemma consistency_lemma_2 : T₀ ⊢!. ((𝔅 σ) ➝ 𝔅 (∼σ)) ➝ have d₃ : [(𝔅 σ), (𝔅 σ) ➝ 𝔅 (∼σ)] ⊢[T₀.alt]! 𝔅 (∼σ) := d₂ ⨀ d₁; exact ((FiniteContext.of'! this) ⨀ d₁) ⨀ d₃; -variable [T₀ ≼ T] [Diagonalization T₀] +variable [T₀ ⪯ T] [Diagonalization T₀] /-- Formalized First Incompleteness Theorem -/ theorem formalized_unprovable_goedel : T ⊢!. 𝔅.con ➝ ∼𝔅 γ := by have h₁ : T₀ ⊢!. 𝔅 γ ➝ 𝔅 (𝔅 γ) := D3; - have h₂ : T ⊢!. 𝔅 γ ➝ ∼γ := Subtheory.prf! $ contra₁'! $ and₁'! goedel_spec; + have h₂ : T ⊢!. 𝔅 γ ➝ ∼γ := WeakerThan.pbl $ contra₁'! $ and₁'! goedel_spec; have h₃ : T₀ ⊢!. 𝔅 (𝔅 γ) ➝ 𝔅 (∼γ) := prov_distribute_imply h₂; - exact Subtheory.prf! $ contra₀'! $ consistency_lemma_2 ⨀ (imp_trans''! h₁ h₃); + exact WeakerThan.pbl $ contra₀'! $ consistency_lemma_2 ⨀ (imp_trans''! h₁ h₃); theorem iff_goedel_consistency : T ⊢!. γ ⭤ 𝔅.con := - iff_trans''! goedel_specAux₁ $ iff_intro! (Subtheory.prf! (𝓢 := T₀) formalized_consistent_of_existance_unprovable) formalized_unprovable_goedel + iff_trans''! goedel_specAux₁ $ iff_intro! (WeakerThan.pbl (𝓢 := T₀.alt) formalized_consistent_of_existance_unprovable) formalized_unprovable_goedel -theorem unprovable_consistency [System.Consistent T] : T ⊬. 𝔅.con := +theorem unprovable_consistency [Entailment.Consistent T] : T ⊬. 𝔅.con := unprovable_iff! iff_goedel_consistency |>.mp $ unprovable_goedel -theorem unrefutable_consistency [System.Consistent T] [𝔅.GoedelSound] : T ⊬. ∼𝔅.con := +theorem unrefutable_consistency [Entailment.Consistent T] [𝔅.GoedelSound] : T ⊬. ∼𝔅.con := unprovable_iff! (neg_replace_iff'! $ iff_goedel_consistency) |>.mp $ unrefutable_goedel end Second @@ -258,7 +258,7 @@ lemma kreisel_spec (σ : Sentence L) : T₀ ⊢!. κ(σ) ⭤ (𝔅 (κ(σ)) ➝ simp [kreisel, ← TransitiveRewriting.comp_app, Rew.substs_comp_substs]; rfl; -private lemma kreisel_specAux₁ [T₀ ≼ T] (σ : Sentence L) : T₀ ⊢!. 𝔅 κ(σ) ➝ (𝔅 σ) := (imp_trans''! (D2 ⨀ (D1 (Subtheory.prf! <| and₁'! (kreisel_spec σ)))) D2) ⨀₁ D3 +private lemma kreisel_specAux₁ [T₀ ⪯ T] (σ : Sentence L) : T₀ ⊢!. 𝔅 κ(σ) ➝ (𝔅 σ) := (imp_trans''! (D2 ⨀ (D1 (WeakerThan.pbl <| and₁'! (kreisel_spec σ)))) D2) ⨀₁ D3 private lemma kreisel_specAux₂ (σ : Sentence L) : T₀ ⊢!. (𝔅 κ(σ) ➝ σ) ➝ κ(σ) := and₂'! (kreisel_spec σ) @@ -266,13 +266,13 @@ end KrieselSentence section LoebTheorem -variable [T₀ ≼ T] [Diagonalization T₀] [𝔅.HBL] +variable [T₀ ⪯ T] [Diagonalization T₀] [𝔅.HBL] local notation "κ(" σ ")" => 𝔅.kreisel σ theorem loeb_theorm (H : T ⊢!. (𝔅 σ) ➝ σ) : T ⊢!. σ := by - have d₁ : T ⊢!. 𝔅 (𝔅.kreisel σ) ➝ σ := imp_trans''! (Subtheory.prf! (kreisel_specAux₁ σ)) H; - have d₂ : T ⊢!. 𝔅 (𝔅.kreisel σ) := Subtheory.prf! (𝓢 := T₀) (D1 $ Subtheory.prf! (kreisel_specAux₂ σ) ⨀ d₁); + have d₁ : T ⊢!. 𝔅 (𝔅.kreisel σ) ➝ σ := imp_trans''! (WeakerThan.pbl (kreisel_specAux₁ σ)) H; + have d₂ : T ⊢!. 𝔅 (𝔅.kreisel σ) := WeakerThan.pbl (𝓢 := T₀.alt) (D1 $ WeakerThan.pbl (kreisel_specAux₂ σ) ⨀ d₁); exact d₁ ⨀ d₂; instance : 𝔅.Loeb := ⟨loeb_theorm (T := T)⟩ @@ -280,14 +280,14 @@ instance : 𝔅.Loeb := ⟨loeb_theorm (T := T)⟩ theorem formalized_loeb_theorem [L.DecidableEq] : T₀ ⊢!. 𝔅 ((𝔅 σ) ➝ σ) ➝ (𝔅 σ) := by have hκ₁ : T₀ ⊢!. 𝔅 (κ(σ)) ➝ (𝔅 σ) := kreisel_specAux₁ σ; have : T₀ ⊢!. ((𝔅 σ) ➝ σ) ➝ (𝔅 κ(σ) ➝ σ) := replace_imply_left! hκ₁; - have : T ⊢!. ((𝔅 σ) ➝ σ) ➝ κ(σ) := Subtheory.prf! (𝓢 := T₀) $ imp_trans''! this (kreisel_specAux₂ σ); + have : T ⊢!. ((𝔅 σ) ➝ σ) ➝ κ(σ) := WeakerThan.pbl (𝓢 := T₀.alt) $ imp_trans''! this (kreisel_specAux₂ σ); exact imp_trans''! (D2 ⨀ (D1 this)) hκ₁; instance [L.DecidableEq] : 𝔅.FormalizedLoeb := ⟨formalized_loeb_theorem (T := T)⟩ end LoebTheorem -variable [System.Consistent T] +variable [Entailment.Consistent T] lemma unprovable_consistency_via_loeb [𝔅.Loeb] : T ⊬. 𝔅.con := by by_contra hC; @@ -295,7 +295,7 @@ lemma unprovable_consistency_via_loeb [𝔅.Loeb] : T ⊬. 𝔅.con := by have : ¬Consistent T := not_consistent_iff_inconsistent.mpr $ inconsistent_iff_provable_bot.mpr (by simpa [provable₀_iff] using this) contradiction -variable [L.DecidableEq] [Diagonalization T₀] [T₀ ≼ T] [𝔅.HBL] [𝔅.GoedelSound] +variable [L.DecidableEq] [Diagonalization T₀] [T₀ ⪯ T] [𝔅.HBL] [𝔅.GoedelSound] lemma formalized_unprovable_not_consistency : T ⊬. 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := by @@ -308,7 +308,7 @@ lemma formalized_unrefutable_goedel : T ⊬. 𝔅.con ➝ ∼𝔅 (∼𝔅.goedel) := by by_contra hC; have : T ⊬. 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := formalized_unprovable_not_consistency; - have : T ⊢!. 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := imp_trans''! hC $ Subtheory.prf! $ and₁'! $ neg_replace_iff'! $ prov_distribute_iff $ neg_replace_iff'! iff_goedel_consistency; + have : T ⊢!. 𝔅.con ➝ ∼𝔅 (∼𝔅.con) := imp_trans''! hC $ WeakerThan.pbl $ and₁'! $ neg_replace_iff'! $ prov_distribute_iff $ neg_replace_iff'! iff_goedel_consistency; contradiction; end Loeb @@ -326,13 +326,13 @@ variable [Diagonalization T₀] [𝔅.Rosser] lemma rosser_spec : T₀ ⊢!. ρ ⭤ ∼(𝔅 ρ) := goedel_spec -private lemma rosser_specAux₁ [T₀ ≼ T] : T ⊢!. ρ ⭤ ∼(𝔅 ρ) := goedel_specAux₁ +private lemma rosser_specAux₁ [T₀ ⪯ T] : T ⊢!. ρ ⭤ ∼(𝔅 ρ) := goedel_specAux₁ end RosserSentence section -variable [Diagonalization T₀] [T₀ ≼ T] [System.Consistent T] [𝔅.Rosser] +variable [Diagonalization T₀] [T₀ ⪯ T] [Entailment.Consistent T] [𝔅.Rosser] local notation "ρ" => 𝔅.rosser @@ -340,25 +340,25 @@ lemma unprovable_rosser : T ⊬. ρ := unprovable_goedel theorem unrefutable_rosser : T ⊬. ∼ρ := by intro hnρ; - have hρ : T ⊢!. ρ := Subtheory.prf! $ (and₂'! rosser_spec) ⨀ (Ro hnρ); + have hρ : T ⊢!. ρ := WeakerThan.pbl $ (and₂'! rosser_spec) ⨀ (Ro hnρ); have : ¬Consistent T := not_consistent_iff_inconsistent.mpr $ inconsistent_iff_provable_bot.mpr <| by simpa [provable₀_iff] using (neg_equiv'!.mp hnρ) ⨀ hρ; contradiction -theorem rosser_independent : System.Undecidable T ↑ρ := by - suffices T ⊬. ρ ∧ T ⊬. ∼ρ by simpa [System.Undecidable, not_or, unprovable₀_iff] using this; +theorem rosser_independent : Entailment.Undecidable T ↑ρ := by + suffices T ⊬. ρ ∧ T ⊬. ∼ρ by simpa [Entailment.Undecidable, not_or, unprovable₀_iff] using this; constructor . apply unprovable_rosser . apply unrefutable_rosser -theorem rosser_first_incompleteness (𝔅 : ProvabilityPredicate T₀ T) [𝔅.Rosser] : ¬System.Complete T := - System.incomplete_iff_exists_undecidable.mpr ⟨𝔅.rosser, rosser_independent ⟩ +theorem rosser_first_incompleteness (𝔅 : ProvabilityPredicate T₀ T) [𝔅.Rosser] : ¬Entailment.Complete T := + Entailment.incomplete_iff_exists_undecidable.mpr ⟨𝔅.rosser, rosser_independent ⟩ omit [Diagonalization T₀] [Consistent T] /-- If `𝔅` satisfies Rosser provability condition, then `𝔅.con` is provable in `T`. -/ theorem kriesel_remark : T ⊢!. 𝔅.con := by have : T₀ ⊢!. ∼𝔅 ⊥ := Ro (neg_equiv'!.mpr (by simp)); - exact Subtheory.prf! $ this; + exact WeakerThan.pbl $ this; end diff --git a/Incompleteness/ProvabilityLogic/Basic.lean b/Incompleteness/ProvabilityLogic/Basic.lean index f587ab9..f7ba940 100644 --- a/Incompleteness/ProvabilityLogic/Basic.lean +++ b/Incompleteness/ProvabilityLogic/Basic.lean @@ -1,6 +1,6 @@ import Incompleteness.Arith.DC import Incompleteness.DC.Basic -import Foundation.Modal.Hilbert.Systems +import Foundation.Modal.Logic.WellKnown namespace LO @@ -16,12 +16,12 @@ variable [Semiterm.Operator.GoedelNumber L (Sentence L)] namespace ProvabilityLogic /-- Mapping modal prop vars to first-order sentence -/ -def Realization (α : Type u) (L) := α → FirstOrder.Sentence L +def Realization (L) := ℕ → FirstOrder.Sentence L /-- Mapping modal formulae to first-order sentence -/ def Realization.interpret {T U : FirstOrder.Theory L} - (f : Realization α L) (𝔅 : ProvabilityPredicate T U) : Formula α → FirstOrder.Sentence L + (f : Realization L) (𝔅 : ProvabilityPredicate T U) : Formula ℕ → FirstOrder.Sentence L | .atom a => f a | □φ => 𝔅 (f.interpret 𝔅 φ) | ⊥ => ⊥ @@ -29,53 +29,53 @@ def Realization.interpret variable [Semiterm.Operator.GoedelNumber L (Sentence L)] -class ArithmeticalSound (Λ : Hilbert α) (𝔅 : ProvabilityPredicate T U) where - sound : ∀ {φ}, (Λ ⊢! φ) → (∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ)) - -class ArithmeticalComplete (Λ : Hilbert α) (𝔅 : ProvabilityPredicate T U) where - complete : ∀ {φ}, (∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ)) → (Λ ⊢! φ) +class ArithmeticalSound (Λ : Modal.Logic) (𝔅 : ProvabilityPredicate T U) where + sound : ∀ {φ}, (φ ∈ Λ) → (∀ {f : Realization L}, U ⊢!. (f.interpret 𝔅 φ)) +class ArithmeticalComplete (Λ : Modal.Logic) (𝔅 : ProvabilityPredicate T U) where + complete : ∀ {φ}, (∀ {f : Realization L}, U ⊢!. (f.interpret 𝔅 φ)) → (φ ∈ Λ) section ArithmeticalSoundness -open System +open Entailment +open Modal open ProvabilityPredicate variable {L : FirstOrder.Language} [Semiterm.Operator.GoedelNumber L (Sentence L)] [L.DecidableEq] - {T U : FirstOrder.Theory L} [T ≼ U] + {T U : FirstOrder.Theory L} [T ⪯ U] {𝔅 : ProvabilityPredicate T U} -lemma arithmetical_soundness_N (h : (Hilbert.N α) ⊢! φ) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ) := by +lemma arithmetical_soundness_N (h : (Hilbert.N) ⊢! φ) : ∀ {f : Realization L}, U ⊢!. (f.interpret 𝔅 φ) := by intro f; - induction h using Deduction.inducition_with_necOnly! with - | hMaxm hp => simp at hp; - | hNec ihp => exact D1_shift ihp; - | hMdp ihpq ihp => exact ihpq ⨀ ihp; - | hImply₁ => exact imply₁!; - | hImply₂ => exact imply₂!; - | hElimContra => exact elim_contra_neg!; + induction h using Hilbert.Deduction.rec! with + | maxm hp => simp at hp; + | nec ihp => exact D1_shift ihp; + | mdp ihpq ihp => exact ihpq ⨀ ihp; + | imply₁ => exact imply₁!; + | imply₂ => exact imply₂!; + | ec => exact elim_contra_neg!; -lemma arithmetical_soundness_GL [Diagonalization T] [𝔅.HBL] (h : (Hilbert.GL α) ⊢! φ) : ∀ {f : Realization α L}, U ⊢!. (f.interpret 𝔅 φ) := by +lemma arithmetical_soundness_GL [Diagonalization T] [𝔅.HBL] (h : (Hilbert.GL) ⊢! φ) : ∀ {f : Realization L}, U ⊢!. (f.interpret 𝔅 φ) := by intro f; - induction h using Deduction.inducition_with_necOnly! with - | hMaxm hp => - rcases hp with (⟨_, _, rfl⟩ | ⟨_, rfl⟩) + induction h using Hilbert.Deduction.rec! with + | maxm hp => + rcases (by simpa using hp) with (⟨_, rfl⟩ | ⟨_, rfl⟩) . exact D2_shift; . exact FLT_shift; - | hNec ihp => exact D1_shift ihp; - | hMdp ihpq ihp => exact ihpq ⨀ ihp; - | hImply₁ => exact imply₁!; - | hImply₂ => exact imply₂!; - | hElimContra => exact elim_contra_neg!; + | nec ihp => exact D1_shift ihp; + | mdp ihpq ihp => exact ihpq ⨀ ihp; + | imply₁ => exact imply₁!; + | imply₂ => exact imply₂!; + | ec => exact elim_contra_neg!; end ArithmeticalSoundness section -instance (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : ArithmeticalSound (Hilbert.GL α) (T.standardDP T) := ⟨arithmetical_soundness_GL⟩ +instance (T : Theory ℒₒᵣ) [𝐈𝚺₁ ⪯ T] [T.Delta1Definable] : ArithmeticalSound (Logic.GL) (T.standardDP T) := ⟨arithmetical_soundness_GL⟩ end diff --git a/lake-manifest.json b/lake-manifest.json index aa5f996..bd54786 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "FormalizedFormalLogic", - "rev": "b0a8544923d55eec67001feafdbafe54b78722f1", + "rev": "86c4a9d76f8aa089ed38ea164d1b72e5f3aa7f47", "name": "arithmetization", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -15,7 +15,7 @@ "type": "git", "subDir": null, "scope": "FormalizedFormalLogic", - "rev": "4ed1d5989c1df5c310ecbc6a24f054f8a72d619e", + "rev": "9e1cfabe084ed320c9af2110cb77c7ed4f6f5e3d", "name": "foundation", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "af8c17b2c995e84c8d44e1c7592136845c590307", + "rev": "5608064d3be9600af7deea2cbb3955c2805dfc01", "name": "mathlib", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -95,7 +95,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d", + "rev": "43dc9fd41505ba34dd359550c94706b4f4abefec", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main",