tinyfix

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,25 +124,25 @@ 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]
   : ∃ (G : Sentence ℒₒᵣ), (IsGoedelSentence T₀ T G ∧ Hierarchy Π n G) := by
   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]
   : ∃ (H : Sentence ℒₒᵣ), (IsHenkinSentence T₀ T H ∧ Hierarchy Σ n H) := by
   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

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]

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;

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]

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;

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;