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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqRel k r v = ⟪0, ⟪k, ⟪r, v⟫⟫⟫ + 1

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqNRel k r v = ⟪1, ⟪k, ⟪r, v⟫⟫⟫ + 1

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqVerum = ⟪2, 0⟫ + 1

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqFalsum = ⟪3, 0⟫ + 1

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqAnd p q = ⟪4, ⟪p, q⟫⟫ + 1

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqOr p q = ⟪5, ⟪p, q⟫⟫ + 1

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqAll p = ⟪6, p⟫ + 1

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.qqExs p = ⟪7, p⟫ + 1

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

Equations

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

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

Equations

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

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.«term^⊤» = Lean.ParserDescr.node `LO.FirstOrder.Arithmetic.Bootstrapping.«term^⊤» 1024 (Lean.ParserDescr.symbol "^⊤")

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.«term^⊥» = Lean.ParserDescr.node `LO.FirstOrder.Arithmetic.Bootstrapping.«term^⊥» 1024 (Lean.ParserDescr.symbol "^⊥")

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def LO.FirstOrder.Arithmetic.qqRelDef : 𝚺₀.Semisentence 4

Equations

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

def LO.FirstOrder.Arithmetic.qqNRelDef : 𝚺₀.Semisentence 4

Equations

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

def LO.FirstOrder.Arithmetic.qqVerumDef : 𝚺₀.Semisentence 1

Equations

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

def LO.FirstOrder.Arithmetic.qqFalsumDef : 𝚺₀.Semisentence 1

Equations

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

def LO.FirstOrder.Arithmetic.qqAndDef : 𝚺₀.Semisentence 3

Equations

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

def LO.FirstOrder.Arithmetic.qqOrDef : 𝚺₀.Semisentence 3

Equations

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

def LO.FirstOrder.Arithmetic.qqAllDef : 𝚺₀.Semisentence 2

Equations

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

def LO.FirstOrder.Arithmetic.qqExsDef : 𝚺₀.Semisentence 2

Equations

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

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

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqVerum_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₀ qqVerum via qqVerumDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqFalsum_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₀ qqFalsum via qqFalsumDef

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

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqForall_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ qqAll via qqAllDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.qqExsists_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] : 𝚺₀-Function₁ qqExs via qqExsDef

instance LO.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₃QqRel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₃ qqRel

instance LO.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₃QqNRel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₃ qqNRel

