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

Equations

• LO.Arith.qqRel k r v = ⟪0, ⟪k, ⟪r, v⟫⟫⟫ + 1

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

Equations

• LO.Arith.qqNRel k r v = ⟪1, ⟪k, ⟪r, v⟫⟫⟫ + 1

def LO.Arith.qqVerum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : V

Equations

• LO.Arith.qqVerum = ⟪2, 0⟫ + 1

def LO.Arith.qqFalsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : V

Equations

• LO.Arith.qqFalsum = ⟪3, 0⟫ + 1

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

Equations

• LO.Arith.qqAnd p q = ⟪4, ⟪p, q⟫⟫ + 1

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

Equations

• LO.Arith.qqOr p q = ⟪5, ⟪p, q⟫⟫ + 1

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

Equations

• LO.Arith.qqAll p = ⟪6, p⟫ + 1

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

Equations

• LO.Arith.qqEx p = ⟪7, p⟫ + 1

def LO.Arith.«term^rel_» : Lean.ParserDescr

Equations

• LO.Arith.«term^rel_» = Lean.ParserDescr.node `LO.Arith.term^rel_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^rel ") (Lean.ParserDescr.cat `term 1024))

def LO.Arith.«term^nrel_» : Lean.ParserDescr

Equations

• LO.Arith.«term^nrel_» = Lean.ParserDescr.node `LO.Arith.term^nrel_ 1024 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^nrel ") (Lean.ParserDescr.cat `term 1024))

def LO.Arith.«term^⊤» : Lean.ParserDescr

Equations

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

def LO.Arith.«term^⊥» : Lean.ParserDescr

Equations

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

def LO.Arith.«term_^⋏_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_^⋏_» = Lean.ParserDescr.trailingNode `LO.Arith.term_^⋏_ 1022 69 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^⋏ ") (Lean.ParserDescr.cat `term 70))

def LO.Arith.«term_^⋎_» : Lean.TrailingParserDescr

Equations

• LO.Arith.«term_^⋎_» = Lean.ParserDescr.trailingNode `LO.Arith.term_^⋎_ 1022 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ^⋎ ") (Lean.ParserDescr.cat `term 69))

def LO.Arith.«term^∀_» : Lean.ParserDescr

Equations

• LO.Arith.«term^∀_» = Lean.ParserDescr.node `LO.Arith.term^∀_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^∀ ") (Lean.ParserDescr.cat `term 64))

def LO.Arith.«term^∃_» : Lean.ParserDescr

Equations

• LO.Arith.«term^∃_» = Lean.ParserDescr.node `LO.Arith.term^∃_ 1022 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol "^∃ ") (Lean.ParserDescr.cat `term 64))

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

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

Equations

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

def LO.FirstOrder.Arith.qqExDef : 𝚺₀.Semisentence 2

Equations

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

theorem LO.Arith.qqRel_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₃ LO.Arith.qqRel via LO.FirstOrder.Arith.qqRelDef

theorem LO.Arith.qqNRel_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₃ LO.Arith.qqNRel via LO.FirstOrder.Arith.qqNRelDef

theorem LO.Arith.qqVerum_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₀ LO.Arith.qqVerum via LO.FirstOrder.Arith.qqVerumDef

theorem LO.Arith.qqFalsum_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₀ LO.Arith.qqFalsum via LO.FirstOrder.Arith.qqFalsumDef

theorem LO.Arith.qqAnd_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ LO.Arith.qqAnd via LO.FirstOrder.Arith.qqAndDef

theorem LO.Arith.qqOr_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₂ LO.Arith.qqOr via LO.FirstOrder.Arith.qqOrDef

theorem LO.Arith.qqForall_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.qqAll via LO.FirstOrder.Arith.qqAllDef

theorem LO.Arith.qqExists_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] : 𝚺₀-Function₁ LO.Arith.qqEx via LO.FirstOrder.Arith.qqExDef

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

instance LO.Arith.instBoldfaceFunction₃QqRel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₃ LO.Arith.qqRel

Equations

• ⋯ = ⋯

instance LO.Arith.instBoldfaceFunction₃QqNRel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₃ LO.Arith.qqNRel

Equations

• ⋯ = ⋯

