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

Equations

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

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

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

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

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

theorem LO.FirstOrder.Theory.Delta1Definable.mem_iff {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [self : T.Delta1Definable] {p : LO.FirstOrder.SyntacticFormula L} : p ∈ T ↔ ℕ ⊧/![⌜p⌝] (LO.FirstOrder.Arith.HierarchySymbol.Semiformula.val (LO.FirstOrder.Theory.Delta1Definable.toTDef T).ch)

theorem LO.FirstOrder.Theory.Delta1Definable.isDelta1 {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} [self : T.Delta1Definable] : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProvablyProperOn (LO.FirstOrder.Theory.Delta1Definable.toTDef T).ch 𝐈𝚺₁

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

Equations

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

def LO.FirstOrder.Theory.codeIn {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (V : Type u_1) [LO.ORingStruc V] (T : LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : LO.FirstOrder.Theory L) [T.Delta1Definable] : LO.FirstOrder.Arith.HierarchySymbol.Semiformula.ProperOn V T.tDef.ch

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

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

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

Equations

• LO.Arith.tDef_defined = { defined := ⋯ }

def LO.FirstOrder.Theory.tCodeIn {L : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] (V : Type u_1) [LO.ORingStruc V] [V ⊧ₘ* 𝐈𝚺₁] (T : LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.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 : LO.FirstOrder.Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [LO.Arith.DefinableLanguage L] {V : Type u_1} [LO.ORingStruc V] {T : LO.FirstOrder.Theory L} {U : LO.FirstOrder.Theory L} (dT : T.Delta1Definable) (dU : U.Delta1Definable) : LO.FirstOrder.Theory.codeIn V T ⊆ LO.FirstOrder.Theory.codeIn V (T + U)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