instance LO.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₂QqAnd {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₂ qqAnd

instance LO.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₂QqOr {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₂ qqOr

instance LO.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₁QqAll {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₁ qqAll

instance LO.FirstOrder.Arithmetic.Bootstrapping.instDefinableFunction₁QqExs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (ℌ : HierarchySymbol) : ℌ-Function₁ qqExs

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqRel_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k₁ r₁ v₁ k₂ r₂ v₂ : V) : qqRel k₁ r₁ v₁ = qqRel k₂ r₂ v₂ ↔ k₁ = k₂ ∧ r₁ = r₂ ∧ v₁ = v₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqNRel_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k₁ r₁ v₁ k₂ r₂ v₂ : V) : qqNRel k₁ r₁ v₁ = qqNRel k₂ r₂ v₂ ↔ k₁ = k₂ ∧ r₁ = r₂ ∧ v₁ = v₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqAnd_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p₁ q₁ p₂ q₂ : V) : qqAnd p₁ q₁ = qqAnd p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqOr_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p₁ q₁ p₂ q₂ : V) : qqOr p₁ q₁ = qqOr p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqAll_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p₁ p₂ : V) : qqAll p₁ = qqAll p₂ ↔ p₁ = p₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.qqExs_inj {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p₁ p₂ : V) : qqExs p₁ = qqExs p₂ ↔ p₁ = p₂

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.arity_lt_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k r v : V) : k < qqRel k r v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.r_lt_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k r v : V) : r < qqRel k r v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.v_lt_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k r v : V) : v < qqRel k r v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.arity_lt_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k r v : V) : k < qqNRel k r v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.r_lt_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k r v : V) : r < qqNRel k r v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.v_lt_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (k r v : V) : v < qqNRel k r v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_lt_qqRel_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i k r v : V} (hi : i < len v) : nth v i < qqRel k r v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.nth_lt_qqNRel_of_lt {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {i k r v : V} (hi : i < len v) : nth v i < qqNRel k r v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_K!_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p q : V) : p < qqAnd p q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_K!_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p q : V) : q < qqAnd p q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_or_left {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p q : V) : p < qqOr p q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_or_right {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p q : V) : q < qqOr p q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_forall {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : p < qqAll p

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.lt_exists {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (p : V) : p < qqExs p

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

Equations

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

def LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedFormula.formulaAux : 𝚺₀.Semisentence 2

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedFormula.blueprint (L : Language) [L.Encodable] [L.LORDefinable] : Fixpoint.Blueprint 0

Equations

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

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

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedFormula.instStrongFiniteConstruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] : Fixpoint.Construction.StrongFinite V (construction L)

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula L = (LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedFormula.construction L).Fixpoint ![]

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.isUFormula (L : Language) [L.Encodable] [L.LORDefinable] : 𝚫₁.Semisentence 1

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.isUFormula L = (LO.FirstOrder.Arithmetic.Bootstrapping.FormalizedFormula.blueprint L).fixpointDefΔ₁

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

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

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.case_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p ↔ (∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsUTermVec L k v ∧ p = qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsUTermVec L k v ∧ p = qqNRel k R v) ∨ p = qqVerum ∨ p = qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), IsUFormula L p₁ ∧ IsUFormula L p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), IsUFormula L p₁ ∧ IsUFormula L p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), IsUFormula L p₁ ∧ p = qqAll p₁) ∨ ∃ (p₁ : V), IsUFormula L p₁ ∧ p = qqExs p₁

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.case {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : IsUFormula L p → (∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsUTermVec L k v ∧ p = qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsUTermVec L k v ∧ p = qqNRel k R v) ∨ p = qqVerum ∨ p = qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), IsUFormula L p₁ ∧ IsUFormula L p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), IsUFormula L p₁ ∧ IsUFormula L p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), IsUFormula L p₁ ∧ p = qqAll p₁) ∨ ∃ (p₁ : V), IsUFormula L p₁ ∧ p = qqExs p₁

Alias of the forward direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.case_iff.

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.mk {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {p : V} : ((∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsUTermVec L k v ∧ p = qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsUTermVec L k v ∧ p = qqNRel k R v) ∨ p = qqVerum ∨ p = qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), IsUFormula L p₁ ∧ IsUFormula L p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), IsUFormula L p₁ ∧ IsUFormula L p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), IsUFormula L p₁ ∧ p = qqAll p₁) ∨ ∃ (p₁ : V), IsUFormula L p₁ ∧ p = qqExs p₁) → IsUFormula L p

Alias of the reverse direction of LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.case_iff.

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k r v : V} : IsUFormula L (qqRel k r v) ↔ L.IsRel k r ∧ IsUTermVec L k v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {k r v : V} : IsUFormula L (qqNRel k r v) ↔ L.IsRel k r ∧ IsUTermVec L k v

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