instance LO.Arith.instBoldfaceFunction₂QqAnd {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ LO.Arith.qqAnd

Equations

• ⋯ = ⋯

instance LO.Arith.instBoldfaceFunction₂QqOr {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₂ LO.Arith.qqOr

Equations

• ⋯ = ⋯

instance LO.Arith.instBoldfaceFunction₁QqAll {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₁ LO.Arith.qqAll

Equations

• ⋯ = ⋯

instance LO.Arith.instBoldfaceFunction₁QqEx {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (ℌ : LO.FirstOrder.Arith.HierarchySymbol) : ℌ-Function₁ LO.Arith.qqEx

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.qqRel_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k₁ : V) (r₁ : V) (v₁ : V) (k₂ : V) (r₂ : V) (v₂ : V) : LO.Arith.qqRel k₁ r₁ v₁ = LO.Arith.qqRel k₂ r₂ v₂ ↔ k₁ = k₂ ∧ r₁ = r₂ ∧ v₁ = v₂

@[simp]

theorem LO.Arith.qqNRel_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k₁ : V) (r₁ : V) (v₁ : V) (k₂ : V) (r₂ : V) (v₂ : V) : LO.Arith.qqNRel k₁ r₁ v₁ = LO.Arith.qqNRel k₂ r₂ v₂ ↔ k₁ = k₂ ∧ r₁ = r₂ ∧ v₁ = v₂

@[simp]

theorem LO.Arith.qqAnd_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ : V) (q₁ : V) (p₂ : V) (q₂ : V) : LO.Arith.qqAnd p₁ q₁ = LO.Arith.qqAnd p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

@[simp]

theorem LO.Arith.qqOr_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ : V) (q₁ : V) (p₂ : V) (q₂ : V) : LO.Arith.qqOr p₁ q₁ = LO.Arith.qqOr p₂ q₂ ↔ p₁ = p₂ ∧ q₁ = q₂

@[simp]

theorem LO.Arith.qqAll_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ : V) (p₂ : V) : LO.Arith.qqAll p₁ = LO.Arith.qqAll p₂ ↔ p₁ = p₂

@[simp]

theorem LO.Arith.qqEx_inj {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p₁ : V) (p₂ : V) : LO.Arith.qqEx p₁ = LO.Arith.qqEx p₂ ↔ p₁ = p₂

@[simp]

theorem LO.Arith.arity_lt_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (r : V) (v : V) : k < LO.Arith.qqRel k r v

@[simp]

theorem LO.Arith.r_lt_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (r : V) (v : V) : r < LO.Arith.qqRel k r v

@[simp]

theorem LO.Arith.v_lt_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (r : V) (v : V) : v < LO.Arith.qqRel k r v

@[simp]

theorem LO.Arith.arity_lt_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (r : V) (v : V) : k < LO.Arith.qqNRel k r v

@[simp]

theorem LO.Arith.r_lt_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (r : V) (v : V) : r < LO.Arith.qqNRel k r v

@[simp]

theorem LO.Arith.v_lt_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (k : V) (r : V) (v : V) : v < LO.Arith.qqNRel k r v

theorem LO.Arith.nth_lt_qqRel_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {k : V} {r : V} {v : V} (hi : i < LO.Arith.len v) : LO.Arith.nth v i < LO.Arith.qqRel k r v

theorem LO.Arith.nth_lt_qqNRel_of_lt {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {i : V} {k : V} {r : V} {v : V} (hi : i < LO.Arith.len v) : LO.Arith.nth v i < LO.Arith.qqNRel k r v

@[simp]

theorem LO.Arith.lt_and_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) (q : V) : p < LO.Arith.qqAnd p q

@[simp]

theorem LO.Arith.lt_and_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) (q : V) : q < LO.Arith.qqAnd p q

@[simp]

theorem LO.Arith.lt_or_left {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) (q : V) : p < LO.Arith.qqOr p q

@[simp]

theorem LO.Arith.lt_or_right {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) (q : V) : q < LO.Arith.qqOr p q

@[simp]

