feat: multidiagonal

Author: iehality

Incompleteness/Arith/Second.lean

@@ -1,5 +1,6 @@
 import Incompleteness.Arith.D3
 import Logic.Logic.HilbertStyle.Supplemental
+import Incompleteness.ToFoundation.Basic
 
 noncomputable section
 
@@ -15,7 +16,7 @@ def substNumeral (p x : V) : V := ⌜ℒₒᵣ⌝.substs₁ (numeral x) p
 
 lemma substNumeral_app_quote (σ : Semisentence ℒₒᵣ 1) (n : ℕ) :
     substNumeral ⌜σ⌝ (n : V) = ⌜(σ/[‘↑n’] : Sentence ℒₒᵣ)⌝ := by
-  simp [substNumeral]
+  dsimp [substNumeral]
   let w : Fin 1 → Semiterm ℒₒᵣ Empty 0 := ![‘↑n’]
   have : ?[numeral (n : V)] = (⌜fun i : Fin 1 ↦ ⌜w i⌝⌝ : V) := nth_ext' 1 (by simp) (by simp) (by simp)
   rw [Language.substs₁, this, quote_substs' (L := ℒₒᵣ)]
@@ -24,6 +25,22 @@ lemma substNumeral_app_quote_quote (σ π : Semisentence ℒₒᵣ 1) :
     substNumeral (⌜σ⌝ : V) ⌜π⌝ = ⌜(σ/[⌜π⌝] : Sentence ℒₒᵣ)⌝ := by
   simpa [coe_quote, quote_eq_encode] using substNumeral_app_quote σ ⌜π⌝
 
+def substNumerals (p : V) (v : Fin k → V) : V := ⌜ℒₒᵣ⌝.substs ⌜fun i ↦ numeral (v i)⌝ p
+
+lemma substNumerals_app_quote (σ : Semisentence ℒₒᵣ k) (v : Fin k → ℕ) :
+    (substNumerals ⌜σ⌝ (v ·) : V) = ⌜((Rew.substs (fun i ↦ ‘↑(v i)’)).hom σ : Sentence ℒₒᵣ)⌝ := by
+  dsimp [substNumerals]
+  let w : Fin k → Semiterm ℒₒᵣ Empty 0 := fun i ↦ ‘↑(v i)’
+  have : ⌜fun i ↦ numeral (v i : V)⌝ = (⌜fun i : Fin k ↦ ⌜w i⌝⌝ : V) := by
+    apply nth_ext' (k : V) (by simp) (by simp)
+    intro i hi; rcases eq_fin_of_lt_nat hi with ⟨i, rfl⟩
+    simp [w]
+  rw [this, quote_substs' (L := ℒₒᵣ)]
+
+lemma substNumerals_app_quote_quote (σ : Semisentence ℒₒᵣ k) (π : Fin k → Semisentence ℒₒᵣ k) :
+    substNumerals (⌜σ⌝ : V) (fun i ↦ ⌜π i⌝) = ⌜((Rew.substs (fun i ↦ ⌜π i⌝)).hom σ : Sentence ℒₒᵣ)⌝ := by
+  simpa [coe_quote, quote_eq_encode] using substNumerals_app_quote σ (fun i ↦ ⌜π i⌝)
+
 section
 
 def _root_.LO.FirstOrder.Arith.ssnum : 𝚺₁.Semisentence 3 := .mkSigma
@@ -35,6 +52,29 @@ lemma substNumeral_defined : 𝚺₁-Function₂ (substNumeral : V → V → V)
 @[simp] lemma eval_ssnum (v) :
     Semiformula.Evalbm V v ssnum.val ↔ v 0 = substNumeral (v 1) (v 2) := substNumeral_defined.df.iff v
 
+def _root_.LO.FirstOrder.Arith.ssnums : 𝚺₁.Semisentence (k + 2) := .mkSigma
+  “y p. ∃ n, !lenDef ↑k n ∧
+    (⋀ i, ∃ z, !nthDef z n ↑(i : Fin k) ∧ !numeralDef z #i.succ.succ.succ.succ) ∧
+    !p⌜ℒₒᵣ⌝.substsDef y n p” (by simp)
+
+lemma substNumerals_defined :
+    Arith.HierarchySymbol.DefinedFunction (fun v ↦ substNumerals (v 0) (v ·.succ) : (Fin (k + 1) → V) → V) ssnums := by
+  intro v
+  suffices
+    (v 0 = ⌜ℒₒᵣ⌝.substs ⌜fun (i : Fin k) ↦ numeral (v i.succ.succ)⌝ (v 1)) ↔
+      ∃ x, ↑k = len x ∧ (∀ (i : Fin k), x.[↑↑i] = numeral (v i.succ.succ)) ∧ v 0 = ⌜ℒₒᵣ⌝.substs x (v 1) by
+    simpa [ssnums, ⌜ℒₒᵣ⌝.substs_defined.df.iff, substNumerals, numeral_eq_natCast] using this
+  constructor
+  · intro e
+    refine ⟨_, by simp, by intro i; simp, e⟩
+  · rintro ⟨w, hk, h, e⟩
+    have : w = ⌜fun (i : Fin k) ↦ numeral (v i.succ.succ)⌝ := nth_ext' (k : V) hk.symm (by simp)
+      (by intro i hi; rcases eq_fin_of_lt_nat hi with ⟨i, rfl⟩; simp [h])
+    rcases this; exact e
+
+@[simp] lemma eval_ssnums (v : Fin (k + 2) → V) :
+    Semiformula.Evalbm V v ssnums.val ↔ v 0 = substNumerals (v 1) (fun i ↦ v i.succ.succ) := substNumerals_defined.df.iff v
+
 end
 
 end LO.Arith.Formalized
@@ -73,6 +113,32 @@ theorem diagonal (θ : Semisentence ℒₒᵣ 1) :
 
 end Diagonalization
 
+section Multidiagonalization
+
+/-- $\mathrm{diag}_i(\vec{x}) := (\forall \vec{y})\left[ \left(\bigwedge_j \mathrm{ssnums}(y_j, x_j, \vec{x})\right) \to \theta_i(\vec{y}) \right]$ -/
+def multidiag (θ : Semisentence ℒₒᵣ k) : Semisentence ℒₒᵣ k :=
+  ∀^[k] (
+    (Matrix.conj fun j : Fin k ↦ (Rew.substs <| #(j.addCast k) :> #(j.addNat k) :> fun l ↦ #(l.addNat k)).hom ssnums.val) ➝
+    (Rew.substs fun j ↦ #(j.addCast k)).hom θ)
+
+def multifixpoint (θ : Fin k → Semisentence ℒₒᵣ k) (i : Fin k) : Sentence ℒₒᵣ := (Rew.substs fun j ↦ ⌜multidiag (θ j)⌝).hom (multidiag (θ i))
+
+theorem multidiagonal (θ : Fin k → Semisentence ℒₒᵣ k) :
+    T ⊢!. multifixpoint θ i ⭤ (Rew.substs fun j ↦ ⌜multifixpoint θ j⌝).hom (θ i) :=
+  haveI : 𝐄𝐐 ≼ T := System.Subtheory.comp (𝓣 := 𝐈𝚺₁) inferInstance inferInstance
+  complete (T := T) <| oRing_consequence_of _ _ fun (V : Type) _ _ ↦ by
+    haveI : V ⊧ₘ* 𝐈𝚺₁ := ModelsTheory.of_provably_subtheory V 𝐈𝚺₁ T inferInstance inferInstance
+    suffices V ⊧/![] (multifixpoint θ i) ↔ V ⊧/(fun i ↦ ⌜multifixpoint θ i⌝) (θ i) by simpa [models_iff]
+    let t : Fin k → V := fun i ↦ ⌜multidiag (θ i)⌝
+    have ht : ∀ i, substNumerals (t i) t = ⌜multifixpoint θ i⌝ := by
+      intro i; simp [t, multifixpoint, substNumerals_app_quote_quote]
+    calc
+      V ⊧/![] (multifixpoint θ i) ↔ V ⊧/t (multidiag (θ i))                 := by simp [multifixpoint]
+      _                      ↔ V ⊧/(fun i ↦ substNumerals (t i) t) (θ i) := by simp [multidiag, ←Function.funext_iff]
+      _                      ↔ V ⊧/(fun i ↦ ⌜multifixpoint θ i⌝) (θ i) := by simp [ht]
+
+end Multidiagonalization
+
 section
 
 variable (U : Theory ℒₒᵣ) [U.Delta1Definable]

Incompleteness/ToFoundation/Basic.lean

@@ -0,0 +1,37 @@
+import Logic.FirstOrder.Arith.Hierarchy
+
+namespace Fin
+
+@[inline] def addCast (m) : Fin n → Fin (m + n) :=
+  castLE <| Nat.le_add_left n m
+
+@[simp] lemma addCast_val (i : Fin n) : (i.addCast m : ℕ) = i := rfl
+
+end Fin
+
+namespace Matrix
+
+variable {α : Type*}
+
+@[simp] lemma appeendr_addCast (u : Fin m → α) (v : Fin n → α) (i : Fin m) :
+    appendr u v (i.addCast n) = u i := by simp [appendr, vecAppend_eq_ite]
+
+@[simp] lemma appeendr_addNat (u : Fin m → α) (v : Fin n → α) (i : Fin n) :
+    appendr u v (i.addNat m) = v i := by simp [appendr, vecAppend_eq_ite]
+
+end Matrix
+
+namespace LO.FirstOrder
+
+variable {L : Language}
+
+namespace Semiformula
+
+open Rew
+
+variable (ω : Rew L ξ₁ n₁ ξ₂ n₂)
+
+
+end Semiformula
+
+end LO.FirstOrder