add Iteration

Arithmetization/ISigmaOne/Metamath/Formula/Basic.lean

@@ -368,7 +368,10 @@ instance uformulaDef_definable : 𝚫₁-Predicate L.UFormula := Defined.to_defi
 
 def Language.Semiformula (n p : V) : Prop := L.UFormula p ∧ n = fstIdx p
 
-def Language.Formula (p : V) : Prop := L.Semiformula 0 p
+abbrev Language.Formula (p : V) : Prop := L.Semiformula 0 p
+
+lemma Language.UFormula.toSemiformula {p} (h : L.UFormula p) : L.Semiformula (fstIdx p) p :=
+  ⟨h, by rfl⟩
 
 def _root_.LO.FirstOrder.Arith.LDef.isSemiformulaDef (pL : LDef) : 𝚫₁-Semisentence 2 := .mkDelta
   (.mkSigma “n p | !pL.uformulaDef.sigma p ∧ !fstIdxDef n p” (by simp))
@@ -393,10 +396,10 @@ lemma Language.UFormula.case_iff {p : V} :
     (∃ n k r v, L.Rel k r ∧ L.SemitermVec k n v ∧ p = ^nrel n k r v) ∨
     (∃ n, p = ^⊤[n]) ∨
     (∃ n, p = ^⊥[n]) ∨
-    (∃ n q r, (𝐔 q ∧ n = fstIdx q) ∧ (𝐔 r ∧ n = fstIdx r) ∧ p = q ^⋏[n] r) ∨
-    (∃ n q r, (𝐔 q ∧ n = fstIdx q) ∧ (𝐔 r ∧ n = fstIdx r) ∧ p = q ^⋎[n] r) ∨
-    (∃ n q, (𝐔 q ∧ n + 1 = fstIdx q) ∧ p = ^∀[n] q) ∨
-    (∃ n q, (𝐔 q ∧ n + 1 = fstIdx q) ∧ p = ^∃[n] q) :=
+    (∃ n q r, L.Semiformula n q ∧ L.Semiformula n r ∧ p = q ^⋏[n] r) ∨
+    (∃ n q r, L.Semiformula n q ∧ L.Semiformula n r ∧ p = q ^⋎[n] r) ∨
+    (∃ n q, L.Semiformula (n + 1) q ∧ p = ^∀[n] q) ∨
+    (∃ n q, L.Semiformula (n + 1) q ∧ p = ^∃[n] q) :=
   (construction L).case
 
 alias ⟨Language.UFormula.case, Language.UFormula.mk⟩ := Language.UFormula.case_iff
@@ -469,6 +472,15 @@ alias ⟨Language.UFormula.case, Language.UFormula.mk⟩ := Language.UFormula.ca
    by rintro hp
       exact Language.UFormula.mk (Or.inr <| Or.inr <| Or.inr <| Or.inr <| Or.inr <| Or.inr <| Or.inr ⟨n, p, hp, rfl⟩)⟩
 
+lemma Language.UFormula.pos {p : V} (h : L.UFormula p) : 0 < p := by
+  rcases h.case with (⟨_, _, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ |
+    ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, rfl⟩ | ⟨_, _, _, rfl⟩) <;>
+    simp [qqRel, qqNRel, qqVerum, qqFalsum, qqAnd, qqOr, qqAll, qqEx]
+
+@[simp] lemma Language.UFormula.not_zero : ¬L.UFormula (0 : V) := by intro h; simpa using h.pos
+
+lemma Language.Semiformula.pos {n p : V} (h : L.Semiformula n p) : 0 < p := h.1.pos
+
 @[simp] lemma Language.Semiformula.rel {n k r v : V} :
     L.Semiformula n (^rel n k r v) ↔ L.Rel k r ∧ L.SemitermVec k n v := by simp [Language.Semiformula]
 @[simp] lemma Language.Semiformula.nrel {n k r v : V} :

Arithmetization/ISigmaOne/Metamath/Formula/Functions.lean

@@ -105,7 +105,15 @@ end
 @[simp] lemma neg_ex {n p} (hp : L.Semiformula (n + 1) p) :
     L.neg (^∃[n] p) = ^∀[n] (L.neg p) := by simp [Language.neg, hp, construction]
 