@[simp]

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

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.ISigma1.sigma1_succ_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 → IsUTermVec L k v → P (qqRel k r v)) (hnrel : ∀ (k r v : V), L.IsRel k r → IsUTermVec L k v → P (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), IsUFormula L p → IsUFormula L q → P p → P q → P (qqAnd p q)) (hor : ∀ (p q : V), IsUFormula L p → IsUFormula L q → P p → P q → P (qqOr p q)) (hall : ∀ (p : V), IsUFormula L p → P p → P (qqAll p)) (hexs : ∀ (p : V), IsUFormula L p → P p → P (qqExs p)) (p : V) : IsUFormula L p → P p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsUFormula.ISigma1.pi1_succ_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 → IsUTermVec L k v → P (qqRel k r v)) (hnrel : ∀ (k r v : V), L.IsRel k r → IsUTermVec L k v → P (qqNRel k r v)) (hverum : P qqVerum) (hfalsum : P qqFalsum) (hand : ∀ (p q : V), IsUFormula L p → IsUFormula L q → P p → P q → P (qqAnd p q)) (hor : ∀ (p q : V), IsUFormula L p → IsUFormula L q → P p → P q → P (qqOr p q)) (hall : ∀ (p : V), IsUFormula L p → P p → P (qqAll p)) (hexs : ∀ (p : V), IsUFormula L p → P p → P (qqExs p)) (p : V) : IsUFormula L p → P p

structure LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Blueprint : Type

• rel : 𝚺₁.Semisentence 5
• nrel : 𝚺₁.Semisentence 5
• verum : 𝚺₁.Semisentence 2
• falsum : 𝚺₁.Semisentence 2
• and : 𝚺₁.Semisentence 6
• or : 𝚺₁.Semisentence 6
• all : 𝚺₁.Semisentence 4
• exs : 𝚺₁.Semisentence 4
• allChanges : 𝚺₁.Semisentence 2
• exsChanges : 𝚺₁.Semisentence 2

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

Equations

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

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

Note: noncomputable attribute to prohibit compilation of a large term. This is necessary for Zoo and integration with Verso.

Equations

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

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

Note: noncomputable attribute to prohibit compilation of a large term. This is necessary for Zoo and integration with Verso.

Equations

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

structure LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction (V : Type u_1) [ORingStructure V] (φ : Blueprint) : Type u_1

• rel (param k R v : V) : V
• nrel (param k R v : V) : V
• verum (param : V) : V
• falsum (param : V) : V
• and (param p₁ p₂ y₁ y₂ : V) : V
• or (param p₁ p₂ y₁ y₂ : V) : V
• all (param p₁ y₁ : V) : V
• exs (param p₁ y₁ : V) : V
• allChanges (param : V) : V
• exsChanges (param : V) : V
• rel_defined : 𝚺₁-Function₄ self.rel via φ.rel
• nrel_defined : 𝚺₁-Function₄ self.nrel via φ.nrel
• verum_defined : 𝚺₁-Function₁ self.verum via φ.verum
• falsum_defined : 𝚺₁-Function₁ self.falsum via φ.falsum
• and_defined : 𝚺₁-Function₅ self.and via φ.and
• or_defined : 𝚺₁-Function₅ self.or via φ.or
• all_defined : 𝚺₁-Function₃ self.all via φ.all
• exs_defined : 𝚺₁-Function₃ self.exs via φ.exs
• allChanges_defined : 𝚺₁-Function₁ self.allChanges via φ.allChanges
• exChanges_defined : 𝚺₁-Function₁ self.exsChanges via φ.exsChanges

def LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.Phi {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) (C : Set V) (pr : V) : Prop

Equations

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

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

Equations

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

instance LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.instFiniteConstruction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) : Fixpoint.Construction.Finite V (construction L c)

def LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.Graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) (param x y : V) : Prop

