remove dep arith wip

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;
 

Logic/FirstOrder/Incompleteness/Derivability/FirstIncompleteness.lean

@@ -10,15 +10,15 @@ 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]
 
 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

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

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