def LO.FirstOrder.Semiformula.replicate {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : ℕ → LO.FirstOrder.Semiformula L ξ n

Equations

• p.replicate 0 = p
• p.replicate k.succ = p ⋏ p.replicate k

theorem LO.FirstOrder.Semiformula.replicate_zero {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) : p.replicate 0 = p

theorem LO.FirstOrder.Semiformula.replicate_succ {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (p : LO.FirstOrder.Semiformula L ξ n) (k : ℕ) : p.replicate (k + 1) = p ⋏ p.replicate k

def LO.FirstOrder.Semiformula.weight {L : LO.FirstOrder.Language} {ξ : Type u_1} {n : ℕ} (k : ℕ) : LO.FirstOrder.Semiformula L ξ n

Equations

• LO.FirstOrder.Semiformula.weight k = (List.replicate k ⊤).conj

def LO.Arith.QQConj.blueprint : LO.Arith.VecRec.Blueprint 0

Equations

• One or more equations did not get rendered due to their size.

def LO.Arith.QQConj.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.VecRec.Construction V LO.Arith.QQConj.blueprint

Equations

• LO.Arith.QQConj.construction = { nil := fun (x : Fin 0 → V) => LO.Arith.qqVerum, cons := fun (x : Fin 0 → V) (p x ih : V) => LO.Arith.qqAnd p ih, nil_defined := ⋯, cons_defined := ⋯ }

def LO.Arith.qqConj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ps : V) : V

Equations

• LO.Arith.qqConj ps = LO.Arith.QQConj.construction.result ![] ps

def LO.Arith.«term^⋀_» : Lean.ParserDescr

Equations

• LO.Arith.«term^⋀_» = Lean.ParserDescr.node `LO.Arith.term^⋀_ 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^⋀ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem LO.Arith.qqConj_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.qqConj 0 = LO.Arith.qqVerum

@[simp]

theorem LO.Arith.qqConj_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) (ps : V) : LO.Arith.qqConj (cons p ps) = LO.Arith.qqAnd p (LO.Arith.qqConj ps)

def LO.FirstOrder.Arith.qqConjDef : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arith.qqConjDef = LO.Arith.QQConj.blueprint.resultDef

theorem LO.Arith.qqConj_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.qqConj via LO.FirstOrder.Arith.qqConjDef

@[simp]

theorem LO.Arith.eval_qqConj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqConjDef) ↔ v 0 = LO.Arith.qqConj (v 1)

instance LO.Arith.qqConj_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.qqConj

Equations

• ⋯ = ⋯

instance LO.Arith.qqConj_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.qqConj

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.qqConj_semiformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {ps : V} : L.IsSemiformula n (LO.Arith.qqConj ps) ↔ ∀ i < LO.Arith.len ps, L.IsSemiformula n (LO.Arith.nth ps i)

@[simp]

theorem LO.Arith.len_le_conj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ps : V) : LO.Arith.len ps ≤ LO.Arith.qqConj ps

def LO.Arith.QQDisj.blueprint : LO.Arith.VecRec.Blueprint 0

Equations

• One or more equations did not get rendered due to their size.

def LO.Arith.QQDisj.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.VecRec.Construction V LO.Arith.QQDisj.blueprint

Equations

• LO.Arith.QQDisj.construction = { nil := fun (x : Fin 0 → V) => LO.Arith.qqFalsum, cons := fun (x : Fin 0 → V) (p x ih : V) => LO.Arith.qqOr p ih, nil_defined := ⋯, cons_defined := ⋯ }

def LO.Arith.qqDisj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ps : V) : V

Equations

• LO.Arith.qqDisj ps = LO.Arith.QQDisj.construction.result ![] ps

def LO.Arith.«term^⋁_» : Lean.ParserDescr

Equations

• LO.Arith.«term^⋁_» = Lean.ParserDescr.node `LO.Arith.term^⋁_ 65 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^⋁ ") (Lean.ParserDescr.cat `term 66))

@[simp]

theorem LO.Arith.qqDisj_nil {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.qqDisj 0 = LO.Arith.qqFalsum

@[simp]

theorem LO.Arith.qqDisj_cons {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) (ps : V) : LO.Arith.qqDisj (cons p ps) = LO.Arith.qqOr p (LO.Arith.qqDisj ps)

def LO.FirstOrder.Arith.qqDisjDef : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arith.qqDisjDef = LO.Arith.QQDisj.blueprint.resultDef

theorem LO.Arith.qqDisj_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.qqDisj via LO.FirstOrder.Arith.qqDisjDef

@[simp]

theorem LO.Arith.eval_qqDisj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqDisjDef) ↔ v 0 = LO.Arith.qqDisj (v 1)

instance LO.Arith.qqDisj_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.qqDisj

Equations

• ⋯ = ⋯

instance LO.Arith.qqDisj_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : ℕ} (Γ : LO.SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.qqDisj

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.qqDisj_semiformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {ps : V} : L.IsSemiformula n (LO.Arith.qqDisj ps) ↔ ∀ i < LO.Arith.len ps, L.IsSemiformula n (LO.Arith.nth ps i)

def LO.Arith.Formalized.SubstItr.blueprint : LO.Arith.PR.Blueprint 2

Equations

• One or more equations did not get rendered due to their size.

def LO.Arith.Formalized.SubstItr.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.PR.Construction V LO.Arith.Formalized.SubstItr.blueprint

Equations

• One or more equations did not get rendered due to their size.

def LO.Arith.Formalized.substItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (w : V) (p : V) (k : V) : V

Equations

• LO.Arith.Formalized.substItr w p k = LO.Arith.Formalized.SubstItr.construction.result ![w, p] k

@[simp]

theorem LO.Arith.Formalized.substItr_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (w : V) (p : V) : LO.Arith.Formalized.substItr w p 0 = 0

@[simp]

theorem LO.Arith.Formalized.substItr_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (w : V) (p : V) (k : V) : LO.Arith.Formalized.substItr w p (k + 1) = cons (⌜ℒₒᵣ⌝.substs (cons (LO.Arith.Formalized.numeral k) w) p) (LO.Arith.Formalized.substItr w p k)

def LO.FirstOrder.Arith.substItrDef : 𝚺₁.Semisentence 4

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.Formalized.substItr_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₃ LO.Arith.Formalized.substItr via LO.FirstOrder.Arith.substItrDef

@[simp]

theorem LO.Arith.Formalized.substItr_defined_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 4 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.substItrDef) ↔ v 0 = LO.Arith.Formalized.substItr (v 1) (v 2) (v 3)

