Negation function

def LO.FirstOrder.Arithmetic.Bootstrapping.Negation.blueprint : UformulaRec1.Blueprint

Equations

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

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

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.neg {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.neg L p = LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result L LO.FirstOrder.Arithmetic.Bootstrapping.Negation.construction 0 p

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.negGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.neg.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ neg L via negGraph L

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

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : neg L (qqRel k R v) = qqNRel k R v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : neg L (qqNRel k R v) = qqRel k R v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : neg L qqVerum = qqFalsum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : neg L qqFalsum = qqVerum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : neg L (qqAnd p q) = qqOr (neg L p) (neg L q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : neg L (qqOr p q) = qqAnd (neg L p) (neg L q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsUFormula L p) : neg L (qqAll p) = qqExs (neg L p)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_ex {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsUFormula L p) : neg L (qqExs p) = qqAll (neg L p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_not_uformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {x : V} (h : ¬IsUFormula L x) : neg L x = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.neg {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → IsUFormula L (Bootstrapping.neg L p)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.bv_neg {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → bv L (Bootstrapping.neg L p) = bv L p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.neg_neg {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → Bootstrapping.neg L (Bootstrapping.neg L p) = p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.neg_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L (Bootstrapping.neg L p) ↔ IsUFormula L p

@[simp]

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

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

Alias of the reverse direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.neg_iff.

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

Alias of the forward direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.neg_iff.

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.neg_inj_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : neg L p = neg L q ↔ p = q

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.imp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p q : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.imp L p q = LO.FirstOrder.Arithmetic.Bootstrapping.qqOr (LO.FirstOrder.Arithmetic.Bootstrapping.neg L p) q

def LO.FirstOrder.Arithmetic.Bootstrapping.«term_^→[_]_» : Lean.TrailingParserDescr

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.impGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p q : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.iffGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.imp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} : IsUFormula L (Bootstrapping.imp L p q) ↔ IsUFormula L p ∧ IsUFormula L q

@[simp]

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.imp.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ imp L via impGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.imp.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ imp L

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} : IsUFormula L (Bootstrapping.iff L p q) ↔ IsUFormula L p ∧ IsUFormula L q

@[simp]

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_iff_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (p q : V) : p < iff L p q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_iff_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (p q : V) : q < iff L p q

instance LO.FirstOrder.Arithmetic.Bootstrapping.iff.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ iff L via iffGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.iff.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ iff L

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

Shift function

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Shift.blueprint (L : Language) [L.Encodable] [L.LORDefinable] : UformulaRec1.Blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Shift.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : UformulaRec1.Construction V (blueprint L)

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.shift L p = LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result L (LO.FirstOrder.Arithmetic.Bootstrapping.Shift.construction L) 0 p

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.shiftGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.shift.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ shift L via shiftGraph L

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

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : shift L (qqRel k R v) = qqRel k R (termShiftVec L k v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : shift L (qqNRel k R v) = qqNRel k R (termShiftVec L k v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : shift L qqVerum = qqVerum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : shift L qqFalsum = qqFalsum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : shift L (qqAnd p q) = qqAnd (shift L p) (shift L q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : shift L (qqOr p q) = qqOr (shift L p) (shift L q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsUFormula L p) : shift L (qqAll p) = qqAll (shift L p)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_exs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsUFormula L p) : shift L (qqExs p) = qqExs (shift L p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_not_uformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {x : V} (h : ¬IsUFormula L x) : shift L x = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → IsUFormula L (Bootstrapping.shift L p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.bv_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → bv L (Bootstrapping.shift L p) = bv L p

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.shift_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L (Bootstrapping.shift L p) ↔ IsUFormula L p

@[simp]

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

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

Substitution function

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Substs.blueprint (L : Language) [L.Encodable] [L.LORDefinable] : UformulaRec1.Blueprint

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.Substs.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : UformulaRec1.Construction V (blueprint L)

Equations

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

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.subst L w p = LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result L (LO.FirstOrder.Arithmetic.Bootstrapping.Substs.construction L) w p

@[irreducible]

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.substsGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.substsGraph L = LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Blueprint.result L (LO.FirstOrder.Arithmetic.Bootstrapping.Substs.blueprint L)

instance LO.FirstOrder.Arithmetic.Bootstrapping.subst.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ subst L via substsGraph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.subst.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ subst L

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : subst L w (qqRel k R v) = qqRel k R (termSubstVec L k w v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : subst L w (qqNRel k R v) = qqNRel k R (termSubstVec L k w v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (w : V) : subst L w qqVerum = qqVerum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (w : V) : subst L w qqFalsum = qqFalsum

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : subst L w (qqAnd p q) = qqAnd (subst L w p) (subst L w q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : subst L w (qqOr p q) = qqOr (subst L w p) (subst L w q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w p : V} (hp : IsUFormula L p) : subst L w (qqAll p) = qqAll (subst L (qVec L w) p)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_ex {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w p : V} (hp : IsUFormula L p) : subst L w (qqExs p) = qqExs (subst L (qVec L w) p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.isUFormula_subst_ISigma1.sigma1_succ_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {P : V → V → V → Prop} (hP : 𝚺₁-Relation₃ P) (hRel : ∀ (w k R v : V), L.IsRel k R → IsUTermVec L k v → P w (qqRel k R v) (qqRel k R (termSubstVec L k w v))) (hNRel : ∀ (w k R v : V), L.IsRel k R → IsUTermVec L k v → P w (qqNRel k R v) (qqNRel k R (termSubstVec L k w v))) (hverum : ∀ (w : V), P w qqVerum qqVerum) (hfalsum : ∀ (w : V), P w qqFalsum qqFalsum) (hand : ∀ (w p q : V), IsUFormula L p → IsUFormula L q → P w p (subst L w p) → P w q (subst L w q) → P w (qqAnd p q) (qqAnd (subst L w p) (subst L w q))) (hor : ∀ (w p q : V), IsUFormula L p → IsUFormula L q → P w p (subst L w p) → P w q (subst L w q) → P w (qqOr p q) (qqOr (subst L w p) (subst L w q))) (hall : ∀ (w p : V), IsUFormula L p → P (qVec L w) p (subst L (qVec L w) p) → P w (qqAll p) (qqAll (subst L (qVec L w) p))) (hexs : ∀ (w p : V), IsUFormula L p → P (qVec L w) p (subst L (qVec L w) p) → P w (qqExs p) (qqExs (subst L (qVec L w) p))) {w p : V} : IsUFormula L p → P w p (subst L w p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.semiformula_subst_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {P : V → V → V → V → Prop} (hP : 𝚺₁-Relation₄ P) (hRel : ∀ (n w k R v : V), L.IsRel k R → IsSemitermVec L k n v → P n w (qqRel k R v) (qqRel k R (termSubstVec L k w v))) (hNRel : ∀ (n w k R v : V), L.IsRel k R → IsSemitermVec L k n v → P n w (qqNRel k R v) (qqNRel k R (termSubstVec L k w v))) (hverum : ∀ (n w : V), P n w qqVerum qqVerum) (hfalsum : ∀ (n w : V), P n w qqFalsum qqFalsum) (hand : ∀ (n w p q : V), IsSemiformula L n p → IsSemiformula L n q → P n w p (subst L w p) → P n w q (subst L w q) → P n w (qqAnd p q) (qqAnd (subst L w p) (subst L w q))) (hor : ∀ (n w p q : V), IsSemiformula L n p → IsSemiformula L n q → P n w p (subst L w p) → P n w q (subst L w q) → P n w (qqOr p q) (qqOr (subst L w p) (subst L w q))) (hall : ∀ (n w p : V), IsSemiformula L (n + 1) p → P (n + 1) (qVec L w) p (subst L (qVec L w) p) → P n w (qqAll p) (qqAll (subst L (qVec L w) p))) (hexs : ∀ (n w p : V), IsSemiformula L (n + 1) p → P (n + 1) (qVec L w) p (subst L (qVec L w) p) → P n w (qqExs p) (qqExs (subst L (qVec L w) p))) {n p w : V} : IsSemiformula L n p → P n w p (subst L w p)

@[simp]

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_not_uformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {w x : V} (h : ¬IsUFormula L x) : subst L w x = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_neg {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {m w n p : V} (hp : IsSemiformula L n p) : IsSemitermVec L n m w → subst L w (neg L p) = neg L (subst L w p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.shift_substs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {m w n p : V} (hp : IsSemiformula L n p) : IsSemitermVec L n m w → shift L (subst L w p) = subst L (termShiftVec L n w) (shift L p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.substs_substs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {m w l n v p : V} (hp : IsSemiformula L l p) : IsSemitermVec L n m w → IsSemitermVec L l n v → subst L w (subst L v p) = subst L (termSubstVec L l w v) p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.subst_eq_self {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p n w : V} (hp : IsSemiformula L n p) (hw : IsSemitermVec L n n w) (H : ∀ i < n, nth w i = qqBvar i) : subst L w p = p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.subst_eq_self₁ {L : Language} [L.Encodable] [L.LORDefinable] {p : ℕ} (hp : IsSemiformula L 1 p) : subst L ?[qqBvar 0] p = p

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.substs1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (t u : V) : V

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.substs1 L t u = LO.FirstOrder.Arithmetic.Bootstrapping.subst L ?[t] u

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.substs1Graph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.substs1.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ substs1 L via substs1Graph L

instance LO.FirstOrder.Arithmetic.Bootstrapping.substs1.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₂ substs1 L

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.substs1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n t p : V} (ht : IsSemiterm L n t) (hp : IsSemiformula L 1 p) : IsSemiformula L n (Bootstrapping.substs1 L t p)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.free {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.freeGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

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

free function

instance LO.FirstOrder.Arithmetic.Bootstrapping.free.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ free L via freeGraph L

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

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.free {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsSemiformula L 1 p) : IsFormula L (Bootstrapping.free L p)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.free1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.free1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsSemiformula L 2 p) : IsSemiformula L 1 (Bootstrapping.free1 L p)

Complexity of formula

def LO.FirstOrder.Arithmetic.Bootstrapping.FormulaComplexity.blueprint : UformulaRec1.Blueprint

Equations

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

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

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexityGraph (L : Language) [L.Encodable] [L.LORDefinable] : 𝚺₁.Semisentence 2

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ formulaComplexity L via formulaComplexityGraph L

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

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : formulaComplexity L (qqRel k R v) = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : formulaComplexity L (qqNRel k R v) = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : formulaComplexity L qqVerum = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : formulaComplexity L qqFalsum = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : formulaComplexity L (qqAnd p q) = formulaComplexity L p ⊔ formulaComplexity L q + 1

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : formulaComplexity L (qqOr p q) = formulaComplexity L p ⊔ formulaComplexity L q + 1

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsUFormula L p) : formulaComplexity L (qqAll p) = formulaComplexity L p + 1

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_ex {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsUFormula L p) : formulaComplexity L (qqExs p) = formulaComplexity L p + 1

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_not_uformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {x : V} (h : ¬IsUFormula L x) : formulaComplexity L x = 0

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_neg {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → formulaComplexity L (neg L p) = formulaComplexity L p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_shift {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → formulaComplexity L (shift L p) = formulaComplexity L p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fomulaComplexity_substs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n m w p : V} (hp : IsSemiformula L n p) : IsSemitermVec L n m w → formulaComplexity L (subst L w p) = formulaComplexity L p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fomulaComplexity_substs1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {m t p : V} (hp : IsSemiformula L 1 p) (ht : IsSemiterm L m t) : formulaComplexity L (substs1 L t p) = formulaComplexity L p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fomulaComplexity_free {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsSemiformula L 1 p) : formulaComplexity L (free L p) = formulaComplexity L p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.fomulaComplexity_free1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} (hp : IsSemiformula L 2 p) : formulaComplexity L (free1 L p) = formulaComplexity L p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_max_succ_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : a < a ⊔ b + 1

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_max_succ_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (a b : V) : b < a ⊔ b + 1

A structural induction correspondence to LO.FirstOrder.Semiformula.formulaRec.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormula.sigma1_structural_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {P : V → Prop} (hP : 𝚺₁-Predicate P) (hrel : ∀ (k r v : V), L.IsRel k r → IsTermVec L k v → P (qqRel k r v)) (hnrel : ∀ (k r v : V), L.IsRel k r → IsTermVec L k v → P (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), IsFormula L p → IsFormula L q → P p → P q → P (qqAnd p q)) (hor : ∀ (p q : V), IsFormula L p → IsFormula L q → P p → P q → P (qqOr p q)) (hall : ∀ (p : V), IsSemiformula L 1 p → P (free L p) → P (qqAll p)) (hexs : ∀ (p : V), IsSemiformula L 1 p → P (free L p) → P (qqExs p)) {p : V} : IsFormula L p → P p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormula.sigma1_structural_induction₂ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {P : V → Prop} (hP : 𝚺₁-Predicate P) (hrel : ∀ (k r v : V), L.IsRel k r → IsSemitermVec L k 1 v → P (qqRel k r v)) (hnrel : ∀ (k r v : V), L.IsRel k r → IsSemitermVec L k 1 v → P (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), IsSemiformula L 1 p → IsSemiformula L 1 q → P p → P q → P (qqAnd p q)) (hor : ∀ (p q : V), IsSemiformula L 1 p → IsSemiformula L 1 q → P p → P q → P (qqOr p q)) (hall : ∀ (p : V), IsSemiformula L 2 p → P (free1 L p) → P (qqAll p)) (hexs : ∀ (p : V), IsSemiformula L 2 p → P (free1 L p) → P (qqExs p)) {p : V} : IsSemiformula L 1 p → P p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsFormula.sigma1_structural_induction₂_ss {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {P : V → Prop} (hP : 𝚺₁-Predicate P) (hrel : ∀ (k r v : V), L.IsRel k r → IsSemitermVec L k 1 v → P (qqRel k r v)) (hnrel : ∀ (k r v : V), L.IsRel k r → IsSemitermVec L k 1 v → P (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), IsSemiformula L 1 p → IsSemiformula L 1 q → P p → P q → P (qqAnd p q)) (hor : ∀ (p q : V), IsSemiformula L 1 p → IsSemiformula L 1 q → P p → P q → P (qqOr p q)) (hall : ∀ (p : V), IsSemiformula L 2 p → P (free1 L (shift L (shift L p))) → P (qqAll p)) (hexs : ∀ (p : V), IsSemiformula L 2 p → P (free1 L (shift L (shift L p))) → P (qqExs p)) {p : V} : IsSemiformula L 1 p → P p

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

Equations

• x ^= y = LO.FirstOrder.Arithmetic.Bootstrapping.qqRel 2 ↑LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eqIndex ?[x, y]

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

Equations

• x ^≠ y = LO.FirstOrder.Arithmetic.Bootstrapping.qqNRel 2 ↑LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.eqIndex ?[x, y]

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

Equations

• x ^< y = LO.FirstOrder.Arithmetic.Bootstrapping.qqRel 2 ↑LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ltIndex ?[x, y]

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

Equations

• x ^≮ y = LO.FirstOrder.Arithmetic.Bootstrapping.qqNRel 2 ↑LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.ltIndex ?[x, y]

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term_^=_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term_^≠_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term_^<_» : Lean.TrailingParserDescr

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.«term_^≮_» : Lean.TrailingParserDescr

Equations

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqEQ_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : x < x ^= y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqEQ_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : y < x ^= y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqLT_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : x < x ^< y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqLT_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : y < x ^< y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqNEQ_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : x < x ^≠ y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqNEQ_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : y < x ^≠ y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqNLT_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : x < x ^≮ y

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.lt_qqNLT_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (x y : V) : y < x ^≮ y

def LO.FirstOrder.Arithmetic.qqEQDef : 𝚺₁.Semisentence 3

Equations

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

def LO.FirstOrder.Arithmetic.qqNEQDef : 𝚺₁.Semisentence 3

Equations

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

def LO.FirstOrder.Arithmetic.qqLTDef : 𝚺₁.Semisentence 3

Equations

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

def LO.FirstOrder.Arithmetic.qqNLTDef : 𝚺₁.Semisentence 3

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqEQ_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ qqEQ via qqEQDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqNEQ_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ qqNEQ via qqNEQDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqLT_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ qqLT via qqLTDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.qqNLT_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₁-Function₂ qqNLT via qqNLTDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instDefinableFunction₂MkHAddNatOfNatQqEQ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ qqEQ

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instDefinableFunction₂MkHAddNatOfNatQqNEQ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ qqNEQ

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instDefinableFunction₂MkHAddNatOfNatQqLT {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ qqLT

instance LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.instDefinableFunction₂MkHAddNatOfNatQqNLT {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (Γ : SigmaPiDelta) (m : ℕ) : { Γ := Γ, rank := m + 1 }-Function₂ qqNLT

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.neg_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {t u : V} (ht : IsUTerm ℒₒᵣ t) (hu : IsUTerm ℒₒᵣ u) : neg ℒₒᵣ (t ^= u) = t ^≠ u

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.neg_neq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {t u : V} (ht : IsUTerm ℒₒᵣ t) (hu : IsUTerm ℒₒᵣ u) : neg ℒₒᵣ (t ^≠ u) = t ^= u

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.neg_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {t u : V} (ht : IsUTerm ℒₒᵣ t) (hu : IsUTerm ℒₒᵣ u) : neg ℒₒᵣ (t ^< u) = t ^≮ u

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.neg_nlt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {t u : V} (ht : IsUTerm ℒₒᵣ t) (hu : IsUTerm ℒₒᵣ u) : neg ℒₒᵣ (t ^≮ u) = t ^< u

theorem LO.FirstOrder.Arithmetic.Bootstrapping.Arithmetic.substs_eq {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {w t u : V} (ht : IsUTerm ℒₒᵣ t) (hu : IsUTerm ℒₒᵣ u) : subst ℒₒᵣ w (t ^= u) = termSubst ℒₒᵣ w t ^= termSubst ℒₒᵣ w u