Supporting results for pointwise provable equality.

Negation function

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Negation.blueprint : UformulaRec1.Blueprint

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.Negation.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Negation.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : UformulaRec1.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.Negation.

Equations

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

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

The neg construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.negGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 2

The neg Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.neg.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₁ neg L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.neg_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : neg L qqVerum = qqFalsum

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.neg_iff.

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.neg_iff.

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.imp {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (p q : V) : V

The imp construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

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

The «term ^→[ ] » construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.impGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 3

The imp Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

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

The iff construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.iffGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 3

The iff Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.imp.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₂ imp L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.iff.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₂ iff L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Shift.blueprint (L : Language) [L.Encodable] [L.LORDefinable] : UformulaRec1.Blueprint

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.Shift.

Equations

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

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

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.Shift.

Equations

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

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

The shift construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.shiftGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 2

The shift Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.shift.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₁ shift L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.shift_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : shift L qqVerum = qqVerum

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.Substs.blueprint (L : Language) [L.Encodable] [L.LORDefinable] : UformulaRec1.Blueprint

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.Substs.

Equations

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

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

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.Substs.

Equations

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

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

The subst construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

@[irreducible]

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.substsGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 3

The substs Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.subst.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₂ subst L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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)

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.substs1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (t u : V) : V

The substs1 construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.substs1Graph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 3

The substs1Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.substs1.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₂ substs1 L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.free {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

The free construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.freeGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 2

The free Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

free function

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.free.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₁ free L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.free1 {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

The free1 construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.FormulaComplexity.blueprint : UformulaRec1.Blueprint

The blueprint construction in FFL.FirstOrder.Arithmetic.Bootstrapping.FormulaComplexity.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.FormulaComplexity.construction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : UformulaRec1.Construction V blueprint

The construction construction in FFL.FirstOrder.Arithmetic.Bootstrapping.FormulaComplexity.

Equations

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

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

The formula Complexity construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.formulaComplexityGraph (L : Language) [L.Encodable] [L.LORDefinable] : Σ₁.Semisentence 2

The formula Complexity Graph construction in FFL.FirstOrder.Arithmetic.Bootstrapping.

Equations

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

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity.definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : Σ₁-Function₁ formulaComplexity L

instance PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.formulaComplexity_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] : formulaComplexity L qqVerum = 0

@[simp]

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

@[simp]

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.lt_max_succ_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (a b : V) : a < a ⊔ b + 1

@[simp]

theorem PointwiseComposition.FFL.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 FFL.FirstOrder.Semiformula.formulaRec.

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.sigma1_structural_induction_of_opening {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] {L : Language} [L.Encodable] [L.LORDefinable] (n : V) (opening : V → V) (hOpening : Σ₁-Function₁ opening) (hClosed : ∀ {p : V}, IsSemiformula L (n + 1) p → IsSemiformula L n (opening p)) (hComplexity : ∀ {p : V}, IsSemiformula L (n + 1) p → formulaComplexity L (opening p) = formulaComplexity L p) {P : V → Prop} (hP : Σ₁-Predicate P) (hrel : ∀ (k r v : V), L.IsRel k r → IsSemitermVec L k n v → P (qqRel k r v)) (hnrel : ∀ (k r v : V), L.IsRel k r → IsSemitermVec L k n v → P (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), IsSemiformula L n p → IsSemiformula L n q → P p → P q → P (qqAnd p q)) (hor : ∀ (p q : V), IsSemiformula L n p → IsSemiformula L n q → P p → P q → P (qqOr p q)) (hall : ∀ (p : V), IsSemiformula L (n + 1) p → P (opening p) → P (qqAll p)) (hexs : ∀ (p : V), IsSemiformula L (n + 1) p → P (opening p) → P (qqExs p)) {p : V} : IsSemiformula L n p → P p

Structural induction at any variable bound, using a Sigma-one definable opening that lowers that bound by one and preserves formula complexity.

theorem PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.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 PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqEQ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : V

The qq EQ construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqNEQ {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : V

The qq NEQ construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqLT {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : V

The qq LT construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

noncomputable def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqNLT {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : V

The qq NLT construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term_^=_» : Lean.TrailingParserDescr

The «term ^= » construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term_^≠_» : Lean.TrailingParserDescr

The «term ^≠ » construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term_^<_» : Lean.TrailingParserDescr

The «term ^< » construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.«term_^≮_» : Lean.TrailingParserDescr

The «term ^≮ » construction in FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.

Equations

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

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqEQ_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : x < x ^= y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqEQ_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : y < x ^= y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqLT_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : x < x ^< y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqLT_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : y < x ^< y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqNEQ_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : x < x ^≠ y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqNEQ_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : y < x ^≠ y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqNLT_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : x < x ^≮ y

@[simp]

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.lt_qqNLT_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] (x y : V) : y < x ^≮ y

def PointwiseComposition.FFL.FirstOrder.Arithmetic.qqEQDef : Σ₁.Semisentence 3

The qq EQDef construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.qqNEQDef : Σ₁.Semisentence 3

The qq NEQDef construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.qqLTDef : Σ₁.Semisentence 3

The qq LTDef construction in FFL.FirstOrder.Arithmetic.

Equations

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

def PointwiseComposition.FFL.FirstOrder.Arithmetic.qqNLTDef : Σ₁.Semisentence 3

The qq NLTDef construction in FFL.FirstOrder.Arithmetic.

Equations

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

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqEQ_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ qqEQ via qqEQDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqNEQ_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ qqNEQ via qqNEQDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqLT_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ qqLT via qqLTDef

instance PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.qqNLT_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝐈Σ₁] : Σ₁-Function₂ qqNLT via qqNLTDef

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

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

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

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

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

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

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

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

theorem PointwiseComposition.FFL.FirstOrder.Arithmetic.Bootstrapping.ObjectArithmetic.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