Equations

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.Graph.case_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} {c : Construction V β} {param p y : V} : Graph L c param p y ↔ IsUFormula L p ∧ ((∃ (k : V) (R : V) (v : V), p = qqRel k R v ∧ y = c.rel param k R v) ∨ (∃ (k : V) (R : V) (v : V), p = qqNRel k R v ∧ y = c.nrel param k R v) ∨ p = qqVerum ∧ y = c.verum param ∨ p = qqFalsum ∧ y = c.falsum param ∨ (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V), Graph L c param p₁ y₁ ∧ Graph L c param p₂ y₂ ∧ p = qqAnd p₁ p₂ ∧ y = c.and param p₁ p₂ y₁ y₂) ∨ (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V), Graph L c param p₁ y₁ ∧ Graph L c param p₂ y₂ ∧ p = qqOr p₁ p₂ ∧ y = c.or param p₁ p₂ y₁ y₂) ∨ (∃ (p₁ : V) (y₁ : V), Graph L c (c.allChanges param) p₁ y₁ ∧ p = qqAll p₁ ∧ y = c.all param p₁ y₁) ∨ ∃ (p₁ : V) (y₁ : V), Graph L c (c.exsChanges param) p₁ y₁ ∧ p = qqExs p₁ ∧ y = c.exs param p₁ y₁)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (β : Blueprint) (c : Construction V β) : 𝚺₁-Relation₃ Graph L c via Blueprint.graph L β

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.eval_graphDef {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (β : Blueprint) (c : Construction V β) (v : Fin 3 → V) : (Semiformula.Evalb v) ↑(Blueprint.graph L β) ↔ Graph L c (v 0) (v 1) (v 2)

instance LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] (β : Blueprint) (c : Construction V β) : { Γ := 𝚺, rank := 0 + 1 }-Relation₃ Graph L c

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_dom_uformula {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p r : V} : Graph L c param p r → IsUFormula L p

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_rel_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param k r v y : V} (hkr : L.IsRel k r) (hv : IsUTermVec L k v) : Graph L c param (qqRel k r v) y ↔ y = c.rel param k r v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_nrel_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param k r v y : V} (hkr : L.IsRel k r) (hv : IsUTermVec L k v) : Graph L c param (qqNRel k r v) y ↔ y = c.nrel param k r v

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_verum_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param y : V} : Graph L c param qqVerum y ↔ y = c.verum param

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_falsum_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param y : V} : Graph L c param qqFalsum y ↔ y = c.falsum param

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param k r v : V} (hkr : L.IsRel k r) (hv : IsUTermVec L k v) : Graph L c param (qqRel k r v) (c.rel param k r v)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param k r v : V} (hkr : L.IsRel k r) (hv : IsUTermVec L k v) : Graph L c param (qqNRel k r v) (c.nrel param k r v)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param : V} : Graph L c param qqVerum (c.verum param)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param : V} : Graph L c param qqFalsum (c.falsum param)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ p₂ r₁ r₂ : V} (hp₁ : IsUFormula L p₁) (hp₂ : IsUFormula L p₂) (h₁ : Graph L c param p₁ r₁) (h₂ : Graph L c param p₂ r₂) : Graph L c param (qqAnd p₁ p₂) (c.and param p₁ p₂ r₁ r₂)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_and_inv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ p₂ r : V} : Graph L c param (qqAnd p₁ p₂) r → ∃ (r₁ : V) (r₂ : V), Graph L c param p₁ r₁ ∧ Graph L c param p₂ r₂ ∧ r = c.and param p₁ p₂ r₁ r₂

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ p₂ r₁ r₂ : V} (hp₁ : IsUFormula L p₁) (hp₂ : IsUFormula L p₂) (h₁ : Graph L c param p₁ r₁) (h₂ : Graph L c param p₂ r₂) : Graph L c param (qqOr p₁ p₂) (c.or param p₁ p₂ r₁ r₂)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_or_inv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ p₂ r : V} : Graph L c param (qqOr p₁ p₂) r → ∃ (r₁ : V) (r₂ : V), Graph L c param p₁ r₁ ∧ Graph L c param p₂ r₂ ∧ r = c.or param p₁ p₂ r₁ r₂

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ r₁ : V} (hp₁ : IsUFormula L p₁) (h₁ : Graph L c (c.allChanges param) p₁ r₁) : Graph L c param (qqAll p₁) (c.all param p₁ r₁)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_all_inv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ r : V} : Graph L c param (qqAll p₁) r → ∃ (r₁ : V), Graph L c (c.allChanges param) p₁ r₁ ∧ r = c.all param p₁ r₁

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_ex {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ r₁ : V} (hp₁ : IsUFormula L p₁) (h₁ : Graph L c (c.exsChanges param) p₁ r₁) : Graph L c param (qqExs p₁) (c.exs param p₁ r₁)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_ex_inv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p₁ r : V} : Graph L c param (qqExs p₁) r → ∃ (r₁ : V), Graph L c (c.exsChanges param) p₁ r₁ ∧ r = c.exs param p₁ r₁

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_exists {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) (param : V) {p : V} : IsUFormula L p → ∃ (y : V), Graph L c param p y

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.graph_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {p : V} : IsUFormula L p → ∀ {param r r' : V}, Graph L c param p r → Graph L c param p r' → r = r'

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.exists_unique {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) (param : V) {p : V} (hp : IsUFormula L p) : ∃! r : V, Graph L c param p r

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.exists_unique_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) (param p : V) : ∃! r : V, (IsUFormula L p → Graph L c param p r) ∧ (¬IsUFormula L p → r = 0)

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result L c param p = Classical.choose! ⋯

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_prop {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) (param : V) {p : V} (hp : IsUFormula L p) : Graph L c param p (result L c param p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_prop_not {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) (param : V) {p : V} (hp : ¬IsUFormula L p) : result L c param p = 0

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_eq_of_graph {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p r : V} (h : Graph L c param p r) : result L c param p = r

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : result L c param (qqRel k R v) = c.rel param k R v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param k R v : V} (hR : L.IsRel k R) (hv : IsUTermVec L k v) : result L c param (qqNRel k R v) = c.nrel param k R v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_verum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param : V} : result L c param qqVerum = c.verum param

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_falsum {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param : V} : result L c param qqFalsum = c.falsum param

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_and {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : result L c param (qqAnd p q) = c.and param p q (result L c param p) (result L c param q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_or {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p q : V} (hp : IsUFormula L p) (hq : IsUFormula L q) : result L c param (qqOr p q) = c.or param p q (result L c param p) (result L c param q)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_all {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p : V} (hp : IsUFormula L p) : result L c param (qqAll p) = c.all param p (result L c (c.allChanges param) p)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_exs {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {param p : V} (hp : IsUFormula L p) : result L c param (qqExs p) = c.exs param p (result L c (c.exsChanges param) p)

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) : 𝚺₁-Function₂ result L c via Blueprint.result L β

instance LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.result_definable {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) : { Γ := 𝚺, rank := 0 + 1 }-Function₂ result L c

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.uformula_result_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} (c : Construction V β) {P : V → V → V → Prop} (hP : 𝚺₁-Relation₃ P) (hRel : ∀ (param k R v : V), L.IsRel k R → IsUTermVec L k v → P param (qqRel k R v) (c.rel param k R v)) (hNRel : ∀ (param k R v : V), L.IsRel k R → IsUTermVec L k v → P param (qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (param : V), P param qqVerum (c.verum param)) (hfalsum : ∀ (param : V), P param qqFalsum (c.falsum param)) (hand : ∀ (param p q : V), IsUFormula L p → IsUFormula L q → P param p (result L c param p) → P param q (result L c param q) → P param (qqAnd p q) (c.and param p q (result L c param p) (result L c param q))) (hor : ∀ (param p q : V), IsUFormula L p → IsUFormula L q → P param p (result L c param p) → P param q (result L c param q) → P param (qqOr p q) (c.or param p q (result L c param p) (result L c param q))) (hall : ∀ (param p : V), IsUFormula L p → P (c.allChanges param) p (result L c (c.allChanges param) p) → P param (qqAll p) (c.all param p (result L c (c.allChanges param) p))) (hexs : ∀ (param p : V), IsUFormula L p → P (c.exsChanges param) p (result L c (c.exsChanges param) p) → P param (qqExs p) (c.exs param p (result L c (c.exsChanges param) p))) {param p : V} : IsUFormula L p → P param p (result L c param p)

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.BV.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.BV.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.bv {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] (L : Language) [L.Encodable] [L.LORDefinable] (p : V) : V

Equations

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

noncomputable def LO.FirstOrder.Arithmetic.Bootstrapping.bvGraph (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.bv.defined {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] : 𝚺₁-Function₁ bv L via bvGraph L

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

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.bv_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) : bv L (qqRel k R v) = listMax (termBVVec L k v)

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.bv_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) : bv L (qqNRel k R v) = listMax (termBVVec L k v)

@[simp]

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.bv_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) : bv L (qqAnd p q) = bv L p ⊔ bv L q

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.bv_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) : bv L (qqOr p q) = bv L p ⊔ bv L q