instance LO.Arith.Formalized.substItr_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₃ LO.Arith.Formalized.substItr

Equations

• ⋯ = ⋯

instance LO.Arith.Formalized.substItr_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₃ LO.Arith.Formalized.substItr

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Formalized.len_substItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (w : V) (p : V) (k : V) : LO.Arith.len (LO.Arith.Formalized.substItr w p k) = k

@[simp]

theorem LO.Arith.Formalized.substItr_nth {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (w : V) (p : V) (k : V) {i : V} (hi : i < k) : LO.Arith.nth (LO.Arith.Formalized.substItr w p k) i = ⌜ℒₒᵣ⌝.substs (cons (LO.Arith.Formalized.numeral (k - (i + 1))) w) p

theorem LO.Arith.Formalized.neg_conj_substItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {n : V} {w : V} {p : V} {k : V} (hp : ⌜ℒₒᵣ⌝.IsSemiformula (n + 1) p) (hw : ⌜ℒₒᵣ⌝.IsSemitermVec n m w) : ⌜ℒₒᵣ⌝.neg (LO.Arith.qqConj (LO.Arith.Formalized.substItr w p k)) = LO.Arith.qqDisj (LO.Arith.Formalized.substItr w (⌜ℒₒᵣ⌝.neg p) k)

theorem LO.Arith.Formalized.neg_disj_substItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {m : V} {n : V} {w : V} {p : V} {k : V} (hp : ⌜ℒₒᵣ⌝.IsSemiformula (n + 1) p) (hw : ⌜ℒₒᵣ⌝.IsSemitermVec n m w) : ⌜ℒₒᵣ⌝.neg (LO.Arith.qqDisj (LO.Arith.Formalized.substItr w p k)) = LO.Arith.qqConj (LO.Arith.Formalized.substItr w (⌜ℒₒᵣ⌝.neg p) k)

theorem LO.Arith.Formalized.substs_conj_substItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {n : V} {m : V} {l : V} {w : V} {p : V} {k : V} (hp : ⌜ℒₒᵣ⌝.IsSemiformula (n + 1) p) (hw : ⌜ℒₒᵣ⌝.IsSemitermVec n m w) (hv : ⌜ℒₒᵣ⌝.IsSemitermVec m l v) : ⌜ℒₒᵣ⌝.substs v (LO.Arith.qqConj (LO.Arith.Formalized.substItr w p k)) = LO.Arith.qqConj (LO.Arith.Formalized.substItr (⌜ℒₒᵣ⌝.termSubstVec n v w) p k)

theorem LO.Arith.Formalized.substs_disj_substItr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {v : V} {n : V} {m : V} {l : V} {w : V} {p : V} {k : V} (hp : ⌜ℒₒᵣ⌝.IsSemiformula (n + 1) p) (hw : ⌜ℒₒᵣ⌝.IsSemitermVec n m w) (hv : ⌜ℒₒᵣ⌝.IsSemitermVec m l v) : ⌜ℒₒᵣ⌝.substs v (LO.Arith.qqDisj (LO.Arith.Formalized.substItr w p k)) = LO.Arith.qqDisj (LO.Arith.Formalized.substItr (⌜ℒₒᵣ⌝.termSubstVec n v w) p k)

def LO.Arith.qqVerums {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) : V

Equations

• LO.Arith.qqVerums k = LO.Arith.qqConj (LO.Arith.repeatVec LO.Arith.qqVerum k)

@[simp]

theorem LO.Arith.le_qqVerums {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) : k ≤ LO.Arith.qqVerums k

def LO.FirstOrder.Arith.qqVerumsDef : 𝚺₁.Semisentence 2

Equations

• One or more equations did not get rendered due to their size.

theorem LO.Arith.qqVerums_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.qqVerums via LO.FirstOrder.Arith.qqVerumsDef

@[simp]

theorem LO.Arith.qqVerums_repeatVec {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (v : Fin 2 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val LO.FirstOrder.Arith.qqVerumsDef) ↔ v 0 = LO.Arith.qqVerums (v 1)

instance LO.Arith.qqVerums_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ LO.Arith.qqVerums

Equations

• ⋯ = ⋯

instance LO.Arith.qqVerums_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ LO.Arith.qqVerums

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Language.IsSemiformula.qqVerums {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} (k : V) : L.IsSemiformula n (LO.Arith.qqVerums k)

@[simp]

theorem LO.Arith.qqVerums_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : LO.Arith.qqVerums 0 = LO.Arith.qqVerum

@[simp]

theorem LO.Arith.qqVerums_succ {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) : LO.Arith.qqVerums (k + 1) = LO.Arith.qqAnd LO.Arith.qqVerum (LO.Arith.qqVerums k)