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} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) : Prop

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

Equations

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

structure FirstOrder.Language.ElementarySubstructure (L : FirstOrder.Language) (M : Type u_1) [FirstOrder.Language.Structure L 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 : FirstOrder.Language.Substructure L M
• isElementary' : FirstOrder.Language.Substructure.IsElementary ↑self

instance FirstOrder.Language.ElementarySubstructure.instCoe {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Coe (FirstOrder.Language.ElementarySubstructure L M) (FirstOrder.Language.Substructure L M)

Equations

• FirstOrder.Language.ElementarySubstructure.instCoe = { coe := FirstOrder.Language.ElementarySubstructure.toSubstructure }

instance FirstOrder.Language.ElementarySubstructure.instSetLike {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : SetLike (FirstOrder.Language.ElementarySubstructure L M) M

Equations

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

instance FirstOrder.Language.ElementarySubstructure.inducedStructure {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.Structure L ↥S

Equations

• FirstOrder.Language.ElementarySubstructure.inducedStructure S = FirstOrder.Language.Substructure.inducedStructure

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.isElementary {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.Substructure.IsElementary ↑S

def FirstOrder.Language.ElementarySubstructure.subtype {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.ElementaryEmbedding L (↥S) M

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

Equations

• FirstOrder.Language.ElementarySubstructure.subtype S = FirstOrder.Language.ElementaryEmbedding.mk Subtype.val

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.coeSubtype {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {S : FirstOrder.Language.ElementarySubstructure L M} : ⇑(FirstOrder.Language.ElementarySubstructure.subtype S) = Subtype.val

instance FirstOrder.Language.ElementarySubstructure.instTop {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Top (FirstOrder.Language.ElementarySubstructure L M)

The substructure M of the structure M is elementary.

Equations

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

instance FirstOrder.Language.ElementarySubstructure.instInhabited {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : Inhabited (FirstOrder.Language.ElementarySubstructure L M)

Equations

• FirstOrder.Language.ElementarySubstructure.instInhabited = { default := ⊤ }

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.mem_top {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (x : M) : x ∈ ⊤

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.coe_top {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] : ↑⊤ = Set.univ

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.realize_sentence {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) (φ : FirstOrder.Language.Sentence L) : ↥S ⊨ φ ↔ M ⊨ φ

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.theory_model_iff {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) (T : FirstOrder.Language.Theory L) : ↥S ⊨ T ↔ M ⊨ T

instance FirstOrder.Language.ElementarySubstructure.theory_model {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] {T : FirstOrder.Language.Theory L} [h : M ⊨ T] {S : FirstOrder.Language.ElementarySubstructure L M} : ↥S ⊨ T

Equations

• (_ : ↥S ⊨ T) = (_ : ↥S ⊨ T)

instance FirstOrder.Language.ElementarySubstructure.instNonempty {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] [Nonempty M] {S : FirstOrder.Language.ElementarySubstructure L M} : Nonempty ↥S

Equations

• (_ : Nonempty ↥S) = (_ : Nonempty ↥S)

theorem FirstOrder.Language.ElementarySubstructure.elementarilyEquivalent {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.ElementarySubstructure L M) : FirstOrder.Language.ElementarilyEquivalent L (↥S) M

theorem FirstOrder.Language.Substructure.isElementary_of_exists {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → ↥S) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) → ∃ (b : ↥S), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)) : FirstOrder.Language.Substructure.IsElementary S

The Tarski-Vaught test for elementarity of a substructure.

@[simp]

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

def FirstOrder.Language.Substructure.toElementarySubstructure {L : FirstOrder.Language} {M : Type u_1} [FirstOrder.Language.Structure L M] (S : FirstOrder.Language.Substructure L M) (htv : ∀ (n : ℕ) (φ : FirstOrder.Language.BoundedFormula L Empty (n + 1)) (x : Fin n → ↥S) (a : M), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) a) → ∃ (b : ↥S), FirstOrder.Language.BoundedFormula.Realize φ default (Fin.snoc (Subtype.val ∘ x) ↑b)) : FirstOrder.Language.ElementarySubstructure L M

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

Equations

• FirstOrder.Language.Substructure.toElementarySubstructure S htv = { toSubstructure := S, isElementary' := (_ : FirstOrder.Language.Substructure.IsElementary S) }