@[simp]

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

@[simp]

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

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

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

• isUFormula : IsUFormula L p
• bv_le : bv L p ≤ n

@[reducible, inline]

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

Equations

• LO.FirstOrder.Arithmetic.Bootstrapping.IsFormula L p = LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula L 0 p

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

Equations

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

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

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

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

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

@[simp]

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

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.rel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k r v : V} : IsSemiformula L n (qqRel k r v) ↔ L.IsRel k r ∧ IsSemitermVec L k n v

@[simp]

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.nrel {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n k r v : V} : IsSemiformula L n (qqNRel k r v) ↔ L.IsRel k r ∧ IsSemitermVec L k n v

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.IsSemiformula.case_iff {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {n p : V} : IsSemiformula L n p ↔ (∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsSemitermVec L k n v ∧ p = qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.IsRel k R ∧ IsSemitermVec L k n v ∧ p = qqNRel k R v) ∨ p = qqVerum ∨ p = qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), IsSemiformula L n p₁ ∧ IsSemiformula L n p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), IsSemiformula L n p₁ ∧ IsSemiformula L n p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), IsSemiformula L (n + 1) p₁ ∧ p = qqAll p₁) ∨ ∃ (p₁ : V), IsSemiformula L (n + 1) p₁ ∧ p = qqExs p₁

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

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

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

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

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

