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 : Language} {M : Type u_1} [L.Structure M] (S : L.Substructure 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

• S.IsElementary = ∀ ⦃n : ℕ⦄ (φ : L.Formula (Fin n)) (x : Fin n → ↥S), φ.Realize (Subtype.val ∘ x) ↔ φ.Realize x

structure FirstOrder.Language.ElementarySubstructure (L : 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

  The underlying substructure

• isElementary' : (↑self).IsElementary

@[implicit_reducible]

instance FirstOrder.Language.ElementarySubstructure.instCoe {L : 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 }

@[implicit_reducible]

instance FirstOrder.Language.ElementarySubstructure.instSetLike {L : 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' := ⋯ }

@[implicit_reducible]

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

Equations

• FirstOrder.Language.ElementarySubstructure.instPartialOrder = PartialOrder.ofSetLike (L.ElementarySubstructure M) M

@[implicit_reducible]

instance FirstOrder.Language.ElementarySubstructure.inducedStructure {L : 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 : Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) : (↑S).IsElementary

def FirstOrder.Language.ElementarySubstructure.subtype {L : 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' := ⋯ }

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.subtype_apply {L : Language} {M : Type u_1} [L.Structure M] {S : L.ElementarySubstructure M} {x : ↥S} : S.subtype x = ↑x

theorem FirstOrder.Language.ElementarySubstructure.subtype_injective {L : Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) : Function.Injective ⇑S.subtype

@[simp]

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

@[implicit_reducible]

instance FirstOrder.Language.ElementarySubstructure.instTop {L : 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' := ⋯ } }

@[implicit_reducible]

instance FirstOrder.Language.ElementarySubstructure.instInhabited {L : 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 : Language} {M : Type u_1} [L.Structure M] (x : M) : x ∈ ⊤

@[simp]

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

@[simp]

theorem FirstOrder.Language.ElementarySubstructure.realize_sentence {L : 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 : 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 : Language} {M : Type u_1} [L.Structure M] {T : L.Theory} [h : M ⊨ T] {S : L.ElementarySubstructure M} : ↥S ⊨ T

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

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

theorem FirstOrder.Language.Substructure.isElementary_of_exists {L : Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) (htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (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.

def FirstOrder.Language.Substructure.toElementarySubstructure {L : Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) (htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (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' := ⋯ }

@[simp]

theorem FirstOrder.Language.Substructure.toElementarySubstructure_toSubstructure {L : Language} {M : Type u_1} [L.Structure M] (S : L.Substructure M) (htv : ∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → ↥S) (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.MeetsDefinable {L : Language} {M : Type u_1} [L.Structure M] (A : Set M) : Prop

A set meets definable sets if it meets every nonempty definable subset.

Equations

• FirstOrder.Language.MeetsDefinable A = ∀ (D : Set M), D.Nonempty → A.Definable₁ L D → (D ∩ A).Nonempty

theorem FirstOrder.Language.MeetsDefinable.closure_eq_self {L : Language} {M : Type u_1} [L.Structure M] {A : Set M} (hA : MeetsDefinable A) : ↑((Substructure.closure L).toFun A) = A

The closure of a set meeting definable sets is equal to itself.

theorem FirstOrder.Language.MeetsDefinable.isElementary_closure {L : Language} {M : Type u_1} [L.Structure M] {A : Set M} (hA : MeetsDefinable A) : ((Substructure.closure L).toFun A).IsElementary

The closure of a set meeting definable sets is an elementary substructure.

def FirstOrder.Language.MeetsDefinable.toElementarySubstructure {L : Language} {M : Type u_1} [L.Structure M] {A : Set M} (hA : MeetsDefinable A) : L.ElementarySubstructure M

Bundles the closure of a set meeting definable sets as an elementary substructure.

Equations

• hA.toElementarySubstructure = { toSubstructure := (FirstOrder.Language.Substructure.closure L).toFun A, isElementary' := ⋯ }

theorem FirstOrder.Language.ElementarySubstructure.meetsDefinable {L : Language} {M : Type u_1} [L.Structure M] (S : L.ElementarySubstructure M) : MeetsDefinable ↑S

An elementary substructure, regarded as a subset of the ambient structure, meets definable sets.