-@[simp] lemma Language.Semiformula.neg {p : V} : L.Semiformula n p → L.Semiformula n (L.neg p) := by
+lemma neg_not_uformula {x} (h : ¬L.UFormula x) :
+    L.neg x = 0 := (construction L).result_prop_not _ h
+
+lemma fstIdx_neg {p} (h : L.UFormula p) : fstIdx (L.neg p) = fstIdx p := by
+  rcases h.case with (⟨_, _, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ |
+    ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, rfl⟩ | ⟨_, _, _, rfl⟩) <;>
+    simp [*]
+
+lemma Language.Semiformula.neg {p : V} : L.Semiformula n p → L.Semiformula n (L.neg p) := by
   apply Language.Semiformula.induction_sigma₁
   · definability
   · intro n k r v hr hv; simp [hr, hv]
@@ -117,6 +125,15 @@ end
   · intro n p hp ihp; simp [hp, ihp]
   · intro n p hp ihp; simp [hp, ihp]
 
+@[simp] lemma Language.Semiformula.neg_iff {p : V} : L.Semiformula n (L.neg p) ↔ L.Semiformula n p :=
+  ⟨fun h ↦ by
+    rcases h with ⟨h, rfl⟩
+    have : L.UFormula p := by
+      by_contra hp
+      simp [neg_not_uformula hp] at h
+    exact ⟨this, by simp [fstIdx_neg this]⟩,
+    Language.Semiformula.neg⟩
+
 @[simp] lemma neg_neg {p : V} : L.Semiformula n p → L.neg (L.neg p) = p := by
   apply Language.Semiformula.induction_sigma₁
   · definability
@@ -225,7 +242,10 @@ end
 @[simp] lemma shift_ex {n p} (hp : L.Semiformula (n + 1) p) :
     L.shift (^∃[n] p) = ^∃[n] (L.shift p) := by simp [Language.shift, hp, construction]
 
-@[simp] lemma Language.Semiformula.shift {p : V} : L.Semiformula n p → L.Semiformula n (L.shift p) := by
+lemma shift_not_uformula {x} (h : ¬L.UFormula x) :
+    L.shift x = 0 := (construction L).result_prop_not _ h
+
+lemma Language.Semiformula.shift {p : V} : L.Semiformula n p → L.Semiformula n (L.shift p) := by
   apply Language.Semiformula.induction_sigma₁
   · definability
   · intro n k r v hr hv; simp [hr, hv]
@@ -237,6 +257,20 @@ end
   · intro n p hp ihp; simp [hp, ihp]
   · intro n p hp ihp; simp [hp, ihp]
 
+lemma fstIdx_shift {p} (h : L.UFormula p) : fstIdx (L.shift p) = fstIdx p := by
+  rcases h.case with (⟨_, _, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, _, rfl⟩ | ⟨_, rfl⟩ | ⟨_, rfl⟩ |
+    ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, _, _, rfl⟩ | ⟨_, _, _, rfl⟩ | ⟨_, _, _, rfl⟩) <;>
+    simp [*]
+
+@[simp] lemma Language.Semiformula.shift_iff {p : V} : L.Semiformula n (L.shift p) ↔ L.Semiformula n p :=
+  ⟨fun h ↦ by
+    rcases h with ⟨h, rfl⟩
+    have : L.UFormula p := by
+      by_contra hp
+      simp [shift_not_uformula hp] at h
+    exact ⟨this, by simp [fstIdx_shift this]⟩,
+    Language.Semiformula.shift⟩
+
 end shift
 
 section substs