theorem LO.Arith.lt_forall {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : p < LO.Arith.qqAll p

@[simp]

theorem LO.Arith.lt_exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (p : V) : p < LO.Arith.qqEx p

def LO.Arith.FormalizedFormula.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (C : Set V) (p : V) : Prop

Equations

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

def LO.Arith.FormalizedFormula.formulaAux : 𝚺₀.Semisentence 2

Equations

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

def LO.Arith.FormalizedFormula.blueprint (pL : LO.FirstOrder.Arith.LDef) : LO.Arith.Fixpoint.Blueprint 0

Equations

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

def LO.Arith.FormalizedFormula.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : LO.Arith.Fixpoint.Construction V (LO.Arith.FormalizedFormula.blueprint pL)

Equations

• LO.Arith.FormalizedFormula.construction L = { Φ := fun (x : Fin 0 → V) => LO.Arith.FormalizedFormula.Phi L, defined := ⋯, monotone := ⋯ }

instance LO.Arith.FormalizedFormula.instStrongFiniteConstruction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : LO.Arith.Fixpoint.Construction.StrongFinite V (LO.Arith.FormalizedFormula.construction L)

Equations

• LO.Arith.FormalizedFormula.instStrongFiniteConstruction L = { strong_finite := ⋯ }

def LO.Arith.Language.IsUFormula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : V → Prop

Equations

• L.IsUFormula = (LO.Arith.FormalizedFormula.construction L).Fixpoint ![]

def LO.FirstOrder.Arith.LDef.isUFormulaDef (pL : LO.FirstOrder.Arith.LDef) : 𝚫₁.Semisentence 1

Equations

• pL.isUFormulaDef = (LO.Arith.FormalizedFormula.blueprint pL).fixpointDefΔ₁

theorem LO.Arith.Language.isUFormula_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Predicate L.IsUFormula via pL.isUFormulaDef

instance LO.Arith.Language.isUFormulaDef_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Predicate L.IsUFormula

Equations

• ⋯ = ⋯

instance LO.Arith.Language.isUFormulaDef_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Predicate L.IsUFormula

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.IsUFormula.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} : L.IsUFormula p ↔ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqEx p₁

theorem LO.Arith.Language.IsUFormula.mk {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} : ((∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqEx p₁) → L.IsUFormula p

Alias of the reverse direction of LO.Arith.Language.IsUFormula.case_iff.

theorem LO.Arith.Language.IsUFormula.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} : L.IsUFormula p → (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = LO.Arith.qqEx p₁

Alias of the forward direction of LO.Arith.Language.IsUFormula.case_iff.

@[simp]

theorem LO.Arith.Language.IsUFormula.rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {r : V} {v : V} : L.IsUFormula (LO.Arith.qqRel k r v) ↔ L.Rel k r ∧ L.IsUTermVec k v

@[simp]

theorem LO.Arith.Language.IsUFormula.nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {r : V} {v : V} : L.IsUFormula (LO.Arith.qqNRel k r v) ↔ L.Rel k r ∧ L.IsUTermVec k v

@[simp]

theorem LO.Arith.Language.IsUFormula.verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : L.IsUFormula LO.Arith.qqVerum

@[simp]

theorem LO.Arith.Language.IsUFormula.falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : L.IsUFormula LO.Arith.qqFalsum

@[simp]

theorem LO.Arith.Language.IsUFormula.and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} : L.IsUFormula (LO.Arith.qqAnd p q) ↔ L.IsUFormula p ∧ L.IsUFormula q

@[simp]

theorem LO.Arith.Language.IsUFormula.or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} : L.IsUFormula (LO.Arith.qqOr p q) ↔ L.IsUFormula p ∧ L.IsUFormula q

@[simp]

theorem LO.Arith.Language.IsUFormula.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} : L.IsUFormula (LO.Arith.qqAll p) ↔ L.IsUFormula p

@[simp]

theorem LO.Arith.Language.IsUFormula.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} : L.IsUFormula (LO.Arith.qqEx p) ↔ L.IsUFormula p

theorem LO.Arith.Language.IsUFormula.pos {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (h : L.IsUFormula p) : 0 < p

@[simp]

theorem LO.Arith.Language.IsUFormula.not_zero {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : ¬L.IsUFormula 0

theorem LO.Arith.Language.IsUFormula.induction1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : LO.SigmaPiDelta) {P : V → Prop} (hP : { Γ := Γ, rank := 1 }-Predicate P) (hrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqNRel k r v)) (hverum : P LO.Arith.qqVerum) (hfalsum : P LO.Arith.qqFalsum) (hand : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqOr p q)) (hall : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqAll p)) (hex : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqEx p)) (p : V) : L.IsUFormula p → P p

theorem LO.Arith.Language.IsUFormula.induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : V → Prop} (hP : 𝚺₁-Predicate P) (hrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqNRel k r v)) (hverum : P LO.Arith.qqVerum) (hfalsum : P LO.Arith.qqFalsum) (hand : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqOr p q)) (hall : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqAll p)) (hex : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqEx p)) (p : V) : L.IsUFormula p → P p

theorem LO.Arith.Language.IsUFormula.induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : V → Prop} (hP : 𝚷₁-Predicate P) (hrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqRel k r v)) (hnrel : ∀ (k r v : V), L.Rel k r → L.IsUTermVec k v → P (LO.Arith.qqNRel k r v)) (hverum : P LO.Arith.qqVerum) (hfalsum : P LO.Arith.qqFalsum) (hand : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqAnd p q)) (hor : ∀ (p q : V), L.IsUFormula p → L.IsUFormula q → P p → P q → P (LO.Arith.qqOr p q)) (hall : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqAll p)) (hex : ∀ (p : V), L.IsUFormula p → P p → P (LO.Arith.qqEx p)) (p : V) : L.IsUFormula p → P p

