From 18b3d196c7f75e4101827cba9b11563c3f70d6ce Mon Sep 17 00:00:00 2001 From: SnO2WMaN Date: Fri, 24 Nov 2023 02:19:28 +0900 Subject: [PATCH] tinyfix --- .../Incompleteness/Derivability/Conditions.lean | 14 ++++++++------ .../Derivability/FirstIncompleteness.lean | 4 +++- .../Incompleteness/Derivability/LoebWithIT2.lean | 6 ++++-- .../Derivability/LoebWithoutIT2.lean | 4 +++- .../Derivability/SecondIncompleteness.lean | 6 ++++-- .../Incompleteness/Derivability/Theory.lean | 13 ++++++++++++- 6 files changed, 34 insertions(+), 13 deletions(-) diff --git a/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean b/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean index 1f28d79c..fb4a90b1 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/Conditions.lean @@ -3,6 +3,8 @@ import Logic.FirstOrder.Incompleteness.Derivability.Theory notation "Σ" => Bool.true notation "Π" => Bool.false +open LO.System + namespace LO.FirstOrder.Arith variable (T₀ T: Theory ℒₒᵣ) @@ -53,14 +55,14 @@ section PrCalculus open Subformula FirstOrder.Theory Derivability1 Derivability2 Derivability3 -variable {T₀ T : Theory ℒₒᵣ} [SubTheory T₀ T] [HasProvablePred T] +variable {T₀ T : Theory ℒₒᵣ} [Subtheory T₀ T] [HasProvablePred T] variable [hD1 : Derivability1 T₀ T] [hD2 : Derivability2 T₀ T] [hD3 : Derivability3 T₀ T] [hFC : FormalizedCompleteness T₀ T b n] lemma Derivability1.D1' {σ : Sentence ℒₒᵣ} : T ⊢! σ → T ⊢! (Pr[T] ⸢σ⸣) := by intro h; exact weakening $ hD1.D1 h; lemma Derivability2.D2' {σ π : Sentence ℒₒᵣ} : T ⊢! (Pr[T] ⸢σ ⟶ π⸣) ⟶ ((Pr[T] ⸢σ⸣) ⟶ (Pr[T] ⸢π⸣)) := weakening hD2.D2 -lemma Derivability2.D2_iff [SubTheory T₀ T] [hd : Derivability2 T₀ T] {σ π : Sentence ℒₒᵣ} : T₀ ⊢! (Pr[T] ⸢σ ⟷ π⸣) ⟶ ((Pr[T] ⸢σ⸣) ⟷ (Pr[T] ⸢π⸣)) := by +lemma Derivability2.D2_iff [Subtheory T₀ T] [hd : Derivability2 T₀ T] {σ π : Sentence ℒₒᵣ} : T₀ ⊢! (Pr[T] ⸢σ ⟷ π⸣) ⟶ ((Pr[T] ⸢σ⸣) ⟷ (Pr[T] ⸢π⸣)) := by sorry; -- have a := @Derivability2.D2 T₀ T _ _ _ σ π; -- have b := @Derivability2.D2 T₀ T _ _ _ π σ; @@ -122,9 +124,9 @@ section FixedPoints open HasProvablePred -variable (T₀ T : Theory ℒₒᵣ) [HasProvablePred T] [SubTheory T₀ T] {n} +variable (T₀ T : Theory ℒₒᵣ) [HasProvablePred T] [Subtheory T₀ T] {n} -def IsGoedelSentence [SubTheory T₀ T] (G : Sentence ℒₒᵣ) := T₀ ⊢! G ⟷ ~(Pr[T] ⸢G⸣) +def IsGoedelSentence [Subtheory T₀ T] (G : Sentence ℒₒᵣ) := T₀ ⊢! G ⟷ ~(Pr[T] ⸢G⸣) lemma existsGoedelSentence [hdiag : Diagonizable T₀ Π n] [hdef : Definable.Sigma T n] @@ -132,7 +134,7 @@ lemma existsGoedelSentence have ⟨G, ⟨hH, hd⟩⟩ := hdiag.diag (~ProvablePred T) (Hierarchy.neg hdef.definable); existsi G; simpa [IsGoedelSentence, hH, Rew.neg'] using hd; -def IsHenkinSentence [SubTheory T₀ T] (H : Sentence ℒₒᵣ) := T₀ ⊢! H ⟷ (Pr[T] ⸢H⸣) +def IsHenkinSentence [Subtheory T₀ T] (H : Sentence ℒₒᵣ) := T₀ ⊢! H ⟷ (Pr[T] ⸢H⸣) lemma existsHenkinSentence [hdiag : Diagonizable T₀ Σ n] [hdef : Definable.Sigma T n] @@ -140,7 +142,7 @@ lemma existsHenkinSentence have ⟨H, ⟨hH, hd⟩⟩ := hdiag.diag (ProvablePred T) hdef.definable; existsi H; simpa [IsHenkinSentence, hH] using hd; -def IsKrieselSentence [SubTheory T₀ T] (K σ : Sentence ℒₒᵣ) := T₀ ⊢! K ⟷ ((Pr[T] ⸢K⸣) ⟶ σ) +def IsKrieselSentence [Subtheory T₀ T] (K σ : Sentence ℒₒᵣ) := T₀ ⊢! K ⟷ ((Pr[T] ⸢K⸣) ⟶ σ) lemma existsKreiselSentence [hdef : Definable.Sigma T n] (σ) : ∃ (K : Sentence ℒₒᵣ), IsKrieselSentence T₀ T K σ := by sorry diff --git a/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean b/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean index 94de3014..f7aaa34b 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean @@ -1,11 +1,13 @@ import Logic.FirstOrder.Incompleteness.Derivability.Theory import Logic.FirstOrder.Incompleteness.Derivability.Conditions +open LO.System + namespace LO.FirstOrder.Arith.Incompleteness open FirstOrder.Theory HasProvablePred -variable (T₀ T : Theory ℒₒᵣ) [SubTheory T₀ T] +variable (T₀ T : Theory ℒₒᵣ) [Subtheory T₀ T] variable [Diagonizable T₀ Π 1] variable [hPred : HasProvablePred T] diff --git a/Logic/FirstOrder/Incompleteness/Derivability/LoebWithIT2.lean b/Logic/FirstOrder/Incompleteness/Derivability/LoebWithIT2.lean index 7705ed02..eb7149e4 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/LoebWithIT2.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/LoebWithIT2.lean @@ -3,11 +3,13 @@ import Logic.FirstOrder.Incompleteness.Derivability.Conditions import Logic.FirstOrder.Incompleteness.Derivability.FirstIncompleteness import Logic.FirstOrder.Incompleteness.Derivability.SecondIncompleteness +open LO.System + namespace LO.FirstOrder.Arith.Incompleteness open FirstOrder.Theory HasProvablePred -variable (T₀ T : Theory ℒₒᵣ) [hSub : SubTheory T₀ T] +variable (T₀ T : Theory ℒₒᵣ) [hSub : Subtheory T₀ T] variable [Diagonizable T₀ Σ 1] [Diagonizable T₀ Π 1] variable [HasProvablePred T] @@ -25,7 +27,7 @@ variable (σ) /-- Löb's Theorem *with* 2nd Incompleteness Theorem -/ theorem LoebTheorem : (T ⊢! σ) ↔ (T ⊢! ((Pr[T] ⸢σ⸣) ⟶ σ)) := by - have : SubTheory T₀ (T ∪ {~σ}) := SubTheory.instCoeSubTheoryForAllSentenceUnionTheoryInstUnionSetSingletonInstSingletonSet.coe hSub (~σ); + have : Subtheory T₀ (T ∪ {~σ}) := by sorry; have : Derivability1 T₀ (T ∪ {~σ}) := by sorry; have : Derivability2 T₀ (T ∪ {~σ}) := by sorry; have : Derivability3 T₀ (T ∪ {~σ}) := by sorry; diff --git a/Logic/FirstOrder/Incompleteness/Derivability/LoebWithoutIT2.lean b/Logic/FirstOrder/Incompleteness/Derivability/LoebWithoutIT2.lean index 9f7e2afe..f8140629 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/LoebWithoutIT2.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/LoebWithoutIT2.lean @@ -2,12 +2,14 @@ import Logic.FirstOrder.Incompleteness.Derivability.Theory import Logic.FirstOrder.Incompleteness.Derivability.Conditions import Logic.FirstOrder.Incompleteness.Derivability.FirstIncompleteness +open LO.System + namespace LO.FirstOrder.Arith.Incompleteness open FirstOrder.Theory HasProvablePred FirstIncompleteness open Derivability1 Derivability2 Derivability3 -variable (T₀ T : Theory ℒₒᵣ) [SubTheory T₀ T] +variable (T₀ T : Theory ℒₒᵣ) [Subtheory T₀ T] variable [Diagonizable T₀ Σ 1] [Diagonizable T₀ Π 1] variable [hConsis : Theory.Consistent T] diff --git a/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean b/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean index 00f759dd..a37950bd 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/SecondIncompleteness.lean @@ -2,11 +2,13 @@ import Logic.FirstOrder.Incompleteness.Derivability.Theory import Logic.FirstOrder.Incompleteness.Derivability.Conditions import Logic.FirstOrder.Incompleteness.Derivability.FirstIncompleteness +open LO.System + namespace LO.FirstOrder.Arith.Incompleteness open FirstOrder.Theory HasProvablePred FirstIncompleteness -variable (T₀ T : Theory ℒₒᵣ) [SubTheory T₀ T] +variable (T₀ T : Theory ℒₒᵣ) [Subtheory T₀ T] variable [Diagonizable T₀ Π 1] variable [HasProvablePred T] @@ -20,7 +22,7 @@ open Derivability1 Derivability2 Derivability3 lemma FormalizedConsistency (σ : Sentence ℒₒᵣ) : T₀ ⊢! ~(Pr[T] ⸢σ⸣) ⟶ ConL[T] := by exact imply_contra₀ $ MP D2 $ D1 EFQ -variable (U : Theory ℒₒᵣ) [SubTheory T₀ U] in +variable (U : Theory ℒₒᵣ) [Subtheory T₀ U] in private lemma extend {σ : Sentence ℒₒᵣ} : (U ⊢! ConL[T] ⟶ ~Pr[T] ⸢σ⸣) ↔ (U ⊢! (Pr[T] ⸢σ⸣) ⟶ (Pr[T] ⸢~σ⸣)) := by apply Iff.intro; diff --git a/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean b/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean index 132b10eb..90630e60 100644 --- a/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean +++ b/Logic/FirstOrder/Incompleteness/Derivability/Theory.lean @@ -1,6 +1,9 @@ +import Logic.Logic.System import Logic.Logic.HilbertStyle import Logic.FirstOrder.Incompleteness.FirstIncompleteness +open LO.System + namespace LO.FirstOrder.Theory open Subformula @@ -24,10 +27,18 @@ open System.IntuitionisticNC variable {T : Theory L} [System.IntuitionisticNC (Sentence L)] +instance : Subtheory T (T ∪ {σ}) where + sub := by + intro σ' h; + exact weakening h (by simp) + infixl:50 "⊕" => modusPonens @[simp] -lemma weakening [hs : SubTheory T₀ T] : (T₀ ⊢! σ) → (T ⊢! σ) := by simp; intro H; exact ⟨System.weakening H hs.sub⟩; +lemma weakening [hs : Subtheory T₀ T] : (T₀ ⊢! σ) → (T ⊢! σ) := by + simp; + intro H; + exact ⟨hs.sub H⟩; lemma deduction {σ π} : (T ⊢! σ ⟶ π) ↔ (T ∪ {σ} ⊢! π) := by apply Iff.intro;