@@ -427,6 +461,9 @@ lemma semiformula_subst_induction {P : V → V → V → V → V → Prop} (hP :
     intro n m w p _ ih hw
     simpa using ih hw.qVec
 
+lemma substs_not_uformula {m w x} (h : ¬L.UFormula x) :
+    L.substs m w x = 0 := (construction L).result_prop_not _ h
+
 end substs
 
 end LO.Arith

Arithmetization/ISigmaOne/Metamath/Formula/Iteration.lean

@@ -0,0 +1,140 @@
+import Arithmetization.ISigmaOne.Metamath.Formula.Functions
+
+
+noncomputable section
+
+namespace LO.Arith
+
+open FirstOrder FirstOrder.Arith
+
+variable {V : Type*} [Zero V] [One V] [Add V] [Mul V] [LT V] [V ⊧ₘ* 𝐈𝚺₁]
+
+variable {L : Arith.Language V} {pL : LDef} [Arith.Language.Defined L pL]
+
+namespace QQConj
+
+def blueprint : VecRec.Blueprint 1 where
+  nil := .mkSigma “y n | !qqVerumDef y n” (by simp)
+  cons := .mkSigma “y p ps ih n | !qqAndDef y n p ih” (by simp)
+
+def construction : VecRec.Construction V blueprint where
+  nil (param) := ^⊤[param 0]
+  cons (param) p _ ih := p ^⋏[param 0] ih
+  nil_defined := by intro v; simp [blueprint]
+  cons_defined := by intro v; simp [blueprint]; rfl
+
+end QQConj
+
+section qqConj
+
+open QQConj
+
+def qqConj (n ps : V) : V := construction.result ![n] ps
+
+scoped notation:65 "^⋀[" n "] " ps:66 => qqConj n ps
+
+@[simp] lemma qqConj_nil (n : V) : ^⋀[n] 0 = ^⊤[n] := by simp [qqConj, construction]
+
+@[simp] lemma qqConj_cons (n p ps : V) : ^⋀[n] (p ∷ ps) = p ^⋏[n] (^⋀[n] ps) := by simp [qqConj, construction]
+
+section
+
+def _root_.LO.FirstOrder.Arith.qqConjDef : 𝚺₁-Semisentence 3 := blueprint.resultDef.rew (Rew.substs ![#0, #2, #1])
+
+lemma qqConj_defined : 𝚺₁-Function₂ (qqConj : V → V → V) via qqConjDef := by
+  intro v; simpa [qqConjDef] using construction.result_defined ![v 0, v 2, v 1]
+
+@[simp] lemma eval_qqConj (v) :
+    Semiformula.Evalbm V v qqConjDef.val ↔ v 0 = qqConj (v 1) (v 2) := qqConj_defined.df.iff v
+
+instance qqConj_definable : 𝚺₁-Function₂ (qqConj : V → V → V) := Defined.to_definable _ qqConj_defined
+
+instance qqConj_definable' (Γ) : (Γ, m + 1)-Function₂ (qqConj : V → V → V) := .of_sigmaOne qqConj_definable _ _
+
+end
+
+@[simp]
+lemma qqConj_semiformula {n ps : V} :
+    L.Semiformula n (^⋀[n] ps) ↔ (∀ i < len ps, L.Semiformula n ps.[i]) := by
+  induction ps using cons_induction_sigma₁
+  · definability
+  case nil => simp
+  case cons p ps ih =>
+    simp [ih]
+    constructor
+    · rintro ⟨hp, hps⟩ i hi
+      rcases zero_or_succ i with (rfl | ⟨i, rfl⟩)
+      · simpa using hp
+      · simpa using hps i (by simpa using hi)
+    · intro h
+      exact ⟨
+        by simpa using h 0 (by simp),
+        fun i hi ↦ by simpa using h (i + 1) (by simpa using hi)⟩
+
+end qqConj
+
+namespace QQDisj
+
+def blueprint : VecRec.Blueprint 1 where
+  nil := .mkSigma “y n | !qqFalsumDef y n” (by simp)
+  cons := .mkSigma “y p ps ih n | !qqOrDef y n p ih” (by simp)
+
+def construction : VecRec.Construction V blueprint where
+  nil (param) := ^⊥[param 0]
+  cons (param) p _ ih := p ^⋎[param 0] ih
+  nil_defined := by intro v; simp [blueprint]
+  cons_defined := by intro v; simp [blueprint]; rfl
+
+end QQDisj
+
+section qqDisj
+
+open QQDisj
+
+def qqDisj (n ps : V) : V := construction.result ![n] ps
+
+scoped notation:65 "^⋁[" n "] " ps:66 => qqDisj n ps
+
+@[simp] lemma qqDisj_nil (n : V) : ^⋁[n] 0 = ^⊥[n] := by simp [qqDisj, construction]
+
+@[simp] lemma qqDisj_cons (n p ps : V) : ^⋁[n] (p ∷ ps) = p ^⋎[n] (^⋁[n] ps) := by simp [qqDisj, construction]
+
+section
+
+def _root_.LO.FirstOrder.Arith.qqDisjDef : 𝚺₁-Semisentence 3 := blueprint.resultDef.rew (Rew.substs ![#0, #2, #1])
+
+lemma qqDisj_defined : 𝚺₁-Function₂ (qqDisj : V → V → V) via qqDisjDef := by
+  intro v; simpa [qqDisjDef] using construction.result_defined ![v 0, v 2, v 1]
+
+@[simp] lemma eval_qqDisj (v) :
+    Semiformula.Evalbm V v qqDisjDef.val ↔ v 0 = qqDisj (v 1) (v 2) := qqDisj_defined.df.iff v
+
+instance qqDisj_definable : 𝚺₁-Function₂ (qqDisj : V → V → V) := Defined.to_definable _ qqDisj_defined
+
+instance qqDisj_definable' (Γ) : (Γ, m + 1)-Function₂ (qqDisj : V → V → V) := .of_sigmaOne qqDisj_definable _ _
+
+end
+
+@[simp]
+lemma qqDisj_semiformula {n ps : V} :
+    L.Semiformula n (^⋁[n] ps) ↔ (∀ i < len ps, L.Semiformula n ps.[i]) := by
+  induction ps using cons_induction_sigma₁
+  · definability
+  case nil => simp
+  case cons p ps ih =>
+    simp [ih]
+    constructor
+    · rintro ⟨hp, hps⟩ i hi
+      rcases zero_or_succ i with (rfl | ⟨i, rfl⟩)
+      · simpa using hp
+      · simpa using hps i (by simpa using hi)
+    · intro h
+      exact ⟨
+        by simpa using h 0 (by simp),
+        fun i hi ↦ by simpa using h (i + 1) (by simpa using hi)⟩
+
+end qqDisj
+
+end LO.Arith
+
+end

Arithmetization/ISigmaOne/Metamath/Term/Functions.lean

@@ -99,6 +99,13 @@ lemma nth_termSubstVec {k n ts i : V} (hts : L.SemitermVec k n ts) (hi : i < k)
     (L.termSubstVec k n m w ts).[i] = L.termSubst n m w ts.[i] :=
   (construction L).nth_resultVec _ hts hi
 
+@[simp] lemma termSubstVec_nil (n : V) : L.termSubstVec 0 n m w 0 = 0 :=
+  (construction L).resultVec_nil _ _
+
+lemma termSubstVec_cons {k n t ts : V} (ht : L.Semiterm n t) (hts : L.SemitermVec k n ts) :
+    L.termSubstVec (k + 1) n m w (t ∷ ts) = L.termSubst n m w t ∷ L.termSubstVec k n m w ts :=
+  (construction L).resultVec_cons ![m, w] hts ht
+
 @[simp] lemma termSubst_rng_semiterm {t} (hw : L.SemitermVec n m w) (ht : L.Semiterm n t) : L.Semiterm m (L.termSubst n m w t) := by
   apply Language.Semiterm.induction 𝚺 ?_ ?_ ?_ ?_ t ht
   · definability
@@ -199,6 +206,13 @@ lemma nth_termShiftVec {k n ts i : V} (hts : L.SemitermVec k n ts) (hi : i < k)
     (L.termShiftVec k n ts).[i] = L.termShift n ts.[i] :=
   (construction L).nth_resultVec _ hts hi
 
+@[simp] lemma termShiftVec_nil (n : V) : L.termShiftVec 0 n 0 = 0 :=
+  (construction L).resultVec_nil ![] _
+
+lemma termShiftVec_cons {k n t ts : V} (ht : L.Semiterm n t) (hts : L.SemitermVec k n ts) :
+    L.termShiftVec (k + 1) n (t ∷ ts) = L.termShift n t ∷ L.termShiftVec k n ts :=
+  (construction L).resultVec_cons ![] hts ht
+
 @[simp] lemma Language.Semiterm.termShift {t} (ht : L.Semiterm n t) : L.Semiterm n (L.termShift n t) := by
   apply Language.Semiterm.induction 𝚺 ?_ ?_ ?_ ?_ t ht
   · definability
@@ -298,6 +312,13 @@ end
     (L.termBShiftVec k n ts).[i] = L.termBShift n ts.[i] :=
   (construction L).nth_resultVec _ hts hi
 
+@[simp] lemma termBShiftVec_nil (n : V) : L.termBShiftVec 0 n 0 = 0 :=
+  (construction L).resultVec_nil ![] _
+
+lemma termBShiftVec_cons {k n t ts : V} (ht : L.Semiterm n t) (hts : L.SemitermVec k n ts) :
+    L.termBShiftVec (k + 1) n (t ∷ ts) = L.termBShift n t ∷ L.termBShiftVec k n ts :=
+  (construction L).resultVec_cons ![] hts ht
+
 @[simp] lemma Language.Semiterm.termBShift {t} (ht : L.Semiterm n t) : L.Semiterm (n + 1) (L.termBShift n t) := by
   apply Language.Semiterm.induction 𝚺 ?_ ?_ ?_ ?_ t ht
   · definability