Basic

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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 : Sg0.Semisentence 4

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.qqNRelDef : Sg0.Semisentence 4

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.qqVerumDef : Sg0.Semisentence 1

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.qqFalsumDef : Sg0.Semisentence 1

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.qqAndDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.qqOrDef : Sg0.Semisentence 3

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.qqAllDef : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.FirstOrder.Arith.qqExDef : Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

def LO.Arith.FormalizedFormula.formulaAux : FirstOrder.Arith.Sg0.Semisentence 2

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] : Fixpoint.Construction.StrongFinite V (construction L)

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

theorem LO.Arith.Language.IsUFormula.case_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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 = qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = qqNRel k R v) ∨ p = qqVerum ∨ p = qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = qqEx p₁

theorem LO.Arith.Language.IsUFormula.mk {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {p : V} : ((∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = qqNRel k R v) ∨ p = qqVerum ∨ p = qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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 = qqRel k R v) ∨ (∃ (k : V) (R : V) (v : V), L.Rel k R ∧ L.IsUTermVec k v ∧ p = qqNRel k R v) ∨ p = qqVerum ∨ p = qqFalsum ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = qqAnd p₁ p₂) ∨ (∃ (p₁ : V) (p₂ : V), L.IsUFormula p₁ ∧ L.IsUFormula p₂ ∧ p = qqOr p₁ p₂) ∨ (∃ (p₁ : V), L.IsUFormula p₁ ∧ p = qqAll p₁) ∨ ∃ (p₁ : V), L.IsUFormula p₁ ∧ p = 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {k r v : V} : L.IsUFormula (qqRel k r v) ↔ L.Rel k r ∧ L.IsUTermVec k v

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.Arith.Language.IsUFormula.pos {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] : ¬L.IsUFormula 0

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

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

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

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

Imported declaration from the Incompleteness formalization.

• rel : FirstOrder.Arith.Sg1.Semisentence 5

  Imported declaration from the Incompleteness formalization.

• nrel : FirstOrder.Arith.Sg1.Semisentence 5

  Imported declaration from the Incompleteness formalization.

• verum : FirstOrder.Arith.Sg1.Semisentence 2

  Imported declaration from the Incompleteness formalization.

• falsum : FirstOrder.Arith.Sg1.Semisentence 2

  Imported declaration from the Incompleteness formalization.

• and : FirstOrder.Arith.Sg1.Semisentence 6

  Imported declaration from the Incompleteness formalization.

• or : FirstOrder.Arith.Sg1.Semisentence 6

  Imported declaration from the Incompleteness formalization.

• all : FirstOrder.Arith.Sg1.Semisentence 4

  Imported declaration from the Incompleteness formalization.

• ex : FirstOrder.Arith.Sg1.Semisentence 4

  Imported declaration from the Incompleteness formalization.

• allChanges : FirstOrder.Arith.Sg1.Semisentence 2

  Imported declaration from the Incompleteness formalization.

• exChanges : FirstOrder.Arith.Sg1.Semisentence 2

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

• rel (param k R v : V) : V

  Imported declaration from the Incompleteness formalization.

• nrel (param k R v : V) : V

  Imported declaration from the Incompleteness formalization.

• verum (param : V) : V

  Imported declaration from the Incompleteness formalization.

• falsum (param : V) : V

  Imported declaration from the Incompleteness formalization.

• and (param p₁ p₂ y₁ y₂ : V) : V

  Imported declaration from the Incompleteness formalization.

• or (param p₁ p₂ y₁ y₂ : V) : V

  Imported declaration from the Incompleteness formalization.

• all (param p₁ y₁ : V) : V

  Imported declaration from the Incompleteness formalization.

• ex (param p₁ y₁ : V) : V

  Imported declaration from the Incompleteness formalization.

• allChanges (param : V) : V

  Imported declaration from the Incompleteness formalization.

• exChanges (param : V) : V

  Imported declaration from the Incompleteness formalization.

• rel_defined : FirstOrder.Arith.Sg1-Function₄ self.rel via φ.rel
• nrel_defined : FirstOrder.Arith.Sg1-Function₄ self.nrel via φ.nrel
• verum_defined : FirstOrder.Arith.Sg1-Function₁ self.verum via φ.verum
• falsum_defined : FirstOrder.Arith.Sg1-Function₁ self.falsum via φ.falsum
• and_defined : FirstOrder.Arith.Sg1-Function₅ self.and via φ.and
• or_defined : FirstOrder.Arith.Sg1-Function₅ self.or via φ.or
• all_defined : FirstOrder.Arith.Sg1-Function₃ self.all via φ.all
• ex_defined : FirstOrder.Arith.Sg1-Function₃ self.ex via φ.ex
• allChanges_defined : FirstOrder.Arith.Sg1-Function₁ self.allChanges via φ.allChanges
• exChanges_defined : FirstOrder.Arith.Sg1-Function₁ self.exChanges via φ.exChanges

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

Imported declaration from the Incompleteness formalization.

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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} {c : Construction V L β} {param p y : V} : c.Graph param p y ↔ L.IsUFormula 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), c.Graph param p₁ y₁ ∧ c.Graph param p₂ y₂ ∧ p = 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 = qqOr p₁ p₂ ∧ y = c.or param p₁ p₂ y₁ y₂) ∨ (∃ (p₁ : V) (y₁ : V), c.Graph (c.allChanges param) p₁ y₁ ∧ p = qqAll p₁ ∧ y = c.all param p₁ y₁) ∨ ∃ (p₁ : V) (y₁ : V), c.Graph (c.exChanges param) p₁ y₁ ∧ p = qqEx p₁ ∧ y = c.ex param p₁ y₁)

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

