From 0cba9e6e68c0e884eae0703ebb3f9102633b517e Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Wed, 13 Aug 2025 14:14:24 +0900
Subject: [PATCH 01/10] yablo system

---
 Foundation.lean                           |  2 ++
 Foundation/FirstOrder/Internal/Yablo.lean | 27 +++++++++++++++++++++++
 2 files changed, 29 insertions(+)
 create mode 100644 Foundation/FirstOrder/Internal/Yablo.lean

diff --git a/Foundation.lean b/Foundation.lean
index a24dece32..b17af6663 100644
--- a/Foundation.lean
+++ b/Foundation.lean
@@ -70,6 +70,8 @@ import Foundation.FirstOrder.Internal.Consistency
 import Foundation.FirstOrder.Internal.WitnessComparison
 import Foundation.FirstOrder.Internal.RosserProvability
 
+import Foundation.FirstOrder.Internal.Yablo
+
 import Foundation.FirstOrder.Incompleteness.First
 import Foundation.FirstOrder.Incompleteness.Halting
 
diff --git a/Foundation/FirstOrder/Internal/Yablo.lean b/Foundation/FirstOrder/Internal/Yablo.lean
new file mode 100644
index 000000000..9da133f9c
--- /dev/null
+++ b/Foundation/FirstOrder/Internal/Yablo.lean
@@ -0,0 +1,27 @@
+import Foundation.ProvabilityLogic.Incompleteness
+import Foundation.FirstOrder.Internal.FixedPoint
+import Foundation.FirstOrder.Internal.RosserProvability
+
+namespace LO.FirstOrder
+
+open FirstOrder Arithmetic PeanoMinus IOpen ISigma0 ISigma1 Metamath InternalArithmetic
+
+namespace Theory
+
+variable {V} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
+         {L : Language} [L.Encodable] [L.LORDefinable]
+         (T : Theory ℒₒᵣ) [T.Δ₁]
+
+def YabloSystem (φ n : V) : Prop := ∀ m, n < m → ¬T.Provable (substNumeral φ m)
+
+def yabloSystem : 𝚷₁.Semisentence 2 := .mkPi
+  “φ n. ∀ m, n < m → ∀ nσ, !ssnum nσ φ m → ¬!T.provable (nσ)”
+
+lemma YabloSystem_defined :
+    𝚷₁-Relation[V] (T.YabloSystem) via T.yabloSystem := by
+  intro f;
+  simp [Theory.YabloSystem, Theory.yabloSystem];
+
+end Theory
+
+end LO.FirstOrder

From 7f4a5a77e721243868c20c02a3ce5a02f2aaf512 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Wed, 20 Aug 2025 00:30:28 +0900
Subject: [PATCH 02/10] wip

---
 Foundation/FirstOrder/Internal/Yablo.lean | 48 ++++++++++++++++++++---
 1 file changed, 42 insertions(+), 6 deletions(-)

diff --git a/Foundation/FirstOrder/Internal/Yablo.lean b/Foundation/FirstOrder/Internal/Yablo.lean
index 9da133f9c..ab1799f59 100644
--- a/Foundation/FirstOrder/Internal/Yablo.lean
+++ b/Foundation/FirstOrder/Internal/Yablo.lean
@@ -9,19 +9,55 @@ open FirstOrder Arithmetic PeanoMinus IOpen ISigma0 ISigma1 Metamath InternalAri
 namespace Theory
 
 variable {V} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
-         {L : Language} [L.Encodable] [L.LORDefinable]
-         (T : Theory ℒₒᵣ) [T.Δ₁]
+         {T U : ArithmeticTheory} [T.Δ₁] [𝐈𝚺₁ ⪯ U]
 
-def YabloSystem (φ n : V) : Prop := ∀ m, n < m → ¬T.Provable (substNumeral φ m)
+def YabloSystem (T : ArithmeticTheory) [T.Δ₁] (φ n : V) : Prop := ∀ m, n < m → ¬T.Provable (substNumeral φ m)
 
-def yabloSystem : 𝚷₁.Semisentence 2 := .mkPi
+def yabloSystem (T : ArithmeticTheory) [T.Δ₁] : 𝚷₁.Semisentence 2 := .mkPi
   “φ n. ∀ m, n < m → ∀ nσ, !ssnum nσ φ m → ¬!T.provable (nσ)”
 
-lemma YabloSystem_defined :
-    𝚷₁-Relation[V] (T.YabloSystem) via T.yabloSystem := by
+lemma yabloSystem.defined : 𝚷₁-Relation[V] (T.YabloSystem) via T.yabloSystem := by
   intro f;
   simp [Theory.YabloSystem, Theory.yabloSystem];
 
