Thy

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

Imported declaration from the Incompleteness formalization.

• ch : Dlt1.Semisentence 1

  Imported declaration from the Incompleteness formalization.

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

Imported declaration from the Incompleteness formalization.

• set : Set V

  Imported declaration from the Incompleteness formalization.

@[implicit_reducible]

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 }

@[implicit_reducible]

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

Imported declaration from the Incompleteness formalization.

• defined : FirstOrder.Arith.Dlt1-Predicate fun (x : V) => x ∈ T.set via pT.ch

theorem LO.Arith.Language.Theory.mem_defined {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] : FirstOrder.Arith.Dlt1-Predicate fun (x : V) => x ∈ T via pT.ch

Imported declaration from the Incompleteness formalization.

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] : FirstOrder.Arith.Dlt1-Predicate fun (x : V) => x ∈ T