structure LO.FirstOrder.Arith.LDef.TDef (pL : LO.FirstOrder.Arith.LDef) : Type

• ch : 𝚫₁.Semisentence 1

structure LO.Arith.Language.Theory {V : Type u_1} [LO.ORingStruc V] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : Type u_1

• set : Set V

instance LO.Arith.instMembershipTheory {V : Type u_1} [LO.ORingStruc V] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : Membership V L.Theory

Equations

• LO.Arith.instMembershipTheory L = { mem := fun (x : V) (T : L.Theory) => x ∈ T.set }

instance LO.Arith.instHasSubsetTheory {V : Type u_1} [LO.ORingStruc V] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] : HasSubset L.Theory

Equations

• LO.Arith.instHasSubsetTheory L = { Subset := fun (T U : L.Theory) => T.set ⊆ U.set }

theorem LO.Arith.Language.Theory.mem_def {V : Type u_1} [LO.ORingStruc V] (L : LO.Arith.Language V) {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {p : V} : p ∈ T ↔ p ∈ T.set

class LO.Arith.Language.Theory.Defined {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) (pT : outParam pL.TDef) : Type

• defined : 𝚫₁-Predicate fun (x : V) => x ∈ T.set via pT.ch

theorem LO.Arith.Language.Theory.Defined.defined {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] {T : L.Theory} {pT : outParam pL.TDef} [self : T.Defined pT] : 𝚫₁-Predicate fun (x : V) => x ∈ T.set via pT.ch

instance LO.Arith.Language.Theory.mem_definable {V : Type u_1} [LO.ORingStruc V] {L : LO.Arith.Language V} {pL : LO.FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) {pT : pL.TDef} [T.Defined pT] : 𝚫₁-Predicate fun (x : V) => x ∈ T

Equations

• ⋯ = ⋯