+@[simp]
+lemma yabloSystem.eval (v) :
+   Semiformula.Evalbm V v T.yabloSystem.val ↔ T.YabloSystem (v 0) (v 1) := yabloSystem.defined.df.iff v
+
+instance yabloSystem.definable : 𝚷₁-Relation[V] (T.YabloSystem) := yabloSystem.defined.to_definable
+
+
+/-- Yablo's Predicate -/
+def yablo (T : ArithmeticTheory) [T.Δ₁] : ArithmeticSemisentence 1 := parameterizedFixedpoint (T.yabloSystem)
+
+lemma yablo_diagonal : U ⊢!. ∀' (T.yablo ⭤ (T.yabloSystem)/[⌜T.yablo⌝, #0]) := parameterized_diagonal₁ _
+
+lemma yablo_def {n : ℕ} : U ⊢!. T.yablo/[n] ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
+  sorry;
+
+lemma neg_yablo_def {n : ℕ} : U ⊢!. ∼T.yablo/[n] ↔ U ⊢!. “∃ m, ↑n < m ∧ ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → !T.provable (nσ)” := by
+  sorry;
+
+open LO.Entailment
+variable [U.Δ₁] [Entailment.Consistent U]
+
+theorem yablo_unprovable [Entailment.Consistent U] {n : ℕ} : U ⊬. T.yablo/[n] := by
+  by_contra! hC;
+  have := yablo_def.mp hC;
+  -- have h₁ : U ⊢!. ∼↑(T.provable)/[⌜(T.yablo)/[n + 1]⌝])))”) := by sorry;
+  -- have h₂ : U ⊢!. ↑(T.provable)/[⌜(T.yablo)/[n + 1]⌝])))”) := by sorry;
+  have : ¬Entailment.Consistent U := not_consistent_iff_inconsistent.mpr $ inconsistent_iff_provable_bot.mpr $ by
+    sorry
+  contradiction;
+
+theorem yablo_unrefutable [U.SoundOnHierarchy 𝚺 1] {n : ℕ} : U ⊬. ∼T.yablo/[n] := by
+  have con : Consistent (U : Axiom ℒₒᵣ) := inferInstance;
+  by_contra! hC;
+  have : U ⊢!. (“∃' (↑n < #0 ∧ !(∀' (↑ssnum/[#0, ⌜yablo T⌝, #1] ➝ ↑(provable T)/[#0])))”) := by
+    sorry;
+  have := U.soundOnHierarchy 𝚺 1 this (by sorry);
+  sorry;
+
 end Theory
 
 end LO.FirstOrder

From 843f184932d97fe8b32be57bd61d275e148f5785 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Wed, 20 Aug 2025 00:49:36 +0900
Subject: [PATCH 03/10] move

---
 Foundation.lean                                               | 2 +-
 Foundation/FirstOrder/{Internal => Incompleteness}/Yablo.lean | 0
 2 files changed, 1 insertion(+), 1 deletion(-)
 rename Foundation/FirstOrder/{Internal => Incompleteness}/Yablo.lean (100%)

diff --git a/Foundation.lean b/Foundation.lean
index f28fab85b..3504033b2 100644
--- a/Foundation.lean
+++ b/Foundation.lean
@@ -70,7 +70,6 @@ import Foundation.FirstOrder.Internal.Consistency
 import Foundation.FirstOrder.Internal.WitnessComparison
 import Foundation.FirstOrder.Internal.RosserProvability
 
-import Foundation.FirstOrder.Internal.Yablo
 
 import Foundation.FirstOrder.Incompleteness.First
 import Foundation.FirstOrder.Incompleteness.Halting
@@ -80,6 +79,7 @@ import Foundation.FirstOrder.Incompleteness.Second
 import Foundation.FirstOrder.Incompleteness.Examples
 
 import Foundation.FirstOrder.Incompleteness.Tarski
+import Foundation.FirstOrder.Incompleteness.Yablo
 
 import Foundation.FirstOrder.Hauptsatz
 
diff --git a/Foundation/FirstOrder/Internal/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
similarity index 100%
rename from Foundation/FirstOrder/Internal/Yablo.lean
rename to Foundation/FirstOrder/Incompleteness/Yablo.lean

From be3a7b732f4890dff6be4d9ab5ab2143cf3d5004 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Sun, 24 Aug 2025 03:41:05 +0900
Subject: [PATCH 04/10] wip

---
 .../FirstOrder/Incompleteness/Yablo.lean      | 71 ++++++++++++++++---
 1 file changed, 61 insertions(+), 10 deletions(-)

diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
index ab1799f59..18cff73a6 100644
--- a/Foundation/FirstOrder/Incompleteness/Yablo.lean
+++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean
@@ -27,28 +27,79 @@ lemma yabloSystem.eval (v) :
 instance yabloSystem.definable : 𝚷₁-Relation[V] (T.YabloSystem) := yabloSystem.defined.to_definable
 
 
+open LO.Entailment
+
 /-- Yablo's Predicate -/
 def yablo (T : ArithmeticTheory) [T.Δ₁] : ArithmeticSemisentence 1 := parameterizedFixedpoint (T.yabloSystem)
 
 lemma yablo_diagonal : U ⊢!. ∀' (T.yablo ⭤ (T.yabloSystem)/[⌜T.yablo⌝, #0]) := parameterized_diagonal₁ _
 
-lemma yablo_def {n : ℕ} : U ⊢!. T.yablo/[n] ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
-  sorry;
+section
+
+variable {V : Type} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
+
+lemma iff_yablo_modeled₀ (n : V) : V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by
+  have : V ⊧ₘ₀ ∀' (yablo T ⭤ ↑(yabloSystem T)/[⌜yablo T⌝, #0]) := models_of_provable₀ (by assumption) $ yablo_diagonal;
+  have : ∀ (n : V), V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by simpa [models₀_iff] using this;
+  apply this;
+
+lemma iff_yablo_modeled (n : ℕ) : V ⊧/![(ORingStruc.numeral n)] (T.yablo) ↔ T.YabloSystem (V := V) ⌜T.yablo⌝ (ORingStruc.numeral n) := iff_yablo_modeled₀ _
+
+lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yablo/[n] ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
+  suffices U ⊢!. T.yablo/[n] ⭤ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” by
+    constructor <;>
+    . intro h; cl_prover [h, this];
+  apply oRing_provable₀_of.{0};
+  intro V _ _;
+  have : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
+  suffices V ⊧/![ORingStruc.numeral n] (T.yablo) ↔ T.YabloSystem ⌜yablo T⌝ (ORingStruc.numeral n) by
+    simpa [models_iff, Matrix.constant_eq_singleton];
+  apply iff_yablo_modeled;
+
+end
 
 lemma neg_yablo_def {n : ℕ} : U ⊢!. ∼T.yablo/[n] ↔ U ⊢!. “∃ m, ↑n < m ∧ ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → !T.provable (nσ)” := by
   sorry;
 
 open LO.Entailment
-variable [U.Δ₁] [Entailment.Consistent U]
+variable [𝐈𝚺₁ ⪯ T] [T.Δ₁] [Entailment.Consistent T]
 
-theorem yablo_unprovable [Entailment.Consistent U] {n : ℕ} : U ⊬. T.yablo/[n] := by
+theorem yablo_unprovable [U_consis : Entailment.Consistent U] {n : ℕ} : T ⊬. T.yablo/[n] := by
   by_contra! hC;
-  have := yablo_def.mp hC;
-  -- have h₁ : U ⊢!. ∼↑(T.provable)/[⌜(T.yablo)/[n + 1]⌝])))”) := by sorry;
-  -- have h₂ : U ⊢!. ↑(T.provable)/[⌜(T.yablo)/[n + 1]⌝])))”) := by sorry;
-  have : ¬Entailment.Consistent U := not_consistent_iff_inconsistent.mpr $ inconsistent_iff_provable_bot.mpr $ by
-    sorry
-  contradiction;
+  have hC := iff_yablo_provable n |>.mp hC;
+  have H₁ : T ⊢!. T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
+    apply Entailment.WeakerThan.pbl $ provable_D1 (T := T) ?_
+    apply iff_yablo_provable _ |>.mpr;
+    apply oRing_provable₀_of.{0};
+    intro V _ _;
+    have : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance;
+    suffices
+      ∀ (m : V), ORingStruc.numeral (n + 1) < m → ¬Provable T (substNumeral ⌜yablo T⌝ m) by
+      simpa [models_iff];
+    intro m hm;
+    have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)”
+      := models_of_provable₀ (T := T) (by assumption) $ hC;
+    replace :
+      ∀ (m : V), ORingStruc.numeral n < m → ¬Provable T (substNumeral ⌜yablo T⌝ m)
+      := by simpa [models_iff] using this;
+    apply this;
+    -- TODO: ORingStruc.numeral (n + 1) < m → ORingStruc.numeral n < m
+    sorry;
+  have H₂ : T ⊢!. ∼T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
+    apply oRing_provable₀_of.{0};
+    intro V _ _;
+    have : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance;
+    suffices ¬T.Provable ⌜(yablo T)/[↑(n + 1)]⌝ by simpa [provabilityPred, models_iff];
+    have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)”
+      := models_of_provable₀ (T := T) (by assumption) $ hC;
+    replace :
+      ∀ (m : V), ORingStruc.numeral n < m →
+      ¬T.Provable (substNumeral ⌜T.yablo⌝ m) := by simpa [models_iff] using this;
+    have := this (ORingStruc.numeral (n + 1)) (by simp);
+    sorry;
+  apply Entailment.Consistent.not_bot (𝓢 := T.toAxiom);
+  . infer_instance;
+  . cl_prover [H₁, H₂];
 
 theorem yablo_unrefutable [U.SoundOnHierarchy 𝚺 1] {n : ℕ} : U ⊬. ∼T.yablo/[n] := by
   have con : Consistent (U : Axiom ℒₒᵣ) := inferInstance;

