Documentation

Mathlib.ModelTheory.ElementarySubstructures

Elementary Substructures #

Main Definitions #

Main Results #

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] [Nonempty 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