structure LO.Arith.Language.UformulaRec1.Blueprint (pL : LO.FirstOrder.Arith.LDef) : Type

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

def LO.Arith.Language.UformulaRec1.Blueprint.blueprint {pL : LO.FirstOrder.Arith.LDef} (β : LO.Arith.Language.UformulaRec1.Blueprint pL) : LO.Arith.Fixpoint.Blueprint 0

Equations

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

def LO.Arith.Language.UformulaRec1.Blueprint.graph {pL : LO.FirstOrder.Arith.LDef} (β : LO.Arith.Language.UformulaRec1.Blueprint pL) : 𝚺₁.Semisentence 3

Equations

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

def LO.Arith.Language.UformulaRec1.Blueprint.result {pL : LO.FirstOrder.Arith.LDef} (β : LO.Arith.Language.UformulaRec1.Blueprint pL) : 𝚺₁.Semisentence 3

Equations

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

structure LO.Arith.Language.UformulaRec1.Construction (V : Type u_1) [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} (L : LO.Arith.Language V) (φ : LO.Arith.Language.UformulaRec1.Blueprint pL) : Type u_1

• rel : V → V → V → V → V
• nrel : V → V → V → V → V
• verum : V → V
• falsum : V → V
• and : V → V → V → V → V → V
• or : V → V → V → V → V → V
• all : V → V → V → V
• ex : V → V → V → V
• allChanges : V → V
• exChanges : 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
• ex_defined : 𝚺₁-Function₃ self.ex via φ.ex
• allChanges_defined : 𝚺₁-Function₁ self.allChanges via φ.allChanges
• exChanges_defined : 𝚺₁-Function₁ self.exChanges via φ.exChanges

theorem LO.Arith.Language.UformulaRec1.Construction.rel_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₄ self.rel via φ.rel

theorem LO.Arith.Language.UformulaRec1.Construction.nrel_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₄ self.nrel via φ.nrel

theorem LO.Arith.Language.UformulaRec1.Construction.verum_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₁ self.verum via φ.verum

theorem LO.Arith.Language.UformulaRec1.Construction.falsum_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₁ self.falsum via φ.falsum

theorem LO.Arith.Language.UformulaRec1.Construction.and_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₅ self.and via φ.and

theorem LO.Arith.Language.UformulaRec1.Construction.or_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₅ self.or via φ.or

theorem LO.Arith.Language.UformulaRec1.Construction.all_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₃ self.all via φ.all

theorem LO.Arith.Language.UformulaRec1.Construction.ex_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₃ self.ex via φ.ex

theorem LO.Arith.Language.UformulaRec1.Construction.allChanges_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₁ self.allChanges via φ.allChanges

theorem LO.Arith.Language.UformulaRec1.Construction.exChanges_defined {V : Type u_1} [LO.ORingStruc V] {pL : LO.FirstOrder.Arith.LDef} {L : LO.Arith.Language V} {φ : LO.Arith.Language.UformulaRec1.Blueprint pL} (self : LO.Arith.Language.UformulaRec1.Construction V L φ) : 𝚺₁-Function₁ self.exChanges via φ.exChanges

def LO.Arith.Language.UformulaRec1.Construction.Phi {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (C : Set V) (pr : V) : Prop

Equations

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

def LO.Arith.Language.UformulaRec1.Construction.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) : LO.Arith.Fixpoint.Construction V β.blueprint

Equations

• c.construction = { Φ := fun (x : Fin 0 → V) => c.Phi, defined := ⋯, monotone := ⋯ }

instance LO.Arith.Language.UformulaRec1.Construction.instFiniteConstruction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) : LO.Arith.Fixpoint.Construction.Finite V c.construction

Equations

• c.instFiniteConstruction = { finite := ⋯ }

def LO.Arith.Language.UformulaRec1.Construction.Graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) (x : V) (y : V) : Prop

Equations

• c.Graph param x y = c.construction.Fixpoint ![] ⟪param, ⟪x, y⟫⟫