From 046aa3bb16b5cc3ee2cdb7ddc40e0f63f43f1cef Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Sun, 24 Aug 2025 18:48:30 +0900
Subject: [PATCH 05/10] `yablo_unprovable`, H1

---
 .../FirstOrder/Incompleteness/Yablo.lean      | 35 ++++++++++++-------
 1 file changed, 23 insertions(+), 12 deletions(-)

diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
index 18cff73a6..8b7c05ba1 100644
--- a/Foundation/FirstOrder/Incompleteness/Yablo.lean
+++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean
@@ -2,6 +2,20 @@ import Foundation.ProvabilityLogic.Incompleteness
 import Foundation.FirstOrder.Internal.FixedPoint
 import Foundation.FirstOrder.Internal.RosserProvability
 
+
+namespace LO.PeanoMinus
+
+open ORingStruc
+
+variable {M : Type*} [ORingStruc M] [M ⊧ₘ* 𝐏𝐀⁻]
+
+lemma numeral_lt_of_numeral_succ_lt {n : ℕ} {m : M} : (numeral (n + 1) : M) < m → (numeral n < m) := by
+  apply PeanoMinus.lt_trans;
+  simp;
+
+end LO.PeanoMinus
+
+
 namespace LO.FirstOrder
 
 open FirstOrder Arithmetic PeanoMinus IOpen ISigma0 ISigma1 Metamath InternalArithmetic
@@ -62,13 +76,13 @@ lemma neg_yablo_def {n : ℕ} : U ⊢!. ∼T.yablo/[n] ↔ U ⊢!. “∃ m, ↑
   sorry;
 
 open LO.Entailment
-variable [𝐈𝚺₁ ⪯ T] [T.Δ₁] [Entailment.Consistent T]
+variable [𝐈𝚺₁ ⪯ T] [T.Δ₁]
 
-theorem yablo_unprovable [U_consis : Entailment.Consistent U] {n : ℕ} : T ⊬. T.yablo/[n] := by
+theorem yablo_unprovable [Entailment.Consistent T] {n : ℕ} : T ⊬. T.yablo/[.numeral n] := by
   by_contra! hC;
-  have hC := iff_yablo_provable n |>.mp hC;
+  replace hC := iff_yablo_provable n |>.mp hC;
   have H₁ : T ⊢!. T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
-    apply Entailment.WeakerThan.pbl $ provable_D1 (T := T) ?_
+    apply Entailment.WeakerThan.pbl $ provable_D1 (T := T) ?_;
     apply iff_yablo_provable _ |>.mpr;
     apply oRing_provable₀_of.{0};
     intro V _ _;
@@ -77,14 +91,11 @@ theorem yablo_unprovable [U_consis : Entailment.Consistent U] {n : ℕ} : T ⊬.
       ∀ (m : V), ORingStruc.numeral (n + 1) < m → ¬Provable T (substNumeral ⌜yablo T⌝ m) by
       simpa [models_iff];
     intro m hm;
-    have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)”
-      := models_of_provable₀ (T := T) (by assumption) $ hC;
-    replace :
-      ∀ (m : V), ORingStruc.numeral n < m → ¬Provable T (substNumeral ⌜yablo T⌝ m)
-      := by simpa [models_iff] using this;
-    apply this;
-    -- TODO: ORingStruc.numeral (n + 1) < m → ORingStruc.numeral n < m
-    sorry;
+    have : ∀ (m : V), ORingStruc.numeral n < m → ¬Provable T (substNumeral ⌜yablo T⌝ m) := by
+      have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
+        models_of_provable₀ (T := T) (by assumption) $ hC;
+      simpa [models_iff] using this;
+    exact this _ $ PeanoMinus.numeral_lt_of_numeral_succ_lt hm;
   have H₂ : T ⊢!. ∼T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
     apply oRing_provable₀_of.{0};
     intro V _ _;

From bf5471152e1874e68ffcb7b41b76294db05b2c36 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Sun, 24 Aug 2025 20:01:05 +0900
Subject: [PATCH 06/10] `yablo_unprovable`

---
 .../FirstOrder/Incompleteness/Yablo.lean      | 47 ++++++++++++-------
 1 file changed, 31 insertions(+), 16 deletions(-)

diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
index 8b7c05ba1..fc3e9dbc7 100644
--- a/Foundation/FirstOrder/Incompleteness/Yablo.lean
+++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean
@@ -16,6 +16,25 @@ lemma numeral_lt_of_numeral_succ_lt {n : ℕ} {m : M} : (numeral (n + 1) : M) <
 end LO.PeanoMinus
 
 
+namespace LO.ISigma1.Metamath.InternalArithmetic
+
+open FirstOrder Arithmetic PeanoMinus IOpen ISigma0
+
+variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
+
+lemma substNumeral_app_quote_nat (σ : Semisentence ℒₒᵣ 1) (n : ℕ) :
+  substNumeral ⌜σ⌝ (n : V) = ⌜(σ/[.numeral n] : Sentence ℒₒᵣ)⌝ := by
+  simp [
+    substNumeral, Semiformula.empty_quote_def, Semiformula.quote_def,
+    Rewriting.embedding_substs_eq_substs_coe₁
+  ];
+
+end LO.ISigma1.Metamath.InternalArithmetic
+
+
+
+
+
 namespace LO.FirstOrder
 
 open FirstOrder Arithmetic PeanoMinus IOpen ISigma0 ISigma1 Metamath InternalArithmetic
@@ -72,11 +91,8 @@ lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yablo/[n] ↔ U ⊢!. “∀ m, 
 
 end
 
-lemma neg_yablo_def {n : ℕ} : U ⊢!. ∼T.yablo/[n] ↔ U ⊢!. “∃ m, ↑n < m ∧ ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → !T.provable (nσ)” := by
-  sorry;
-
 open LO.Entailment
