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

Equations

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

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

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

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

Equations

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

def LO.Arith.QQConj.blueprint : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : VecRec.Construction V 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ps : V) : V

Equations

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

Instances For

• LO.Arith.qqConj_definable
• LO.Arith.qqConj_definable'

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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : qqConj 0 = qqVerum

@[simp]

theorem LO.Arith.qqConj_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p ps : V) : qqConj (cons p ps) = qqAnd p (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ qqConj via FirstOrder.Arith.qqConjDef

@[simp]

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

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

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

@[simp]

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

@[simp]

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

def LO.Arith.QQDisj.blueprint : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : VecRec.Construction V 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ps : V) : V

Equations

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

Instances For

• LO.Arith.qqDisj_definable
• LO.Arith.qqDisj_definable'

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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : qqDisj 0 = qqFalsum

@[simp]

theorem LO.Arith.qqDisj_cons {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p ps : V) : qqDisj (cons p ps) = qqOr p (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ qqDisj via FirstOrder.Arith.qqDisjDef

@[simp]

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

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

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

@[simp]

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

def LO.Arith.Formalized.SubstItr.blueprint : 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : PR.Construction V blueprint

Equations

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

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

Equations

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

Instances For

• LO.Arith.Formalized.substItr_definable
• LO.Arith.Formalized.substItr_definable'

@[simp]

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

@[simp]

theorem LO.Arith.Formalized.substItr_succ {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (w p k : V) : substItr w p (k + 1) = cons (⌜ℒₒᵣ⌝.substs (cons (numeral k) w) p) (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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₃ substItr via FirstOrder.Arith.substItrDef

@[simp]

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

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

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

@[simp]

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

@[simp]

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

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

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

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

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

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

Equations

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

Instances For

• LO.Arith.qqVerums_definable
• LO.Arith.qqVerums_definable'

@[simp]

theorem LO.Arith.le_qqVerums {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) : k ≤ 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} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₁-Function₁ qqVerums via FirstOrder.Arith.qqVerumsDef

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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