theorem LO.Arith.Language.UformulaRec1.Construction.Graph.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} {c : LO.Arith.Language.UformulaRec1.Construction V L β} {param : V} {p : V} {y : V} : c.Graph param p y ↔ L.IsUFormula p ∧ ((∃ (k : V) (R : V) (v : V), p = LO.Arith.qqRel k R v ∧ y = c.rel param k R v) ∨ (∃ (k : V) (R : V) (v : V), p = LO.Arith.qqNRel k R v ∧ y = c.nrel param k R v) ∨ p = LO.Arith.qqVerum ∧ y = c.verum param ∨ p = LO.Arith.qqFalsum ∧ y = c.falsum param ∨ (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V), c.Graph param p₁ y₁ ∧ c.Graph param p₂ y₂ ∧ p = LO.Arith.qqAnd p₁ p₂ ∧ y = c.and param p₁ p₂ y₁ y₂) ∨ (∃ (p₁ : V) (p₂ : V) (y₁ : V) (y₂ : V), c.Graph param p₁ y₁ ∧ c.Graph param p₂ y₂ ∧ p = LO.Arith.qqOr p₁ p₂ ∧ y = c.or param p₁ p₂ y₁ y₂) ∨ (∃ (p₁ : V) (y₁ : V), c.Graph (c.allChanges param) p₁ y₁ ∧ p = LO.Arith.qqAll p₁ ∧ y = c.all param p₁ y₁) ∨ ∃ (p₁ : V) (y₁ : V), c.Graph (c.exChanges param) p₁ y₁ ∧ p = LO.Arith.qqEx p₁ ∧ y = c.ex param p₁ y₁)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (β : LO.Arith.Language.UformulaRec1.Blueprint pL) (c : LO.Arith.Language.UformulaRec1.Construction V L β) : 𝚺₁-Relation₃ c.Graph via β.graph

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.eval_graphDef {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (β : LO.Arith.Language.UformulaRec1.Blueprint pL) (c : LO.Arith.Language.UformulaRec1.Construction V L β) (v : Fin 3 → V) : V ⊧/v (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val β.graph) ↔ c.Graph (v 0) (v 1) (v 2)

instance LO.Arith.Language.UformulaRec1.Construction.graph_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (β : LO.Arith.Language.UformulaRec1.Blueprint pL) (c : LO.Arith.Language.UformulaRec1.Construction V L β) : { Γ := 𝚺, rank := 0 + 1 }-Relation₃ c.Graph

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.UformulaRec1.Construction.graph_dom_uformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {r : V} : c.Graph param p r → L.IsUFormula p

theorem LO.Arith.Language.UformulaRec1.Construction.graph_rel_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} {y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) : c.Graph param (LO.Arith.qqRel k r v) y ↔ y = c.rel param k r v

theorem LO.Arith.Language.UformulaRec1.Construction.graph_nrel_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} {y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) : c.Graph param (LO.Arith.qqNRel k r v) y ↔ y = c.nrel param k r v

theorem LO.Arith.Language.UformulaRec1.Construction.graph_verum_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {y : V} : c.Graph param LO.Arith.qqVerum y ↔ y = c.verum param

theorem LO.Arith.Language.UformulaRec1.Construction.graph_falsum_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {y : V} : c.Graph param LO.Arith.qqFalsum y ↔ y = c.falsum param

theorem LO.Arith.Language.UformulaRec1.Construction.graph_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) : c.Graph param (LO.Arith.qqRel k r v) (c.rel param k r v)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {r : V} {v : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) : c.Graph param (LO.Arith.qqNRel k r v) (c.nrel param k r v)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} : c.Graph param LO.Arith.qqVerum (c.verum param)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} : c.Graph param LO.Arith.qqFalsum (c.falsum param)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r₁ : V} {r₂ : V} (hp₁ : L.IsUFormula p₁) (hp₂ : L.IsUFormula p₂) (h₁ : c.Graph param p₁ r₁) (h₂ : c.Graph param p₂ r₂) : c.Graph param (LO.Arith.qqAnd p₁ p₂) (c.and param p₁ p₂ r₁ r₂)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_and_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r : V} : c.Graph param (LO.Arith.qqAnd p₁ p₂) r → ∃ (r₁ : V) (r₂ : V), c.Graph param p₁ r₁ ∧ c.Graph param p₂ r₂ ∧ r = c.and param p₁ p₂ r₁ r₂

theorem LO.Arith.Language.UformulaRec1.Construction.graph_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r₁ : V} {r₂ : V} (hp₁ : L.IsUFormula p₁) (hp₂ : L.IsUFormula p₂) (h₁ : c.Graph param p₁ r₁) (h₂ : c.Graph param p₂ r₂) : c.Graph param (LO.Arith.qqOr p₁ p₂) (c.or param p₁ p₂ r₁ r₂)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_or_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {p₂ : V} {r : V} : c.Graph param (LO.Arith.qqOr p₁ p₂) r → ∃ (r₁ : V) (r₂ : V), c.Graph param p₁ r₁ ∧ c.Graph param p₂ r₂ ∧ r = c.or param p₁ p₂ r₁ r₂