-variable [𝐈𝚺₁ ⪯ T] [T.Δ₁]
+variable [𝐈𝚺₁ ⪯ T]
 
 theorem yablo_unprovable [Entailment.Consistent T] {n : ℕ} : T ⊬. T.yablo/[.numeral n] := by
   by_contra! hC;
@@ -100,24 +116,23 @@ theorem yablo_unprovable [Entailment.Consistent T] {n : ℕ} : T ⊬. T.yablo/[.
     apply oRing_provable₀_of.{0};
     intro V _ _;
     have : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance;
-    suffices ¬T.Provable ⌜(yablo T)/[↑(n + 1)]⌝ by simpa [provabilityPred, models_iff];
-    have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)”
-      := models_of_provable₀ (T := T) (by assumption) $ hC;
-    replace :
-      ∀ (m : V), ORingStruc.numeral n < m →
-      ¬T.Provable (substNumeral ⌜T.yablo⌝ m) := by simpa [models_iff] using this;
-    have := this (ORingStruc.numeral (n + 1)) (by simp);
-    sorry;
+    suffices ¬T.Provable (substNumeral ⌜yablo T⌝ (n + 1 : V)) by
+      simpa [provabilityPred, models_iff, ←substNumeral_app_quote_nat];
+    replace : ∀ (m : V), ORingStruc.numeral n < m → ¬T.Provable (substNumeral ⌜T.yablo⌝ m) := by
+      have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
+        models_of_provable₀ (T := T) (by assumption) $ hC;
+      simpa [models_iff] using this;
+    apply this (n + 1) (by simp [numeral_eq_natCast]);
   apply Entailment.Consistent.not_bot (𝓢 := T.toAxiom);
   . infer_instance;
   . cl_prover [H₁, H₂];
 
-theorem yablo_unrefutable [U.SoundOnHierarchy 𝚺 1] {n : ℕ} : U ⊬. ∼T.yablo/[n] := by
-  have con : Consistent (U : Axiom ℒₒᵣ) := inferInstance;
+theorem yablo_unrefutable [T.SoundOnHierarchy 𝚺 1] {n : ℕ} : T ⊬. ∼T.yablo/[n] := by
+  have T_consis : Consistent (T : Axiom ℒₒᵣ) := inferInstance;
   by_contra! hC;
