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.FirstOrder.Arithmetic.Bootstrapping.QQConj.blueprint : VecRec.Blueprint 0

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.QQConj.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : VecRec.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqConj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ps : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqConj ps = LO.FirstOrder.Arithmetic.Bootstrapping.QQConj.construction.result ![] ps

def LO.FirstOrder.Arithmetic.Bootstrapping.qqConjGraph : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqConjGraph = LO.FirstOrder.Arithmetic.Bootstrapping.QQConj.blueprint.resultDef

def LO.FirstOrder.Arithmetic.Bootstrapping.«term^⋀_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqConj_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : qqConj 0 = qqVerum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqConj_cons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p ps : V) : qqConj (adjoin p ps) = qqAnd p (qqConj ps)

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqConj.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ qqConj via qqConjGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqConj.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ qqConj

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqConj.definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ qqConj

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqConj_semiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n ps : V} : IsSemiformula L n (qqConj ps) ↔ ∀ i < len ps, IsSemiformula L n (nth ps i)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.len_le_conj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ps : V) : len ps ≤ qqConj ps

def LO.FirstOrder.Arithmetic.Bootstrapping.QQDisj.blueprint : VecRec.Blueprint 0

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.QQDisj.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : VecRec.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ps : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj ps = LO.FirstOrder.Arithmetic.Bootstrapping.QQDisj.construction.result ![] ps

def LO.FirstOrder.Arithmetic.Bootstrapping.qqDisjGraph : 𝚺₁.Semisentence 2

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqDisjGraph = LO.FirstOrder.Arithmetic.Bootstrapping.QQDisj.blueprint.resultDef

def LO.FirstOrder.Arithmetic.Bootstrapping.«term^⋁_» : Lean.ParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj_nil {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : qqDisj 0 = qqFalsum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj_cons {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p ps : V) : qqDisj (adjoin p ps) = qqOr p (qqDisj ps)

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ qqDisj via qqDisjGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ qqDisj

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj.definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ qqDisj

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqDisj_semiformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n ps : V} : IsSemiformula L n (qqDisj ps) ↔ ∀ i < len ps, IsSemiformula L n (nth ps i)

Disjunction of sequential substution

disjSeqSubst w p k = subst (k ∷ w) p ^⋎ ⋯ ^⋎ subst (0 ∷ w) p ^⋎ ⊥

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.DisjSeqSubst.blueprint : PR.Blueprint 2

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.DisjSeqSubst.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : PR.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubst {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p k : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubst w p k = LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.DisjSeqSubst.construction.result ![w, p] k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubst_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p : V) : disjSeqSubst w p 0 = qqFalsum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubst_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p k : V) : disjSeqSubst w p (k + 1) = qqOr (subst ℒₒᵣ (adjoin (numeral k) w) p) (disjSeqSubst w p k)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubstGraph : 𝚺₁.Semisentence 4

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubst.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₃ disjSeqSubst via disjSeqSubstGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubst.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₃ disjSeqSubst

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.disjSeqSubst.definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₃ disjSeqSubst

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.disjSeqSubst {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n m w p : V} (hw : IsSemitermVec ℒₒᵣ n m w) (hp : IsSemiformula ℒₒᵣ (n + 1) p) (k : V) : IsSemiformula ℒₒᵣ m (Arithmetic.disjSeqSubst w p k)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substs_conj_disjSeqSubst {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {n m l v w p : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (hv : IsSemitermVec ℒₒᵣ m l v) (k : V) : subst ℒₒᵣ v (disjSeqSubst w p k) = disjSeqSubst (termSubstVec ℒₒᵣ n v w) p k

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.SubstItr.blueprint : PR.Blueprint 2

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.SubstItr.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : PR.Construction V blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p k : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr w p k = LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.SubstItr.construction.result ![w, p] k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p : V) : substItr w p 0 = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p k : V) : substItr w p (k + 1) = adjoin (subst ℒₒᵣ (adjoin (numeral k) w) p) (substItr w p k)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItrGraph : 𝚺₁.Semisentence 4

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₃ substItr via substItrGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₃ substItr

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr.definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₃ substItr

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.len_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p k : V) : len (substItr w p k) = k

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substItr_nth {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (w p k : V) {i : V} (hi : i < k) : nth (substItr w p k) i = subst ℒₒᵣ (adjoin (numeral (k - (i + 1))) w) p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.substItrConj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m n w p : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (k : V) : IsSemiformula ℒₒᵣ m (qqConj (Arithmetic.substItr w p k))

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.substItrDisj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m n w p : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) (k : V) : IsSemiformula ℒₒᵣ m (qqDisj (Arithmetic.substItr w p k))

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.neg_conj_substItr {V : Type u_1} [ORingStructure 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.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.neg_disj_substItr {V : Type u_1} [ORingStructure 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.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.shift_conj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m n w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) : shift ℒₒᵣ (qqConj (substItr w p k)) = qqConj (substItr (termShiftVec ℒₒᵣ n w) (shift ℒₒᵣ p) k)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.shift_disj_substItr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {m n w p k : V} (hp : IsSemiformula ℒₒᵣ (n + 1) p) (hw : IsSemitermVec ℒₒᵣ n m w) : shift ℒₒᵣ (qqDisj (substItr w p k)) = qqDisj (substItr (termShiftVec ℒₒᵣ n w) (shift ℒₒᵣ p) k)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substs_conj_substItr {V : Type u_1} [ORingStructure 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) : subst ℒₒᵣ v (qqConj (substItr w p k)) = qqConj (substItr (termSubstVec ℒₒᵣ n v w) p k)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substs_disj_substItr {V : Type u_1} [ORingStructure 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) : subst ℒₒᵣ v (qqDisj (substItr w p k)) = qqDisj (substItr (termSubstVec ℒₒᵣ n v w) p k)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.qqVerums {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqVerums k = LO.FirstOrder.Arithmetic.Bootstrapping.qqConj (LO.FirstOrder.Arithmetic.repeatVec LO.FirstOrder.Arithmetic.Bootstrapping.qqVerum k)

def LO.FirstOrder.Arithmetic.Bootstrapping.qqVerumsGraph : 𝚺₁.Semisentence 2

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.le_qqVerums {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : k ≤ qqVerums k

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqVerums.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ qqVerums via qqVerumsGraph

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqVerums.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₁ qqVerums

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqVerums.definable' {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {Γ : SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Function₁ qqVerums

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.qqVerums {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n : V} (k : V) : IsSemiformula L n (qqVerums k)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqVerums_zero {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : qqVerums 0 = qqVerum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqVerums_succ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k : V) : qqVerums (k + 1) = qqAnd qqVerum (qqVerums k)