theorem LO.Arith.Language.UformulaRec1.Construction.graph_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.allChanges param) p₁ r₁) : c.Graph param (LO.Arith.qqAll p₁) (c.all param p₁ r₁)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_all_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r : V} : c.Graph param (LO.Arith.qqAll p₁) r → ∃ (r₁ : V), c.Graph (c.allChanges param) p₁ r₁ ∧ r = c.all param p₁ r₁

theorem LO.Arith.Language.UformulaRec1.Construction.graph_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.exChanges param) p₁ r₁) : c.Graph param (LO.Arith.qqEx p₁) (c.ex param p₁ r₁)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_ex_inv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p₁ : V} {r : V} : c.Graph param (LO.Arith.qqEx p₁) r → ∃ (r₁ : V), c.Graph (c.exChanges param) p₁ r₁ ∧ r = c.ex param p₁ r₁

theorem LO.Arith.Language.UformulaRec1.Construction.graph_exists {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) {p : V} : L.IsUFormula p → ∃ (y : V), c.Graph param p y

theorem LO.Arith.Language.UformulaRec1.Construction.graph_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {p : V} : L.IsUFormula p → ∀ {param r r' : V}, c.Graph param p r → c.Graph param p r' → r = r'

theorem LO.Arith.Language.UformulaRec1.Construction.exists_unique {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) {p : V} (hp : L.IsUFormula p) : ∃! r : V, c.Graph param p r

theorem LO.Arith.Language.UformulaRec1.Construction.exists_unique_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) (p : V) : ∃! r : V, (L.IsUFormula p → c.Graph param p r) ∧ (¬L.IsUFormula p → r = 0)

def LO.Arith.Language.UformulaRec1.Construction.result {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) (p : V) : V

Equations

• c.result param p = Classical.choose! ⋯

theorem LO.Arith.Language.UformulaRec1.Construction.result_prop {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) {p : V} (hp : L.IsUFormula p) : c.Graph param p (c.result param p)

theorem LO.Arith.Language.UformulaRec1.Construction.result_prop_not {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) (param : V) {p : V} (hp : ¬L.IsUFormula p) : c.result param p = 0

theorem LO.Arith.Language.UformulaRec1.Construction.result_eq_of_graph {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {r : V} (h : c.Graph param p r) : c.result param p = r

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) : c.result param (LO.Arith.qqRel k R v) = c.rel param k R v

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) : c.result param (LO.Arith.qqNRel k R v) = c.nrel param k R v

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} : c.result param LO.Arith.qqVerum = c.verum param

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} : c.result param LO.Arith.qqFalsum = c.falsum param

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) : c.result param (LO.Arith.qqAnd p q) = c.and param p q (c.result param p) (c.result param q)

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) : c.result param (LO.Arith.qqOr p q) = c.or param p q (c.result param p) (c.result param q)

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} (hp : L.IsUFormula p) : c.result param (LO.Arith.qqAll p) = c.all param p (c.result (c.allChanges param) p)

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {param : V} {p : V} (hp : L.IsUFormula p) : c.result param (LO.Arith.qqEx p) = c.ex param p (c.result (c.exChanges param) p)

theorem LO.Arith.Language.UformulaRec1.Construction.result_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) : 𝚺₁-Function₂ c.result via β.result

instance LO.Arith.Language.UformulaRec1.Construction.result_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) : { Γ := 𝚺, rank := 0 + 1 }-Function₂ c.result

Equations

• ⋯ = ⋯

