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

• ch : 𝚫₁.Semisentence 1

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

• set : Set V

Instances For

• LO.Arith.instHasSubsetTheory
• LO.Arith.instMembershipTheory

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

Equations

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

instance LO.Arith.instHasSubsetTheory {V : Type u_1} [ORingStruc V] (L : Arith.Language V) {pL : 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} [ORingStruc V] (L : Arith.Language V) {pL : 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} [ORingStruc V] {L : Arith.Language V} {pL : FirstOrder.Arith.LDef} [L.Defined pL] (T : L.Theory) (pT : outParam pL.TDef) : Prop

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

Instances

• LO.Arith.instDefinedThyPthy
• LO.Arith.tDef_defined

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