From f3bc2077749f2ad41df91a9aef2c36bb0dbe2c5d Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Sun, 10 Dec 2023 18:36:14 +0900 Subject: [PATCH] remove dep arith wip --- .../Derivability/Conditions.lean | 27 +++---- .../Derivability/FirstIncompleteness.lean | 14 ++-- .../Derivability/SecondIncompleteness.lean | 77 +++++++++---------- .../Incompleteness/Derivability/Theory.lean | 4 +- 4 files changed, 60 insertions(+), 62 deletions(-) diff --git a/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean b/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean index 612b53a4..639d3fd7 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean @@ -67,14 +67,14 @@ section PrCalculus open Subformula FirstOrder.Theory Derivability1 Derivability2 Derivability3 -variable {T₀ T : Theory L} [Subtheory T₀ T] [HasProvablePred T M] +variable {T₀ T : Theory L} [Subtheory T₀ T] {M} [Structure L M] [HasProvablePred T M] variable [hD1 : Derivability1 T₀ T M] [hD2 : Derivability2 T₀ T M] [hD3 : Derivability3 T₀ T M] lemma Derivability1.D1' {σ : Sentence L} : T ⊢! σ → T ⊢! ((Pr T M)/[⸢σ⸣]) := by intro h; exact weakening $ hD1.D1 h; lemma Derivability2.D2' {σ π : Sentence L} : T ⊢! (Pr T M)/[⸢σ ⟶ π⸣] ⟶ ((Pr T M)/[⸢σ⸣] ⟶ (Pr T M)/[⸢π⸣]) := weakening hD2.D2 -lemma Derivability2.D2_iff [Subtheory T₀ T] {σ π : Sentence L} +lemma Derivability2.D2_iff {σ π : Sentence L} : T₀ ⊢! ((Pr T M)/[⸢σ ⟷ π⸣]) ⟶ ((Pr T M)/[⸢σ⸣] ⟷ (Pr T M)/[⸢π⸣]) := by have a : T₀ ⊢! (Pr T M)/[⸢σ ⟶ π⸣] ⟶ (Pr T M)/[⸢σ⸣] ⟶ (Pr T M)/[⸢π⸣] := hD2.D2; have b : T₀ ⊢! (Pr T M)/[⸢π ⟶ σ⸣] ⟶ (Pr T M)/[⸢π⸣] ⟶ (Pr T M)/[⸢σ⸣] := hD2.D2; @@ -119,22 +119,19 @@ end PrCalculus section ConsistencyFormalization -variable (T : Theory L) [HasProvablePred T M] - /-- Löb style consistency formalization -/ -@[simp] -def LConsistenncy : Sentence L := ~(Pr T M)/[⸢⊥⸣] +@[simp] def LConsistency : Sentence L := ~(Pr T M)/[⸢⊥⸣] -notation "ConL[" T "]" => LConsistenncy T +notation "Con[" T "," M "]" => LConsistency T M end ConsistencyFormalization end HasProvablePred -variable (P : ∀ (n : Fin 2), (Subsentence L n) → Prop) +variable (hDef : ∀ {n : ℕ}, (Subsentence L n) → Prop) class Diagonizable where - diag (δ : Subsentence L 1) : (P 1 δ) → ∃ (σ : Sentence L), (P 0 σ) ∧ (T ⊢! σ ⟷ ([→ ⸢σ⸣].hom δ)) + diag (δ : Subsentence L 1) : (hDef δ) → ∃ (σ : Sentence L), (hDef σ) ∧ (T ⊢! σ ⟷ δ/[⸢σ⸣]) section FixedPoints @@ -144,24 +141,24 @@ variable [Subtheory T₀ T] [HasProvablePred T M] def IsGoedelSentence (G : Sentence L) := T₀ ⊢! G ⟷ ~(Pr T M)/[⸢G⸣] -variable [hdiag : Diagonizable T₀ P] +variable [hdiag : Diagonizable T₀ hDef] -lemma existsGoedelSentence (h : P 1 (~Pr T M)) -- 可証性述語の否定がΠ₁であることの抽象化 - : ∃ (G : Sentence L), ((IsGoedelSentence T₀ T M G) ∧ (P 0 G)) := by +lemma existsGoedelSentence (h : hDef (~Pr T M)) -- 可証性述語の否定がΠ₁であることの抽象化 + : ∃ (G : Sentence L), (IsGoedelSentence T₀ T M G) ∧ (hDef G) := by have ⟨G, ⟨hH, hd⟩⟩ := hdiag.diag (~(Pr T M)) h; existsi G; simpa [IsGoedelSentence, hH, Rew.neg'] using hd; def IsHenkinSentence [Subtheory T₀ T] (H : Sentence L) := T₀ ⊢! H ⟷ (Pr T M)/[⸢H⸣] -lemma existsHenkinSentence (h : P 1 (Pr T M)) -- 可証性述語がΣ₁であることの抽象化 - : ∃ (H : Sentence L), (IsHenkinSentence T₀ T M H) ∧ (P 0 H) := by +lemma existsHenkinSentence (h : hDef (Pr T M)) -- 可証性述語がΣ₁であることの抽象化 + : ∃ (H : Sentence L), (IsHenkinSentence T₀ T M H) ∧ (hDef H) := by have ⟨H, ⟨hH, hd⟩⟩ := hdiag.diag (Pr T M) h; existsi H; simpa [IsHenkinSentence, hH] using hd; def IsKrieselSentence [Subtheory T₀ T] (K σ : Sentence L) := T₀ ⊢! K ⟷ ((Pr T M)/[⸢K⸣] ⟶ σ) lemma existsKreiselSentence (σ : Sentence L) - : ∃ (K : Sentence L), IsKrieselSentence T₀ T M K σ := by + : ∃ (K : Sentence L), (IsKrieselSentence T₀ T M K σ) := by have ⟨K, ⟨hH, hd⟩⟩ := hdiag.diag ((Pr T M)/[⸢σ⸣]) (by sorry); existsi K; simp [IsKrieselSentence, hH]; sorry; diff --git a/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean b/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean index d5863463..eef245bc 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean @@ -10,7 +10,7 @@ open FirstOrder.Theory HasProvablePred variable {L : Language} [System (Sentence L)] [Intuitionistic (Sentence L)] [GoedelNumber L (Sentence L)] variable (T₀ T : Theory L) [Subtheory T₀ T] -variable {P} [Diagonizable T₀ P] +variable {hDef} [Diagonizable T₀ hDef] variable (M) [Structure L M] variable [hPred : HasProvablePred T M] [hD1 : Derivability1 T₀ T M] @@ -18,7 +18,7 @@ local notation:max "⸢" σ "⸣" => @GoedelNumber.encode L _ _ (σ : Sentence L variable {G : Sentence L} (hG : IsGoedelSentence T₀ T M G) -variable [hConsis : Theory.Consistent T] [hSoundness : PrSoundness T M (λ _ => True)] +variable [hConsis : Theory.Consistent T] [hSoundness : PrSoundness T M (λ σ => hDef σ)] lemma GoedelSentenceUnprovablility : T ⊬! G := by by_contra hP; simp at hP; @@ -27,20 +27,20 @@ lemma GoedelSentenceUnprovablility : T ⊬! G := by have hR : T ⊢! ~G := weakening (h₂ ⨀ h₁); exact broken_consistent hP hR; -lemma GoedelSentenceUnrefutability : T ⊬! ~G := by +lemma GoedelSentenceUnrefutability (a : hDef G) : T ⊬! ~G := by by_contra hR; simp at hR; have h₁ : T ⊢! ~G ⟶ (Pr T M)/[⸢G⸣] := by simpa [Subformula.neg_neg'] using weakening $ iff_mp $ iff_contra hG; have h₂ : T ⊢! (Pr T M)/[⸢G⸣] := h₁ ⨀ hR; simp at h₂; - have h₃ : M ⊧ ((Pr T M)/[⸢G⸣]) := hSoundness.sounds (by simp) h₂; + have h₃ : M ⊧ ((Pr T M)/[⸢G⸣]) := hSoundness.sounds a h₂; have hP : T ⊢! G := hPred.spec.mp h₃; exact broken_consistent hP hR; -theorem FirstIncompleteness (a : P 1 (~Pr T M)) : Theory.Incomplete T := by - have γ := existsGoedelSentence T₀ T M P a; +theorem FirstIncompleteness (a : hDef (~Pr T M)) : Theory.Incomplete T := by + have γ := existsGoedelSentence T₀ T M hDef a; suffices ¬System.Complete T by exact ⟨this⟩; by_contra hC; cases (hC γ.choose) with | inl h => simpa using (GoedelSentenceUnprovablility T₀ T M γ.choose_spec.left); - | inr h => simpa using (GoedelSentenceUnrefutability T₀ T M γ.choose_spec.left); + | inr h => simpa using (GoedelSentenceUnrefutability T₀ T M γ.choose_spec.left γ.choose_spec.right); end LO.FirstOrder.Incompleteness diff --git a/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean b/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean index 41a290cc..247f7f13 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean @@ -4,67 +4,66 @@ import Logic.FirstOrder.Incompleteness.Derivability.FirstIncompleteness open LO.System LO.System.Intuitionistic -namespace LO.FirstOrder.Arith.Incompleteness +namespace LO.FirstOrder.Incompleteness -open FirstOrder.Theory HasProvablePred FirstIncompleteness +open FirstOrder.Theory HasProvablePred -variable (T₀ T : Theory ℒₒᵣ) [Subtheory T₀ T] -variable [Diagonizable T₀ Π 1] -variable - [HasProvablePred T] - [HasProvablePred.Definable.Sigma T 1] - [Derivability1 T₀ T] - [Derivability2 T₀ T] - [hD3 : Derivability3 T₀ T] +variable {L : Language} [System (Sentence L)] [Intuitionistic (Sentence L)] [Deduction (Sentence L)] [GoedelNumber L (Sentence L)] +variable (T₀ T : Theory L) [Subtheory T₀ T] +variable {hDef} [Diagonizable T₀ hDef] +variable {M} [Structure L M] +variable [HasProvablePred T M] [hD1 : Derivability1 T₀ T M] [hD2 : Derivability2 T₀ T M] [hD3 : Derivability3 T₀ T M] + +local notation:max "⸢" σ "⸣" => @GoedelNumber.encode L _ _ (σ : Sentence L) open Derivability1 Derivability2 Derivability3 -lemma FormalizedConsistency (σ : Sentence ℒₒᵣ) : T₀ ⊢! ~(Pr[T] ⸢σ⸣) ⟶ ConL[T] := by +lemma FormalizedConsistency (σ : Sentence L) : T₀ ⊢! ~((Pr T M)/[⸢σ⸣]) ⟶ Con[T, M] := by exact imp_contra₀ $ D2 ⨀ D1 (efq _) -variable (U : Theory ℒₒᵣ) [Subtheory T₀ U] in -private lemma extend {σ : Sentence ℒₒᵣ} - : (U ⊢! ConL[T] ⟶ ~Pr[T] ⸢σ⸣) ↔ (U ⊢! (Pr[T] ⸢σ⸣) ⟶ (Pr[T] ⸢~σ⸣)) := by +variable (U : Theory L) [Subtheory T₀ U] in +private lemma extend {σ : Sentence L} + : (U ⊢! Con[T, M] ⟶ ~(Pr T M)/[⸢σ⸣]) ↔ (U ⊢! ((Pr T M)/[⸢σ⸣]) ⟶ ((Pr T M)/[⸢~σ⸣])) := by apply Iff.intro; . intro H; exact imp_contra₃ $ imp_trans (weakening $ FormalizedConsistency T₀ T (~σ)) H; . intro H; exact imp_contra₀ $ elim_and_left_dilemma (by - have : T₀ ⊢! (Pr[T] ⸢σ⸣ ⋏ Pr[T] ⸢~σ⸣) ⟶ (Pr[T] ⸢⊥⸣) := formalized_NC' σ; + have : T₀ ⊢! ((Pr T M)/[⸢σ⸣] ⋏ (Pr T M)/[⸢~σ⸣]) ⟶ ((Pr T M)/[⸢⊥⸣]) := formalized_NC' σ; exact weakening this ) H; -variable (hG : IsGoedelSentence T₀ T G) (hGh : Hierarchy Π 1 G) - -lemma formalizedGoedelSentenceUnprovablility : T ⊢! ConL[T] ⟶ ~Pr[T] ⸢G⸣ := by - have h₁ : T ⊢! (Pr[T] ⸢G⸣) ⟶ (Pr[T] ⸢(Pr[T] ⸢G⸣)⸣) := hD3.D3'; - have h₂ : T ⊢! Pr[T] ⸢G⸣ ⟶ ~G := weakening $ imp_contra₁ $ iff_mp hG; - have h₃ : T ⊢! Pr[T] ⸢Pr[T] ⸢G⸣⸣ ⟶ Pr[T] ⸢~G⸣ := weakening $ @formalized_imp_intro T₀ T _ _ _ _ _ h₂; +lemma formalizedGoedelSentenceUnprovablility (hG : IsGoedelSentence T₀ T M G) : T ⊢! Con[T, M] ⟶ ~(Pr T M)/[⸢G⸣] := by + have h₁ : T ⊢! ((Pr T M)/[⸢G⸣]) ⟶ ((Pr T M)/[⸢((Pr T M)/[⸢G⸣])⸣]) := hD3.D3'; + simp [IsGoedelSentence] at hG; + have h₂ : T ⊢! (Pr T M)/[⸢G⸣] ⟶ ~G := weakening $ imp_contra₁ $ iff_mp hG; + have h₃ : T ⊢! (Pr T M)/[⸢(Pr T M)/[⸢G⸣]⸣] ⟶ (Pr T M)/[⸢~G⸣] := sorry; -- weakening $ @formalized_imp_intro _ _ _ _ _ T₀ T _ _ _ _ _ h₂; exact (extend T₀ T T).mpr $ imp_trans h₁ h₃; -lemma equality_GoedelSentence_Consistency : T ⊢! G ⟷ ConL[T] := by - have h₄ : T ⊢! ConL[T] ⟶ ~Pr[T] ⸢G⸣ := formalizedGoedelSentenceUnprovablility T₀ T hG; - have h₅ : T ⊢! ~Pr[T] ⸢G⸣ ⟶ ConL[T] := weakening $ FormalizedConsistency T₀ T G; +lemma equality_GoedelSentence_Consistency (hG : IsGoedelSentence T₀ T M G) : T ⊢! G ⟷ Con[T, M] := by + have h₄ : T ⊢! Con[T, M] ⟶ ~(Pr T M)/[⸢G⸣] := formalizedGoedelSentenceUnprovablility T₀ T hG; + have h₅ : T ⊢! ~(Pr T M)/[⸢G⸣] ⟶ Con[T, M] := weakening $ FormalizedConsistency T₀ T G; exact iff_trans (weakening hG) $ iff_intro h₅ h₄; -theorem LConsistencyUnprovablility [hConsis : Theory.Consistent T] : T ⊬! ConL[T] := by - have ⟨G, ⟨hG, _⟩⟩ := @existsGoedelSentence T₀ T _ _ 1 _ _; - exact iff_unprov (equality_GoedelSentence_Consistency T₀ T hG) (GoedelSentenceUnprovablility T₀ T hG); +variable [hConsis : Theory.Consistent T] [hSoundness : PrSoundness T M (λ σ => hDef σ)] +variable (a : hDef (~Pr T M)) + +theorem unprovable_consistency : T ⊬! Con[T, M] := by + have ⟨G, ⟨hG, _⟩⟩ := existsGoedelSentence T₀ T M hDef a; + exact iff_unprov (equality_GoedelSentence_Consistency T₀ T hG) (GoedelSentenceUnprovablility T₀ T M hG); -lemma Inconsistent_of_LConsistencyProvability : T ⊢! ConL[T] → (Theory.Inconsistent T) := by +lemma Inconsistent_of_LConsistencyProvability : T ⊢! Con[T, M] → (Theory.Inconsistent T) := by intro hP; - by_contra hConsis; simp at hConsis; have := hConsis.some; - suffices : T ⊬! ConL[T]; aesop; - exact LConsistencyUnprovablility T₀ T; + suffices : T ⊬! Con[T, M]; aesop; + exact unprovable_consistency T₀ T a; -theorem LConsistencyUnrefutability [hSound : SigmaOneSound T] : T ⊬! ~ConL[T] := by - have ⟨G, ⟨hG, _⟩⟩ := @existsGoedelSentence T₀ T _ _ 1 _ _; - exact iff_unprov (iff_contra $ equality_GoedelSentence_Consistency T₀ T hG) (GoedelSentenceUnrefutability T₀ T hG); +theorem unrefutable_consistency : T ⊬! (Pr T M)/[⸢⊥⸣] := by + have ⟨G, ⟨hG, hGP⟩⟩ := existsGoedelSentence T₀ T M hDef a; + simpa using iff_unprov (iff_contra $ equality_GoedelSentence_Consistency T₀ T hG) (GoedelSentenceUnrefutability T₀ T M hG hGP); -lemma NotSigmaOneSoundness_of_LConsitencyRefutability : T ⊢! ~ConL[T] → IsEmpty (SigmaOneSound T) := by +lemma NotSigmaOneSoundness_of_LConsitencyRefutability : T ⊢! ~Con[T, M] → IsEmpty (PrSoundness T M (λ σ => hDef σ)) := by intro H; - by_contra C; simp at C; have := C.some; - suffices : T ⊬! ~ConL[T]; aesop; - exact LConsistencyUnrefutability T₀ T; + suffices : T ⊬! ~Con[T, M]; aesop; + simpa using unrefutable_consistency T₀ T a; -end LO.FirstOrder.Arith.Incompleteness +end LO.FirstOrder.Incompleteness diff --git a/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean b/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean index 1a2eab1f..8faa1215 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean @@ -19,13 +19,15 @@ class Complete where class Incomplete where incomplete : ¬System.Complete T +lemma false_of_complete_incomplete [c : Complete T] [i: Incomplete T] : False := by + exact i.incomplete c.complete + class Consistent where consistent : System.Consistent T class Inconsistent where inconsistent : ¬System.Consistent T -@[simp] lemma false_of_consistent_inconsistent [c : Consistent T] [i: Inconsistent T] : False := by exact i.inconsistent c.consistent