theorem LO.Arith.Language.UformulaRec1.Construction.uformula_result_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} (c : LO.Arith.Language.UformulaRec1.Construction V L β) {P : V → V → V → Prop} (hP : 𝚺₁-Relation₃ P) (hRel : ∀ (param k R v : V), L.Rel k R → L.IsUTermVec k v → P param (LO.Arith.qqRel k R v) (c.rel param k R v)) (hNRel : ∀ (param k R v : V), L.Rel k R → L.IsUTermVec k v → P param (LO.Arith.qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (param : V), P param LO.Arith.qqVerum (c.verum param)) (hfalsum : ∀ (param : V), P param LO.Arith.qqFalsum (c.falsum param)) (hand : ∀ (param p q : V), L.IsUFormula p → L.IsUFormula q → P param p (c.result param p) → P param q (c.result param q) → P param (LO.Arith.qqAnd p q) (c.and param p q (c.result param p) (c.result param q))) (hor : ∀ (param p q : V), L.IsUFormula p → L.IsUFormula q → P param p (c.result param p) → P param q (c.result param q) → P param (LO.Arith.qqOr p q) (c.or param p q (c.result param p) (c.result param q))) (hall : ∀ (param p : V), L.IsUFormula p → P (c.allChanges param) p (c.result (c.allChanges param) p) → P param (LO.Arith.qqAll p) (c.all param p (c.result (c.allChanges param) p))) (hex : ∀ (param p : V), L.IsUFormula p → P (c.exChanges param) p (c.result (c.exChanges param) p) → P param (LO.Arith.qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param : V} {p : V} : L.IsUFormula p → P param p (c.result param p)

def LO.Arith.BV.blueprint (pL : LO.FirstOrder.Arith.LDef) : LO.Arith.Language.UformulaRec1.Blueprint pL

Equations

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

def LO.Arith.BV.construction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : LO.Arith.Language.UformulaRec1.Construction V L (LO.Arith.BV.blueprint pL)

Equations

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

def LO.Arith.Language.bv {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) : V

Equations

• L.bv p = (LO.Arith.BV.construction L).result 0 p

def LO.FirstOrder.Arith.LDef.bvDef (pL : LO.FirstOrder.Arith.LDef) : 𝚺₁.Semisentence 2

Equations

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

theorem LO.Arith.Language.bv_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₁-Function₁ L.bv via pL.bvDef

instance LO.Arith.Language.bv_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚺₁-Function₁ L.bv

Equations

• ⋯ = ⋯

instance LO.Arith.Language.bv_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {m : ℕ} (Γ : LO.SigmaPiDelta) : { Γ := Γ, rank := m + 1 }-Function₁ L.bv

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.bv_rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) : L.bv (LO.Arith.qqRel k R v) = LO.Arith.listMax (L.termBVVec k v)

@[simp]

theorem LO.Arith.bv_nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {k : V} {R : V} {v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) : L.bv (LO.Arith.qqNRel k R v) = LO.Arith.listMax (L.termBVVec k v)

@[simp]

theorem LO.Arith.bv_verum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : L.bv LO.Arith.qqVerum = 0

@[simp]

theorem LO.Arith.bv_falsum {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : L.bv LO.Arith.qqFalsum = 0

@[simp]

theorem LO.Arith.bv_and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) : L.bv (LO.Arith.qqAnd p q) = max (L.bv p) (L.bv q)

@[simp]

theorem LO.Arith.bv_or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} {q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) : L.bv (LO.Arith.qqOr p q) = max (L.bv p) (L.bv q)

@[simp]

theorem LO.Arith.bv_all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) : L.bv (LO.Arith.qqAll p) = L.bv p - 1

@[simp]

theorem LO.Arith.bv_ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (hp : L.IsUFormula p) : L.bv (LO.Arith.qqEx p) = L.bv p - 1

theorem LO.Arith.bv_eq_of_not_isUFormula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (h : ¬L.IsUFormula p) : L.bv p = 0

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

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

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

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

@[reducible, inline]

abbrev LO.Arith.Language.IsFormula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (p : V) : Prop

Equations

• L.IsFormula p = L.IsSemiformula 0 p

theorem LO.Arith.Language.isSemiformula_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} : L.IsSemiformula n p ↔ L.IsUFormula p ∧ L.bv p ≤ n

def LO.FirstOrder.Arith.LDef.isSemiformulaDef (pL : LO.FirstOrder.Arith.LDef) : 𝚫₁.Semisentence 2

Equations

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

