def LO.FirstOrder.Semiformula.curve {L : Language} {M : Type u_1} [Structure L M] (σ : Semisentence L 1) : Set M

Equations

• LO.FirstOrder.Semiformula.curve σ = {x : M | M ⊧/![x] σ}

theorem LO.FirstOrder.Semiformula.curve_mem_left {L : Language} {M : Type u_1} [Structure L M] {σ π : Semisentence L 1} {x : M} (hx : x ∈ curve σ) : x ∈ curve (σ ⋎ π)

theorem LO.FirstOrder.Semiformula.curve_mem_right {L : Language} {M : Type u_1} [Structure L M] {σ π : Semisentence L 1} {x : M} (hx : x ∈ curve π) : x ∈ curve (σ ⋎ π)

class LO.FirstOrder.Theory.Delta1Definable {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (T : Theory L) extends L.lDef.TDef : Type

• ch : 𝚫₁.Semisentence 1
• mem_iff {p : SyntacticFormula L} : p ∈ T ↔ ℕ ⊧/![⌜p⌝] (Arith.HierarchySymbol.Semiformula.val (toTDef T).ch)
• isDelta1 : Arith.HierarchySymbol.Semiformula.ProvablyProperOn (toTDef T).ch 𝐈𝚺₁

def LO.FirstOrder.Theory.tDef {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (T : Theory L) [d : T.Delta1Definable] : L.lDef.TDef

Equations

• T.tDef = LO.FirstOrder.Theory.Delta1Definable.toTDef T

def LO.FirstOrder.Theory.codeIn {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (V : Type u_1) [ORingStruc V] (T : Theory L) [T.Delta1Definable] : (L.codeIn V).Theory

Equations

• LO.FirstOrder.Theory.codeIn V T = { set := (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val T.tDef.ch).curve }

@[simp]

theorem LO.FirstOrder.Theory.properOn {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : Theory L) [T.Delta1Definable] : Arith.HierarchySymbol.Semiformula.ProperOn V T.tDef.ch

theorem LO.Arith.Language.Theory.codeIn_iff {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] {T : FirstOrder.Theory L} [T.Delta1Definable] {x : V} : x ∈ FirstOrder.Theory.codeIn V T ↔ V ⊧/![x] (FirstOrder.Arith.HierarchySymbol.Semiformula.val T.tDef.ch)

theorem LO.Arith.mem_coded_theory_iff {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : FirstOrder.Theory L} [T.Delta1Definable] {σ : FirstOrder.SyntacticFormula L} : ⌜σ⌝ ∈ FirstOrder.Theory.codeIn V T ↔ σ ∈ T

instance LO.Arith.tDef_defined {L : FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [DefinableLanguage L] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] {T : FirstOrder.Theory L} [T.Delta1Definable] : (FirstOrder.Theory.codeIn V T).Defined T.tDef

def LO.FirstOrder.Theory.tCodeIn {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (V : Type u_1) [ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : Theory L) [T.Delta1Definable] : (L.codeIn V).TTheory

Equations

• LO.FirstOrder.Theory.tCodeIn V T = LO.Arith.Language.TTheory.mk (LO.FirstOrder.Theory.codeIn V T) T.tDef

def LO.FirstOrder.Theory.Delta1Definable.add {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {T U : Theory L} (dT : T.Delta1Definable) (dU : U.Delta1Definable) : (T + U).Delta1Definable

Equations

• dT.add dU = { ch := LO.FirstOrder.Arith.HierarchySymbol.Semiformula.or T.tDef.ch U.tDef.ch, mem_iff := ⋯, isDelta1 := ⋯ }

def LO.FirstOrder.Theory.Delta1Definable.ofEq {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {T U : Theory L} (dT : T.Delta1Definable) (h : T = U) : U.Delta1Definable

Equations

• dT.ofEq h = { ch := (LO.FirstOrder.Theory.Delta1Definable.toTDef T).ch, mem_iff := ⋯, isDelta1 := ⋯ }

def LO.FirstOrder.Theory.Delta1Definable.add_subset_left {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {V : Type u_1} [ORingStruc V] {T U : Theory L} (dT : T.Delta1Definable) (dU : U.Delta1Definable) : codeIn V T ⊆ codeIn V (T + U)

Equations

• ⋯ = ⋯

def LO.FirstOrder.Theory.Delta1Definable.add_subset_right {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {V : Type u_1} [ORingStruc V] {T U : Theory L} (dT : T.Delta1Definable) (dU : U.Delta1Definable) : codeIn V U ⊆ codeIn V (T + U)

Equations

• ⋯ = ⋯