theorem LO.Arith.Language.UformulaRec1.Construction.eval_graphDef {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (β : Blueprint pL) (c : Construction V L β) (v : Fin 3 → V) : V ⊧/v (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (β : Blueprint pL) (c : Construction V L β) : { Γ := Sg, rank := 0 + 1 }-Relation₃ c.Graph

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

theorem LO.Arith.Language.UformulaRec1.Construction.graph_rel_iff {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k r v y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) : c.Graph param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k r v y : V} (hkr : L.Rel k r) (hv : L.IsUTermVec k v) : c.Graph param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param y : V} : c.Graph param qqVerum y ↔ y = c.verum param

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

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

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

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

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

theorem LO.Arith.Language.UformulaRec1.Construction.graph_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r₁ 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 (qqAnd p₁ p₂) (c.and param p₁ p₂ r₁ r₂)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_and_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r : V} : c.Graph param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r₁ 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 (qqOr p₁ p₂) (c.or param p₁ p₂ r₁ r₂)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_or_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ p₂ r : V} : c.Graph param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.allChanges param) p₁ r₁) : c.Graph param (qqAll p₁) (c.all param p₁ r₁)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_all_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r : V} : c.Graph param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r₁ : V} (hp₁ : L.IsUFormula p₁) (h₁ : c.Graph (c.exChanges param) p₁ r₁) : c.Graph param (qqEx p₁) (c.ex param p₁ r₁)

theorem LO.Arith.Language.UformulaRec1.Construction.graph_ex_inv {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p₁ r : V} : c.Graph param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) (param p : V) : ∃! r : V, (L.IsUFormula p → c.Graph param p r) ∧ (¬L.IsUFormula p → r = 0)

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

Imported declaration from the Incompleteness formalization.

Equations

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

theorem LO.Arith.Language.UformulaRec1.Construction.result_prop {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param k R v : V} (hR : L.Rel k R) (hv : L.IsUTermVec k v) : c.result param (qqRel k R v) = c.rel param k R v

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem LO.Arith.Language.UformulaRec1.Construction.result_and {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) : c.result param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p q : V} (hp : L.IsUFormula p) (hq : L.IsUFormula q) : c.result param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p : V} (hp : L.IsUFormula p) : c.result param (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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {param p : V} (hp : L.IsUFormula p) : c.result param (qqEx p) = c.ex param p (c.result (c.exChanges param) p)

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

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

theorem LO.Arith.Language.UformulaRec1.Construction.uformula_result_induction {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} (c : Construction V L β) {P : V → V → V → Prop} (hP : FirstOrder.Arith.Sg1-Relation₃ P) (hRel : ∀ (param k R v : V), L.Rel k R → L.IsUTermVec k v → P param (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 (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), L.IsUFormula p → L.IsUFormula q → P param p (c.result param p) → P param q (c.result param q) → P param (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 (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 (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 (qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param p : V} : L.IsUFormula p → P param p (c.result param p)

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

theorem LO.Arith.bv_eq_of_not_isUFormula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] (L : Arith.Language V) {pL : FirstOrder.Arith.LDef} [L.Defined pL] (n p : V) : Prop

Imported declaration from the Incompleteness formalization.

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

@[reducible, inline]

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

Imported declaration from the Incompleteness formalization.

Equations

• L.IsFormula p = L.IsSemiformula 0 p

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

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

Imported declaration from the Incompleteness formalization.

Equations

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

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

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

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

@[simp]

theorem LO.Arith.Language.IsUFormula.isSemiformula {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {n k r v : V} : L.IsSemiformula n (qqRel k r v) ↔ L.Rel k r ∧ L.IsSemitermVec k n v

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem LO.Arith.Language.IsSemiformula.case {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → Prop} {n p : V} (hp : L.IsSemiformula n p) (hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec 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), L.IsSemiformula n p → L.IsSemiformula n q → P n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P n (qqEx p)) : P n p

theorem LO.Arith.Language.IsSemiformula.induction_sigma1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → Prop} (hP : FirstOrder.Arith.Sg1-Relation P) (hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec 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), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (qqEx p)) {n p : V} : L.IsSemiformula n p → P n p

theorem LO.Arith.Language.IsSemiformula.induction_pi1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {P : V → V → Prop} (hP : FirstOrder.Arith.Pg1-Relation P) (hrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec k n v → P n (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec 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), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (qqEx p)) {n p : V} : L.IsSemiformula n p → P n p

theorem LO.Arith.Language.IsSemiformula.induction1 {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (Γ : 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 (qqRel k r v)) (hnrel : ∀ (n k r v : V), L.Rel k r → L.IsSemitermVec 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), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (qqAnd p q)) (hor : ∀ (n p q : V), L.IsSemiformula n p → L.IsSemiformula n q → P n p → P n q → P n (qqOr p q)) (hall : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (qqAll p)) (hex : ∀ (n p : V), L.IsSemiformula (n + 1) p → P (n + 1) p → P n (qqEx p)) {n p : V} : L.IsSemiformula n p → P n p

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

@[simp]

theorem LO.Arith.Language.IsSemiformula.not_zero {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : 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} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] {β : Blueprint pL} {c : Construction V L β} {P : V → V → V → V → Prop} (hP : FirstOrder.Arith.Sg1-Relation₄ P) (hRel : ∀ (n param k R v : V), L.Rel k R → L.IsSemitermVec k n v → P param n (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 (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), 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 (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 (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 (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 (qqEx p) (c.ex param p (c.result (c.exChanges param) p))) {param n p : V} : L.IsSemiformula n p → P param n p (c.result param p)