CodedTheory

@[simp]

theorem LO.FirstOrder.Theory.mem_add_iff {L : Language} {T U : Theory L} {φ : SyntacticFormula L} : φ ∈ T + U ↔ φ ∈ T ∨ φ ∈ U

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

Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

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

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

Imported declaration from the Incompleteness formalization.

Equations

• T.tDef = d.toTDef T

@[simp]

theorem LO.FirstOrder.Theory.Delta1Definable.mem_iff' {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {φ : SyntacticFormula L} (T : Theory L) [d : T.Delta1Definable] : ℕ ⊧/![⌜φ⌝] (Arith.HierarchySymbol.Semiformula.val T.tDef.ch) ↔ φ ∈ 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

Imported declaration from the Incompleteness formalization.

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 ⊧ₘ* 𝐈Sg1] (T : Theory L) [T.Delta1Definable] : Arith.HierarchySymbol.Semiformula.ProperOn V T.tDef.ch

@[simp]

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

instance LO.FirstOrder.Theory.tDef_defined {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] {V : Type u_1} [ORingStruc V] [V ⊧ₘ* 𝐈Sg1] {T : Theory L} [T.Delta1Definable] : (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 ⊧ₘ* 𝐈Sg1] (T : Theory L) [T.Delta1Definable] : (L.codeIn V).TTheory

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.tCodeIn V T = { thy := LO.FirstOrder.Theory.codeIn V T, pthy := T.tDef, defined := ⋯ }

@[reducible]

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

Imported declaration from the Incompleteness formalization.

Equations

• dT.add dU = { ch := T.tDef.ch ⋎ U.tDef.ch, mem_iff := ⋯, isDelta1 := ⋯ }

@[reducible]

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

Imported declaration from the Incompleteness formalization.

Equations

• dT.ofEq h = { toTDef := dT.toTDef T, mem_iff := ⋯, isDelta1 := ⋯ }

theorem 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)

Imported declaration from the Incompleteness formalization.

theorem 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)

Imported declaration from the Incompleteness formalization.

@[implicit_reducible]

instance LO.FirstOrder.Theory.Delta1Definable.empty {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] : ∅.Delta1Definable

Equations

• LO.FirstOrder.Theory.Delta1Definable.empty = { ch := ⊥, mem_iff := ⋯, isDelta1 := LO.FirstOrder.Theory.Delta1Definable.empty._proof_2 }

memo: This noncomputable is not essetial.

@[reducible]

noncomputable def LO.FirstOrder.Theory.Delta1Definable.singleton {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (φ : SyntacticFormula L) : {φ}.Delta1Definable

Imported declaration from the Incompleteness formalization.

Equations

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

@[simp]

theorem LO.FirstOrder.Theory.Delta1Definable.singleton_toTDef_ch_val {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (φ : SyntacticFormula L) : Arith.HierarchySymbol.Semiformula.val ((singleton φ).toTDef {φ}).ch = (“!!(Semiterm.bvar 0) = !!↑⌜φ⌝”)

@[reducible]

noncomputable def LO.FirstOrder.Theory.Delta1Definable.ofList {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (l : List (SyntacticFormula L)) : Delta1Definable {φ : SyntacticFormula L | φ ∈ l}

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Delta1Definable.ofList [] = LO.FirstOrder.Theory.Delta1Definable.empty.ofEq ⋯
• LO.FirstOrder.Theory.Delta1Definable.ofList (φ :: l_2) = ((LO.FirstOrder.Theory.Delta1Definable.singleton φ).add (LO.FirstOrder.Theory.Delta1Definable.ofList l_2)).ofEq ⋯

@[reducible]

noncomputable def LO.FirstOrder.Theory.Delta1Definable.ofFinite {L : Language} [(k : ℕ) → Encodable (L.Func k)] [(k : ℕ) → Encodable (L.Rel k)] [Arith.DefinableLanguage L] (T : Theory L) (h : Set.Finite T) : T.Delta1Definable

Imported declaration from the Incompleteness formalization.

Equations

• LO.FirstOrder.Theory.Delta1Definable.ofFinite T h = (LO.FirstOrder.Theory.Delta1Definable.ofList h.toFinset.toList).ofEq ⋯