refactor

FormalizedFormalLogic · Sep 14, 2024 · 622ebb7 · 622ebb7
1 parent 77c9fbb
commit 622ebb7
Show file tree

Hide file tree

Showing 2 changed files with 13 additions and 4 deletions.
diff --git a/Incompleteness/Arith/First.lean b/Incompleteness/Arith/First.lean
@@ -18,7 +18,8 @@ lemma re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P := by
 
 variable (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable]
 
-theorem incomplete : ¬System.Complete T  := by
+/-- Gödel's First Incompleteness Theorem-/
+theorem goedel_first_incompleteness : ¬System.Complete T := by
   let D : ℕ → Prop := fun n : ℕ ↦ ∃ p : SyntacticSemiformula ℒₒᵣ 1, n = ⌜p⌝ ∧ T ⊢! ∼p/[⌜p⌝]
   have D_re : RePred D := by
     have : 𝚺₁-Predicate fun p : ℕ ↦

diff --git a/Incompleteness/Arith/Second.lean b/Incompleteness/Arith/Second.lean
@@ -138,6 +138,8 @@ end
 
 section
 
+variable (T)
+
 variable [T.Delta1Definable]
 
 open LO.System LO.System.FiniteContext
@@ -179,11 +181,17 @@ lemma consistent_iff_goedel : T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚 := by
     simpa [provable₀_iff] using  contra₁'! (deduct'! this)
 
 /-- Gödel's Second Incompleteness Theorem-/
-theorem consistent_unprovable [System.Consistent T] : T ⊬ ↑𝗖𝗼𝗻 := fun h ↦
-  goedel_unprovable <| and_left! consistent_iff_goedel ⨀ h
+theorem goedel_second_incompleteness [System.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 <| contra₀'! (and_right! (consistent_iff_goedel (T := T))) ⨀ h
+  not_goedel_unprovable T <| contra₀'! (and_right! (consistent_iff_goedel T)) ⨀ h
+
+theorem inconsistent_undecidable [ℕ ⊧ₘ* T] : System.Undecidable T ↑𝗖𝗼𝗻 := by
+  haveI : Consistent T := Sound.consistent_of_satisfiable ⟨_, (inferInstance : ℕ ⊧ₘ* T)⟩
+  constructor
+  · exact goedel_second_incompleteness T
+  · exact inconsistent_unprovable T
 
 end