-  have : U ⊢!. (“∃' (↑n < #0 ∧ !(∀' (↑ssnum/[#0, ⌜yablo T⌝, #1] ➝ ↑(provable T)/[#0])))”) := by
+  have : T ⊢!. (“∃' (↑n < #0 ∧ !(∀' (↑ssnum/[#0, ⌜yablo T⌝, #1] ➝ ↑(provable T)/[#0])))”) := by
     sorry;
-  have := U.soundOnHierarchy 𝚺 1 this (by sorry);
+  have := T.soundOnHierarchy 𝚺 1 this (by sorry);
   sorry;
 
 end Theory

From 1a9cf56279f4cb0b61e846068cf4cf81c33b3c6c Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Wed, 27 Aug 2025 06:45:46 +0900
Subject: [PATCH 07/10] degenerate

---
 .../FirstOrder/Incompleteness/Yablo.lean      | 78 +++++++++++--------
 1 file changed, 45 insertions(+), 33 deletions(-)

diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
index fc3e9dbc7..c9897718e 100644
--- a/Foundation/FirstOrder/Incompleteness/Yablo.lean
+++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean
@@ -42,7 +42,7 @@ open FirstOrder Arithmetic PeanoMinus IOpen ISigma0 ISigma1 Metamath InternalAri
 namespace Theory
 
 variable {V} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
-         {T U : ArithmeticTheory} [T.Δ₁] [𝐈𝚺₁ ⪯ U]
+         {T U : ArithmeticTheory} [T.Δ₁]
 
 def YabloSystem (T : ArithmeticTheory) [T.Δ₁] (φ n : V) : Prop := ∀ m, n < m → ¬T.Provable (substNumeral φ m)
 
@@ -60,73 +60,83 @@ lemma yabloSystem.eval (v) :
 instance yabloSystem.definable : 𝚷₁-Relation[V] (T.YabloSystem) := yabloSystem.defined.to_definable
 
 
+open Classical
 open LO.Entailment
 
-/-- Yablo's Predicate -/
+/-- Yablo Predicate -/
 def yablo (T : ArithmeticTheory) [T.Δ₁] : ArithmeticSemisentence 1 := parameterizedFixedpoint (T.yabloSystem)
 
-lemma yablo_diagonal : U ⊢!. ∀' (T.yablo ⭤ (T.yabloSystem)/[⌜T.yablo⌝, #0]) := parameterized_diagonal₁ _
+abbrev yabloPred (T : ArithmeticTheory) [T.Δ₁] (n : ℕ) : ArithmeticSentence := T.yablo/[n]
 
 section
 
 variable {V : Type} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
+variable [𝐈𝚺₁ ⪯ U]
+
+lemma yablo_diagonal : U ⊢!. ∀' (T.yablo ⭤ (T.yabloSystem)/[⌜T.yablo⌝, #0]) := parameterized_diagonal₁ _
 
-lemma iff_yablo_modeled₀ (n : V) : V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by
-  have : V ⊧ₘ₀ ∀' (yablo T ⭤ ↑(yabloSystem T)/[⌜yablo T⌝, #0]) := models_of_provable₀ (by assumption) $ yablo_diagonal;
+lemma yablo_diagonal_modeled (n : V) : V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by sorry;
+  /-
+  have : V ⊧ₘ₀ ∀' (T.yablo ⭤ ↑(T.yabloSystem)/[⌜T.yablo⌝, #0]) := models_of_provable₀ (T := 𝐈𝚺₁) (by assumption) $ yablo_diagonal;
   have : ∀ (n : V), V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by simpa [models₀_iff] using this;
   apply this;
+  -/
 
-lemma iff_yablo_modeled (n : ℕ) : V ⊧/![(ORingStruc.numeral n)] (T.yablo) ↔ T.YabloSystem (V := V) ⌜T.yablo⌝ (ORingStruc.numeral n) := iff_yablo_modeled₀ _
 
 lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yablo/[n] ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
   suffices U ⊢!. T.yablo/[n] ⭤ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” by
-    constructor <;>
-    . intro h; cl_prover [h, this];
+    constructor <;> . intro h; cl_prover [h, this];
+  apply oRing_provable₀_of.{0};
+  intro V _ _;
+  haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
+  haveI : V ⊧/![ORingStruc.numeral n] (yablo T) ↔ T.YabloSystem ⌜T.yablo⌝ (ORingStruc.numeral n) := yablo_diagonal_modeled _;
+  -- simpa [models_iff, Matrix.constant_eq_singleton] using this; TODO: compilation problem
+  sorry;
+
+lemma provable_yablo_lt (n m : ℕ) (hnm : n < m) : U ⊢!. (T.yabloPred n) ➝ (T.yabloPred m) := by
   apply oRing_provable₀_of.{0};
   intro V _ _;
-  have : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
-  suffices V ⊧/![ORingStruc.numeral n] (T.yablo) ↔ T.YabloSystem ⌜yablo T⌝ (ORingStruc.numeral n) by
-    simpa [models_iff, Matrix.constant_eq_singleton];
-  apply iff_yablo_modeled;
+  haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
+  suffices V ⊧/![(ORingStruc.numeral n)] (T.yablo) → V ⊧/![(ORingStruc.numeral m)] (T.yablo) by
+    simp only [
+      models₀_iff, LogicalConnective.HomClass.map_imply, Semiformula.eval_substs,
+      Matrix.cons_val_fin_one, Semiterm.val_operator₀, Structure.numeral_eq_numeral,
+      LogicalConnective.Prop.arrow_eq
+    ];
+    convert this <;> simp;
+  simp only [yablo_diagonal_modeled];
+  intro h k hmk;
+  apply h;
+  apply PeanoMinus.lt_trans _ _ _ (by simpa) hmk;
 
 end
 
 open LO.Entailment
-variable [𝐈𝚺₁ ⪯ T]
 
-theorem yablo_unprovable [Entailment.Consistent T] {n : ℕ} : T ⊬. T.yablo/[.numeral n] := by
+theorem yablo_unprovable [𝐈𝚺₁ ⪯ T] [Entailment.Consistent T] {n : ℕ} : T ⊬. (T.yabloPred n) := by
   by_contra! hC;
-  replace hC := iff_yablo_provable n |>.mp hC;
   have H₁ : T ⊢!. T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
     apply Entailment.WeakerThan.pbl $ provable_D1 (T := T) ?_;
-    apply iff_yablo_provable _ |>.mpr;
-    apply oRing_provable₀_of.{0};
-    intro V _ _;
-    have : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance;
-    suffices
-      ∀ (m : V), ORingStruc.numeral (n + 1) < m → ¬Provable T (substNumeral ⌜yablo T⌝ m) by
-      simpa [models_iff];
-    intro m hm;
-    have : ∀ (m : V), ORingStruc.numeral n < m → ¬Provable T (substNumeral ⌜yablo T⌝ m) := by
-      have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
-        models_of_provable₀ (T := T) (by assumption) $ hC;
-      simpa [models_iff] using this;
-    exact this _ $ PeanoMinus.numeral_lt_of_numeral_succ_lt hm;
+    apply provable_yablo_lt n (n + 1) (by omega) ⨀ hC;
   have H₂ : T ⊢!. ∼T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
     apply oRing_provable₀_of.{0};
     intro V _ _;
-    have : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance;
+    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance;
     suffices ¬T.Provable (substNumeral ⌜yablo T⌝ (n + 1 : V)) by
       simpa [provabilityPred, models_iff, ←substNumeral_app_quote_nat];
-    replace : ∀ (m : V), ORingStruc.numeral n < m → ¬T.Provable (substNumeral ⌜T.yablo⌝ m) := by
-      have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
-        models_of_provable₀ (T := T) (by assumption) $ hC;
-      simpa [models_iff] using this;
+    have : ∀ (x : V), ORingStruc.numeral n < x → ¬Provable T (substNumeral ⌜yablo T⌝ x) := by
+      sorry;
+      /-
+      haveI : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
+        models_of_provable₀ (T := T) (by assumption) $ (iff_yablo_provable n |>.mp hC);
+      simpa [models_iff] using this; -- TODO: comilation problem
+      -/
     apply this (n + 1) (by simp [numeral_eq_natCast]);
   apply Entailment.Consistent.not_bot (𝓢 := T.toAxiom);
   . infer_instance;
   . cl_prover [H₁, H₂];
 
+/-
 theorem yablo_unrefutable [T.SoundOnHierarchy 𝚺 1] {n : ℕ} : T ⊬. ∼T.yablo/[n] := by
   have T_consis : Consistent (T : Axiom ℒₒᵣ) := inferInstance;
   by_contra! hC;
@@ -134,7 +144,9 @@ theorem yablo_unrefutable [T.SoundOnHierarchy 𝚺 1] {n : ℕ} : T ⊬. ∼T.ya
     sorry;
   have := T.soundOnHierarchy 𝚺 1 this (by sorry);
   sorry;
+-/
 
 end Theory
 
+
 end LO.FirstOrder

From a682df00164f7f73ad6888102423d7675a2b43c6 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Wed, 27 Aug 2025 17:58:20 +0900
Subject: [PATCH 08/10] yablo_unrefutable

---
 .../FirstOrder/Incompleteness/Yablo.lean      | 97 +++++++++++++------
 1 file changed, 67 insertions(+), 30 deletions(-)

diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
index c9897718e..a90ceaaa4 100644
--- a/Foundation/FirstOrder/Incompleteness/Yablo.lean
+++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean
@@ -1,7 +1,11 @@
-import Foundation.ProvabilityLogic.Incompleteness
-import Foundation.FirstOrder.Internal.FixedPoint
-import Foundation.FirstOrder.Internal.RosserProvability
+/-
+  Formalizing Yablo's Paradox.
+
+  *References*
+  - C. Cieśliński, R. Urbaniak, "Gödelizing the Yablo Sequence"
+-/
 
+import Foundation.FirstOrder.Internal.DerivabilityCondition
 
 namespace LO.PeanoMinus
 
@@ -22,13 +26,20 @@ open FirstOrder Arithmetic PeanoMinus IOpen ISigma0
 
 variable {V : Type*} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
 
-lemma substNumeral_app_quote_nat (σ : Semisentence ℒₒᵣ 1) (n : ℕ) :
+lemma substNumeral_app_quote_nat_model (σ : Semisentence ℒₒᵣ 1) (n : ℕ) :
   substNumeral ⌜σ⌝ (n : V) = ⌜(σ/[.numeral n] : Sentence ℒₒᵣ)⌝ := by
   simp [
     substNumeral, Semiformula.empty_quote_def, Semiformula.quote_def,
     Rewriting.embedding_substs_eq_substs_coe₁
   ];
 
+lemma substNumeral_app_quote_nat_Nat (σ : Semisentence ℒₒᵣ 1) (n : ℕ) :
+  substNumeral ⌜σ⌝ n = ⌜(σ/[.numeral n] : Sentence ℒₒᵣ)⌝ := by
+  simp [
+    substNumeral, Semiformula.empty_quote_def, Semiformula.quote_def,
+    Rewriting.embedding_substs_eq_substs_coe₁
+  ];
+
 end LO.ISigma1.Metamath.InternalArithmetic
 
 
@@ -59,19 +70,25 @@ lemma yabloSystem.eval (v) :
 
 instance yabloSystem.definable : 𝚷₁-Relation[V] (T.YabloSystem) := yabloSystem.defined.to_definable
 
+def yablo (T : ArithmeticTheory) [T.Δ₁] : ArithmeticSemisentence 1 := parameterizedFixedpoint (T.yabloSystem)
+
+abbrev yabloPred (T : ArithmeticTheory) [T.Δ₁] (n : ℕ) : ArithmeticSentence := T.yablo/[.numeral n]
 
-open Classical
-open LO.Entailment
+end Theory
 
-/-- Yablo Predicate -/
-def yablo (T : ArithmeticTheory) [T.Δ₁] : ArithmeticSemisentence 1 := parameterizedFixedpoint (T.yabloSystem)
 
-abbrev yabloPred (T : ArithmeticTheory) [T.Δ₁] (n : ℕ) : ArithmeticSentence := T.yablo/[n]
 
+namespace Arithmetic
+
+variable {T : ArithmeticTheory} [T.Δ₁]
+
+open Theory
+
+-- Lemmata
 section
 
 variable {V : Type} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁]
-variable [𝐈𝚺₁ ⪯ U]
+variable {U : ArithmeticTheory} [𝐈𝚺₁ ⪯ U]
 
 lemma yablo_diagonal : U ⊢!. ∀' (T.yablo ⭤ (T.yabloSystem)/[⌜T.yablo⌝, #0]) := parameterized_diagonal₁ _
 
@@ -82,8 +99,7 @@ lemma yablo_diagonal_modeled (n : V) : V ⊧/![n] (T.yablo) ↔ T.YabloSystem 
   apply this;
   -/
 
-
-lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yablo/[n] ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
+lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yabloPred n ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
   suffices U ⊢!. T.yablo/[n] ⭤ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” by
     constructor <;> . intro h; cl_prover [h, this];
   apply oRing_provable₀_of.{0};
@@ -93,7 +109,22 @@ lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yablo/[n] ↔ U ⊢!. “∀ m, 
   -- simpa [models_iff, Matrix.constant_eq_singleton] using this; TODO: compilation problem
   sorry;
 
-lemma provable_yablo_lt (n m : ℕ) (hnm : n < m) : U ⊢!. (T.yabloPred n) ➝ (T.yabloPred m) := by
+lemma iff_neg_yablo_provable (n : ℕ) : U ⊢!. ∼(T.yabloPred n) ↔ U ⊢!. “∃ m, ↑n < m ∧ ∃ nσ, !ssnum nσ ⌜T.yablo⌝ m ∧ !T.provable (nσ)” := by
+  suffices U ⊢!. ∼T.yablo/[n] ⭤ “∃ m, ↑n < m ∧ ∃ nσ, !ssnum nσ ⌜T.yablo⌝ m ∧ !T.provable (nσ)” by
+    constructor <;> . intro h; cl_prover [h, this];
+  apply oRing_provable₀_of.{0};
+  intro V _ _;
+  haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
+  haveI : ¬V ⊧/![ORingStruc.numeral n] (yablo T) ↔ ¬T.YabloSystem ⌜T.yablo⌝ (ORingStruc.numeral n) := yablo_diagonal_modeled _ |>.not;
+  sorry;
+  /-
+  simp [YabloSystem] at this;
+  simp [models₀_iff];
+  convert this;
+  simp;
+  -/
+
+lemma provable_greater_yablo {n m : ℕ} (hnm : n < m) : U ⊢!. T.yabloPred n ➝ T.yabloPred m := by
   apply oRing_provable₀_of.{0};
   intro V _ _;
   haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
@@ -111,20 +142,24 @@ lemma provable_yablo_lt (n m : ℕ) (hnm : n < m) : U ⊢!. (T.yabloPred n) ➝
 
 end
 
-open LO.Entailment
 
-theorem yablo_unprovable [𝐈𝚺₁ ⪯ T] [Entailment.Consistent T] {n : ℕ} : T ⊬. (T.yabloPred n) := by
+-- Main Results
+section
+
+variable [𝐈𝚺₁ ⪯ T] {n : ℕ}
+
+theorem yablo_unprovable [Entailment.Consistent T] : T ⊬. (T.yabloPred n) := by
   by_contra! hC;
-  have H₁ : T ⊢!. T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
+  have H₁ : T ⊢!. T.provabilityPred (T.yabloPred (n + 1)) := by
     apply Entailment.WeakerThan.pbl $ provable_D1 (T := T) ?_;
-    apply provable_yablo_lt n (n + 1) (by omega) ⨀ hC;
-  have H₂ : T ⊢!. ∼T.provabilityPred (T.yablo/[.numeral (n + 1)]) := by
+    apply provable_greater_yablo (show n < n + 1 by omega) ⨀ hC;
+  have H₂ : T ⊢!. ∼T.provabilityPred (T.yabloPred (n + 1)) := by
     apply oRing_provable₀_of.{0};
     intro V _ _;
     haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance;
-    suffices ¬T.Provable (substNumeral ⌜yablo T⌝ (n + 1 : V)) by
-      simpa [provabilityPred, models_iff, ←substNumeral_app_quote_nat];
-    have : ∀ (x : V), ORingStruc.numeral n < x → ¬Provable T (substNumeral ⌜yablo T⌝ x) := by
+    suffices ¬T.Provable (substNumeral ⌜T.yablo⌝ (n + 1 : V)) by
+      simpa [provabilityPred, models_iff, ←substNumeral_app_quote_nat_model];
+    have : ∀ (x : V), ORingStruc.numeral n < x → ¬T.Provable (substNumeral ⌜T.yablo⌝ x) := by
       sorry;
       /-
       haveI : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
@@ -136,17 +171,19 @@ theorem yablo_unprovable [𝐈𝚺₁ ⪯ T] [Entailment.Consistent T] {n : ℕ}
   . infer_instance;
   . cl_prover [H₁, H₂];
 
-/-
-theorem yablo_unrefutable [T.SoundOnHierarchy 𝚺 1] {n : ℕ} : T ⊬. ∼T.yablo/[n] := by
-  have T_consis : Consistent (T : Axiom ℒₒᵣ) := inferInstance;
+theorem yablo_unrefutable [T.SoundOnHierarchy 𝚺 1] : T ⊬. ∼T.yabloPred n := by
   by_contra! hC;
-  have : T ⊢!. (“∃' (↑n < #0 ∧ !(∀' (↑ssnum/[#0, ⌜yablo T⌝, #1] ➝ ↑(provable T)/[#0])))”) := by
-    sorry;
-  have := T.soundOnHierarchy 𝚺 1 this (by sorry);
-  sorry;
--/
+  have := T.soundOnHierarchy 𝚺 1 (iff_neg_yablo_provable n |>.mp hC) $ by simp;
+  obtain ⟨k, hk₁, hk₂⟩ : ∃ x, n < x ∧ Provable T (substNumeral ⌜T.yablo⌝ x) := by sorry
+    -- simpa [models₀_iff] using this;
+  rw [substNumeral_app_quote_nat_Nat, provable_iff_provable₀ (T := T)] at hk₂;
+  exact yablo_unprovable hk₂;
 
-end Theory
+theorem yablo_independent [T.SoundOnHierarchy 𝚺 1] : Entailment.Independent (T : ArithmeticAxiom) (T.yabloPred n) := ⟨yablo_unprovable, yablo_unrefutable⟩
+
+end
+
+end Arithmetic
 
 
 end LO.FirstOrder

From 8a4655dbe38c1cb86387ce7f3336f165054ab42f Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Thu, 28 Aug 2025 03:51:40 +0900
Subject: [PATCH 09/10] done temporary

---
 .../FirstOrder/Incompleteness/Yablo.lean      | 40 +++++++------------
 1 file changed, 15 insertions(+), 25 deletions(-)

diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
index a90ceaaa4..8b7022a4c 100644
--- a/Foundation/FirstOrder/Incompleteness/Yablo.lean
+++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean
@@ -65,8 +65,7 @@ lemma yabloSystem.defined : 𝚷₁-Relation[V] (T.YabloSystem) via T.yabloSyste
   simp [Theory.YabloSystem, Theory.yabloSystem];
 
 @[simp]
-lemma yabloSystem.eval (v) :
-   Semiformula.Evalbm V v T.yabloSystem.val ↔ T.YabloSystem (v 0) (v 1) := yabloSystem.defined.df.iff v
+lemma yabloSystem.eval (v) : Semiformula.Evalbm V v T.yabloSystem.val ↔ T.YabloSystem (v 0) (v 1) := yabloSystem.defined.df.iff v
 
 instance yabloSystem.definable : 𝚷₁-Relation[V] (T.YabloSystem) := yabloSystem.defined.to_definable
 
@@ -92,12 +91,10 @@ variable {U : ArithmeticTheory} [𝐈𝚺₁ ⪯ U]
 
 lemma yablo_diagonal : U ⊢!. ∀' (T.yablo ⭤ (T.yabloSystem)/[⌜T.yablo⌝, #0]) := parameterized_diagonal₁ _
 
-lemma yablo_diagonal_modeled (n : V) : V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by sorry;
-  /-
+lemma yablo_diagonal_modeled (n : V) : V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by
   have : V ⊧ₘ₀ ∀' (T.yablo ⭤ ↑(T.yabloSystem)/[⌜T.yablo⌝, #0]) := models_of_provable₀ (T := 𝐈𝚺₁) (by assumption) $ yablo_diagonal;
-  have : ∀ (n : V), V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by simpa [models₀_iff] using this;
+  have : ∀ (n : V), V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by simpa [models₀_iff, Matrix.comp_vecCons'] using this;
   apply this;
-  -/
 
 lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yabloPred n ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
   suffices U ⊢!. T.yablo/[n] ⭤ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” by
@@ -105,9 +102,8 @@ lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yabloPred n ↔ U ⊢!. “∀ m,
   apply oRing_provable₀_of.{0};
   intro V _ _;
   haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
-  haveI : V ⊧/![ORingStruc.numeral n] (yablo T) ↔ T.YabloSystem ⌜T.yablo⌝ (ORingStruc.numeral n) := yablo_diagonal_modeled _;
-  -- simpa [models_iff, Matrix.constant_eq_singleton] using this; TODO: compilation problem
-  sorry;
+  haveI : V ⊧/![ORingStruc.numeral n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ (ORingStruc.numeral n) := yablo_diagonal_modeled _;
+  simpa [models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons'] using this;
 
 lemma iff_neg_yablo_provable (n : ℕ) : U ⊢!. ∼(T.yabloPred n) ↔ U ⊢!. “∃ m, ↑n < m ∧ ∃ nσ, !ssnum nσ ⌜T.yablo⌝ m ∧ !T.provable (nσ)” := by
   suffices U ⊢!. ∼T.yablo/[n] ⭤ “∃ m, ↑n < m ∧ ∃ nσ, !ssnum nσ ⌜T.yablo⌝ m ∧ !T.provable (nσ)” by
@@ -115,14 +111,12 @@ lemma iff_neg_yablo_provable (n : ℕ) : U ⊢!. ∼(T.yabloPred n) ↔ U ⊢!.
   apply oRing_provable₀_of.{0};
   intro V _ _;
   haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
-  haveI : ¬V ⊧/![ORingStruc.numeral n] (yablo T) ↔ ¬T.YabloSystem ⌜T.yablo⌝ (ORingStruc.numeral n) := yablo_diagonal_modeled _ |>.not;
-  sorry;
-  /-
-  simp [YabloSystem] at this;
-  simp [models₀_iff];
+  suffices ¬(Semiformula.Eval (standardModel V) (fun i ↦ ORingStruc.numeral n) Empty.elim) (T.yablo) ↔ ∃ m, ORingStruc.numeral n < m ∧ T.Provable (substNumeral ⌜T.yablo⌝ m) by
+    simpa [models₀_iff, Matrix.comp_vecCons'];
+  haveI : ¬V ⊧/![ORingStruc.numeral n] (T.yablo) ↔ ∃ m, ORingStruc.numeral n < m ∧ Provable T (substNumeral ⌜T.yablo⌝ m) := by
+    simpa [YabloSystem, Matrix.cons_val_fin_one] using yablo_diagonal_modeled _ |>.not;
   convert this;
   simp;
-  -/
 
 lemma provable_greater_yablo {n m : ℕ} (hnm : n < m) : U ⊢!. T.yabloPred n ➝ T.yabloPred m := by
   apply oRing_provable₀_of.{0};
@@ -160,12 +154,9 @@ theorem yablo_unprovable [Entailment.Consistent T] : T ⊬. (T.yabloPred n) := b
     suffices ¬T.Provable (substNumeral ⌜T.yablo⌝ (n + 1 : V)) by
       simpa [provabilityPred, models_iff, ←substNumeral_app_quote_nat_model];
     have : ∀ (x : V), ORingStruc.numeral n < x → ¬T.Provable (substNumeral ⌜T.yablo⌝ x) := by
-      sorry;
-      /-
-      haveI : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
+      have : V ⊧ₘ₀ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” :=
         models_of_provable₀ (T := T) (by assumption) $ (iff_yablo_provable n |>.mp hC);
-      simpa [models_iff] using this; -- TODO: comilation problem
-      -/
+      simpa [models_iff, Matrix.comp_vecCons'] using this;
     apply this (n + 1) (by simp [numeral_eq_natCast]);
   apply Entailment.Consistent.not_bot (𝓢 := T.toAxiom);
   . infer_instance;
@@ -173,11 +164,10 @@ theorem yablo_unprovable [Entailment.Consistent T] : T ⊬. (T.yabloPred n) := b
 
 theorem yablo_unrefutable [T.SoundOnHierarchy 𝚺 1] : T ⊬. ∼T.yabloPred n := by
   by_contra! hC;
-  have := T.soundOnHierarchy 𝚺 1 (iff_neg_yablo_provable n |>.mp hC) $ by simp;
-  obtain ⟨k, hk₁, hk₂⟩ : ∃ x, n < x ∧ Provable T (substNumeral ⌜T.yablo⌝ x) := by sorry
-    -- simpa [models₀_iff] using this;
-  rw [substNumeral_app_quote_nat_Nat, provable_iff_provable₀ (T := T)] at hk₂;
-  exact yablo_unprovable hk₂;
+  haveI := T.soundOnHierarchy 𝚺 1 (iff_neg_yablo_provable n |>.mp hC) $ by simp;
+  obtain ⟨k, _, hk⟩ : ∃ k, n < k ∧ Provable T (substNumeral ⌜T.yablo⌝ k) := by simpa [models₀_iff, Matrix.comp_vecCons'] using this;
+  rw [substNumeral_app_quote_nat_Nat, provable_iff_provable₀ (T := T)] at hk;
+  exact yablo_unprovable hk;
 
 theorem yablo_independent [T.SoundOnHierarchy 𝚺 1] : Entailment.Independent (T : ArithmeticAxiom) (T.yabloPred n) := ⟨yablo_unprovable, yablo_unrefutable⟩
 

From e1d66a98ad79ba2b8afc50e237b9868174dde0c4 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Thu, 28 Aug 2025 04:06:47 +0900
Subject: [PATCH 10/10] refactor

---
 .../FirstOrder/Incompleteness/Yablo.lean      | 25 ++++++++-----------
 1 file changed, 10 insertions(+), 15 deletions(-)

diff --git a/Foundation/FirstOrder/Incompleteness/Yablo.lean b/Foundation/FirstOrder/Incompleteness/Yablo.lean
index 8b7022a4c..b88cd7765 100644
--- a/Foundation/FirstOrder/Incompleteness/Yablo.lean
+++ b/Foundation/FirstOrder/Incompleteness/Yablo.lean
@@ -91,11 +91,14 @@ variable {U : ArithmeticTheory} [𝐈𝚺₁ ⪯ U]
 
 lemma yablo_diagonal : U ⊢!. ∀' (T.yablo ⭤ (T.yabloSystem)/[⌜T.yablo⌝, #0]) := parameterized_diagonal₁ _
 
-lemma yablo_diagonal_modeled (n : V) : V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by
+lemma yablo_diagonal_modeled (n : V) : V ⊧/![n] (T.yablo) ↔ ∀ m, n < m → ¬T.Provable (substNumeral ⌜T.yablo⌝ m) := by
   have : V ⊧ₘ₀ ∀' (T.yablo ⭤ ↑(T.yabloSystem)/[⌜T.yablo⌝, #0]) := models_of_provable₀ (T := 𝐈𝚺₁) (by assumption) $ yablo_diagonal;
   have : ∀ (n : V), V ⊧/![n] (T.yablo) ↔ T.YabloSystem ⌜T.yablo⌝ n := by simpa [models₀_iff, Matrix.comp_vecCons'] using this;
   apply this;
 
+lemma yablo_diagonal_neg_modeled (n : V) : ¬V ⊧/![n] (T.yablo) ↔ ∃ m, n < m ∧ T.Provable (substNumeral ⌜T.yablo⌝ m) := by
+  simpa using yablo_diagonal_modeled n |>.not;
+
 lemma iff_yablo_provable (n : ℕ) : U ⊢!. T.yabloPred n ↔ U ⊢!. “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” := by
   suffices U ⊢!. T.yablo/[n] ⭤ “∀ m, ↑n < m → ∀ nσ, !ssnum nσ ⌜T.yablo⌝ m → ¬!T.provable (nσ)” by
     constructor <;> . intro h; cl_prover [h, this];
@@ -111,25 +114,17 @@ lemma iff_neg_yablo_provable (n : ℕ) : U ⊢!. ∼(T.yabloPred n) ↔ U ⊢!.
   apply oRing_provable₀_of.{0};
   intro V _ _;
   haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
-  suffices ¬(Semiformula.Eval (standardModel V) (fun i ↦ ORingStruc.numeral n) Empty.elim) (T.yablo) ↔ ∃ m, ORingStruc.numeral n < m ∧ T.Provable (substNumeral ⌜T.yablo⌝ m) by
-    simpa [models₀_iff, Matrix.comp_vecCons'];
-  haveI : ¬V ⊧/![ORingStruc.numeral n] (T.yablo) ↔ ∃ m, ORingStruc.numeral n < m ∧ Provable T (substNumeral ⌜T.yablo⌝ m) := by
-    simpa [YabloSystem, Matrix.cons_val_fin_one] using yablo_diagonal_modeled _ |>.not;
-  convert this;
-  simp;
+  haveI : ¬V ⊧/![ORingStruc.numeral n] (T.yablo) ↔ ∃ m, ORingStruc.numeral n < m ∧ Provable T (substNumeral ⌜T.yablo⌝ m) := yablo_diagonal_neg_modeled _;
+  simpa [models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons'] using this;
 
 lemma provable_greater_yablo {n m : ℕ} (hnm : n < m) : U ⊢!. T.yabloPred n ➝ T.yabloPred m := by
   apply oRing_provable₀_of.{0};
   intro V _ _;
   haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ U inferInstance;
-  suffices V ⊧/![(ORingStruc.numeral n)] (T.yablo) → V ⊧/![(ORingStruc.numeral m)] (T.yablo) by
-    simp only [
-      models₀_iff, LogicalConnective.HomClass.map_imply, Semiformula.eval_substs,
-      Matrix.cons_val_fin_one, Semiterm.val_operator₀, Structure.numeral_eq_numeral,
-      LogicalConnective.Prop.arrow_eq
-    ];
-    convert this <;> simp;
-  simp only [yablo_diagonal_modeled];
+  suffices
+    (∀ m, ORingStruc.numeral n < m → ¬Provable T (substNumeral ⌜yablo T⌝ m)) →
+    (∀ k, ORingStruc.numeral m < k → ¬Provable T (substNumeral ⌜yablo T⌝ k))
+    by simpa [models_iff, Matrix.constant_eq_singleton, Matrix.comp_vecCons', yablo_diagonal_modeled] using this;
   intro h k hmk;
   apply h;
   apply PeanoMinus.lt_trans _ _ _ (by simpa) hmk;