# Elementary Substructures #

## Main Definitions #

• A FirstOrder.Language.ElementarySubstructure is a substructure where the realization of each formula agrees with the realization in the larger model.

## Main Results #

• The Tarski-Vaught Test for substructures: FirstOrder.Language.Substructure.isElementary_of_exists gives a simple criterion for a substructure to be elementary.
def FirstOrder.Language.Substructure.IsElementary {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) :

A substructure is elementary when every formula applied to a tuple in the substructure agrees with its value in the overall structure.

Equations
• S.IsElementary = ∀ ⦃n : ⦄ (φ : L.Formula (Fin n)) (x : Fin nS), φ.Realize (Subtype.val x) φ.Realize x
Instances For
structure FirstOrder.Language.ElementarySubstructure (L : FirstOrder.Language) (M : Type u_1) [L.Structure M] :
Type u_1

An elementary substructure is one in which every formula applied to a tuple in the substructure agrees with its value in the overall structure.

• toSubstructure : L.Substructure M
• isElementary' : (self).IsElementary
Instances For
theorem FirstOrder.Language.ElementarySubstructure.isElementary' {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (self : L.ElementarySubstructure M) :
(self).IsElementary
instance FirstOrder.Language.ElementarySubstructure.instCoe {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
Coe (L.ElementarySubstructure M) (L.Substructure M)
Equations
• FirstOrder.Language.ElementarySubstructure.instCoe = { coe := FirstOrder.Language.ElementarySubstructure.toSubstructure }
instance FirstOrder.Language.ElementarySubstructure.instSetLike {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
SetLike (L.ElementarySubstructure M) M
Equations
• FirstOrder.Language.ElementarySubstructure.instSetLike = { coe := fun (x : L.ElementarySubstructure M) => x, coe_injective' := }
instance FirstOrder.Language.ElementarySubstructure.inducedStructure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) :
L.Structure S
Equations
• S.inducedStructure = FirstOrder.Language.Substructure.inducedStructure
@[simp]
theorem FirstOrder.Language.ElementarySubstructure.isElementary {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) :
(S).IsElementary
def FirstOrder.Language.ElementarySubstructure.subtype {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) :
L.ElementaryEmbedding (S) M

The natural embedding of an L.Substructure of M into M.

Equations
• S.subtype = { toFun := Subtype.val, map_formula' := }
Instances For
@[simp]
theorem FirstOrder.Language.ElementarySubstructure.coeSubtype {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {S : L.ElementarySubstructure M} :
S.subtype = Subtype.val
instance FirstOrder.Language.ElementarySubstructure.instTop {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
Top (L.ElementarySubstructure M)

The substructure M of the structure M is elementary.

Equations
• FirstOrder.Language.ElementarySubstructure.instTop = { top := { toSubstructure := , isElementary' := } }
instance FirstOrder.Language.ElementarySubstructure.instInhabited {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
Inhabited (L.ElementarySubstructure M)
Equations
• FirstOrder.Language.ElementarySubstructure.instInhabited = { default := }
@[simp]
theorem FirstOrder.Language.ElementarySubstructure.mem_top {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (x : M) :
@[simp]
theorem FirstOrder.Language.ElementarySubstructure.coe_top {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] :
= Set.univ
@[simp]
theorem FirstOrder.Language.ElementarySubstructure.realize_sentence {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) (φ : L.Sentence) :
S φ M φ
@[simp]
theorem FirstOrder.Language.ElementarySubstructure.theory_model_iff {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) (T : L.Theory) :
S T M T
instance FirstOrder.Language.ElementarySubstructure.theory_model {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] {T : L.Theory} [h : M T] {S : L.ElementarySubstructure M} :
S T
Equations
• =
instance FirstOrder.Language.ElementarySubstructure.instNonempty {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] [] {S : L.ElementarySubstructure M} :
Equations
• =
theorem FirstOrder.Language.ElementarySubstructure.elementarilyEquivalent {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) :
L.ElementarilyEquivalent (S) M
theorem FirstOrder.Language.Substructure.isElementary_of_exists {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) (htv : ∀ (n : ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin nS) (a : M), φ.Realize default (Fin.snoc (Subtype.val x) a)∃ (b : S), φ.Realize default (Fin.snoc (Subtype.val x) b)) :
S.IsElementary

The Tarski-Vaught test for elementarity of a substructure.

@[simp]
theorem FirstOrder.Language.Substructure.toElementarySubstructure_toSubstructure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) (htv : ∀ (n : ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin nS) (a : M), φ.Realize default (Fin.snoc (Subtype.val x) a)∃ (b : S), φ.Realize default (Fin.snoc (Subtype.val x) b)) :
(S.toElementarySubstructure htv) = S
def FirstOrder.Language.Substructure.toElementarySubstructure {L : FirstOrder.Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) (htv : ∀ (n : ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin nS) (a : M), φ.Realize default (Fin.snoc (Subtype.val x) a)∃ (b : S), φ.Realize default (Fin.snoc (Subtype.val x) b)) :
L.ElementarySubstructure M

Bundles a substructure satisfying the Tarski-Vaught test as an elementary substructure.

Equations
• S.toElementarySubstructure htv = { toSubstructure := S, isElementary' := }
Instances For