From 622ebb7e95cbccfabb6e722b3194335380f54a29 Mon Sep 17 00:00:00 2001
From: palalansouki <palalansouki@gmail.com>
Date: Sun, 15 Sep 2024 00:05:25 +0900
Subject: [PATCH] refactor

---
 Incompleteness/Arith/First.lean  |  3 ++-
 Incompleteness/Arith/Second.lean | 14 +++++++++++---
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/Incompleteness/Arith/First.lean b/Incompleteness/Arith/First.lean
index a13d8ca..20cf598 100644
--- 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
index bc723f1..3c9e5dc 100644
--- 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