@[simp]

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

theorem LO.FirstOrder.Arithmetic.Bootstrapping.UformulaRec1.Construction.semiformula_result_induction {V : Type u_1} [ORingStructure V] [V↓[ℒₒᵣ] ⊧* 𝗜𝚺₁] {L : Language} [L.Encodable] [L.LORDefinable] {β : Blueprint} {c : Construction V β} {P : V → V → V → V → Prop} (hP : 𝚺₁-Relation₄ P) (hRel : ∀ (n param k R v : V), L.IsRel k R → IsSemitermVec L k n v → P param n (qqRel k R v) (c.rel param k R v)) (hNRel : ∀ (n param k R v : V), L.IsRel k R → IsSemitermVec L k n v → P param n (qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (n param : V), P param n qqVerum (c.verum param)) (hfalsum : ∀ (n param : V), P param n qqFalsum (c.falsum param)) (hand : ∀ (n param p q : V), IsSemiformula L n p → IsSemiformula L n q → P param n p (result L c param p) → P param n q (result L c param q) → P param n (qqAnd p q) (c.and param p q (result L c param p) (result L c param q))) (hor : ∀ (n param p q : V), IsSemiformula L n p → IsSemiformula L n q → P param n p (result L c param p) → P param n q (result L c param q) → P param n (qqOr p q) (c.or param p q (result L c param p) (result L c param q))) (hall : ∀ (n param p : V), IsSemiformula L (n + 1) p → P (c.allChanges param) (n + 1) p (result L c (c.allChanges param) p) → P param n (qqAll p) (c.all param p (result L c (c.allChanges param) p))) (hexs : ∀ (n param p : V), IsSemiformula L (n + 1) p → P (c.exsChanges param) (n + 1) p (result L c (c.exsChanges param) p) → P param n (qqExs p) (c.exs param p (result L c (c.exsChanges param) p))) {param n p : V} : IsSemiformula L n p → P param n p (result L c param p)