theorem LO.Arith.Language.isSemiformula_defined {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsSemiformula via pL.isSemiformulaDef

instance LO.Arith.Language.isSemiformula_definable {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : 𝚫₁-Relation L.IsSemiformula

Equations

• ⋯ = ⋯

instance LO.Arith.Language.isSemiformulaDef_definable' {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {Γ : LO.SigmaPiDelta} {m : ℕ} : { Γ := Γ, rank := m + 1 }-Relation L.IsSemiformula

Equations

• ⋯ = ⋯

@[simp]

theorem LO.Arith.Language.IsUFormula.isSemiformula {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {p : V} (h : L.IsUFormula p) : L.IsSemiformula (L.bv p) p

@[simp]

theorem LO.Arith.Language.IsSemiformula.rel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {r : V} {v : V} : L.IsSemiformula n (LO.Arith.qqRel k r v) ↔ L.Rel k r ∧ L.IsSemitermVec k n v

@[simp]

theorem LO.Arith.Language.IsSemiformula.nrel {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {k : V} {r : V} {v : V} : L.IsSemiformula n (LO.Arith.qqNRel k r v) ↔ L.Rel k r ∧ L.IsSemitermVec k n v

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Arith.Language.IsSemiformula.and {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} : L.IsSemiformula n (LO.Arith.qqAnd p q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q

@[simp]

theorem LO.Arith.Language.IsSemiformula.or {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} {q : V} : L.IsSemiformula n (LO.Arith.qqOr p q) ↔ L.IsSemiformula n p ∧ L.IsSemiformula n q

@[simp]

theorem LO.Arith.Language.IsSemiformula.all {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} : L.IsSemiformula n (LO.Arith.qqAll p) ↔ L.IsSemiformula (n + 1) p

@[simp]

theorem LO.Arith.Language.IsSemiformula.ex {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} : L.IsSemiformula n (LO.Arith.qqEx p) ↔ L.IsSemiformula (n + 1) p

theorem LO.Arith.Language.IsSemiformula.case_iff {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {n : V} {p : V} : L.IsSemiformula n p ↔ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsSemitermVec k n v ∧ p = LO.Arith.qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsSemitermVec k n v ∧ p = LO.Arith.qqNRel k R v) ∨ p = LO.Arith.qqVerum ∨ p = LO.Arith.qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ ∧ L.IsSemiformula n p₂ ∧ p = LO.Arith.qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsSemiformula n p₁ ∧ L.IsSemiformula n p₂ ∧ p = LO.Arith.qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ ∧ p = LO.Arith.qqAll p₁) ∨ ∃ (p₁ : V), L.IsSemiformula (n + 1) p₁ ∧ p = LO.Arith.qqEx p₁

theorem LO.Arith.Language.IsSemiformula.case {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → Prop} {n : V} {p : V} (hp : L.IsSemiformula n p) (hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P n (LO.Arith.qqEx p)) : P n p

theorem LO.Arith.Language.IsSemiformula.induction_sigma1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → Prop} (hP : 𝚺₁-Relation P) (hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqEx p)) {n : V} {p : V} : L.IsSemiformula n p → P n p

theorem LO.Arith.Language.IsSemiformula.induction_pi1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → Prop} (hP : 𝚷₁-Relation P) (hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqEx p)) {n : V} {p : V} : L.IsSemiformula n p → P n p

theorem LO.Arith.Language.IsSemiformula.induction1 {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (Γ : LO.SigmaPiDelta) {P : V → V → Prop} (hP : { Γ := Γ, rank := 1 }-Relation P) (hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (LO.Arith.qqNRel k r v)) (hverum : ∀ (n : V), P n LO.Arith.qqVerum) (hfalsum : ∀ (n : V), P n LO.Arith.qqFalsum) (hand : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (LO.Arith.qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (LO.Arith.qqEx p)) {n : V} {p : V} : L.IsSemiformula n p → P n p

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

@[simp]

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

theorem LO.Arith.Language.UformulaRec1.Construction.semiformula_result_induction {V : Type u_1} [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {β : LO.Arith.Language.UformulaRec1.Blueprint pL} {c : LO.Arith.Language.UformulaRec1.Construction V L β} {P : V → V → V → V → Prop} (hP : 𝚺₁-Relation₄ P) (hRel : ∀ (n param k R v : V), L.Rel k R → L.IsSemitermVec k n v → P param n (LO.Arith.qqRel k R v) (c.rel param k R v)) (hNRel : ∀ (n param k R v : V), L.Rel k R → L.IsSemitermVec k n v → P param n (LO.Arith.qqNRel k R v) (c.nrel param k R v)) (hverum : ∀ (n param : V), P param n LO.Arith.qqVerum (c.verum param)) (hfalsum : ∀ (n param : V), P param n LO.Arith.qqFalsum (c.falsum param)) (hand : ∀ (n param p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P param n p (c.result param p) → P param n q (c.result param q) → P param n (LO.Arith.qqAnd p q) (c.and param p q (c.result param p) (c.result param q))) (hor : ∀ (n param p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P param n p (c.result param p) → P param n q (c.result param q) → P param n (LO.Arith.qqOr p q) (c.or param p q (c.result param p) (c.result param q))) (hall : ∀ (n param p : V), L.IsSemiformula (n + 1) p → P (c.allChanges param) (n + 1) p (c.result (c.allChanges param) p) → P param n (LO.Arith.qqAll p) (c.all param p (c.result (c.allChanges param) p))) (hex : ∀ (n param p : V), L.IsSemiformula (n + 1) p → P (c.exChanges param) (n + 1) p (c.result (c.exChanges param) p) → P param n (LO.Arith.qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param : V} {n : V} {p : V} : L.IsSemiformula n p → P param n p (c.result param p)