Documentation

Mathlib.ModelTheory.Order

Ordered First-Ordered Structures #

This file defines ordered first-order languages and structures, as well as their theories.

Main Definitions #

Main Results #

The type of relations for the language of orders, consisting of a single binary relation le.

Equations
  • FirstOrder.Language.instDecidableEqOrderRel = FirstOrder.Language.decEqorderRel✝

The relational language consisting of a single relation representing .

Equations
@[simp]

A language is ordered if it has a symbol representing .

  • leSymb : L.Relations 2

    The relation symbol representing .

Instances
    theorem FirstOrder.Language.order.relation_eq_leSymb (R : FirstOrder.Language.order.Relations 2) :
    R = FirstOrder.Language.leSymb
    def FirstOrder.Language.Term.le {L : FirstOrder.Language} {α : Type w} {n : } [L.IsOrdered] (t₁ : L.Term (α Fin n)) (t₂ : L.Term (α Fin n)) :
    L.BoundedFormula α n

    Joins two terms t₁, t₂ in a formula representing t₁ ≤ t₂.

    Equations
    • t₁.le t₂ = FirstOrder.Language.leSymb.boundedFormula₂ t₁ t₂
    def FirstOrder.Language.Term.lt {L : FirstOrder.Language} {α : Type w} {n : } [L.IsOrdered] (t₁ : L.Term (α Fin n)) (t₂ : L.Term (α Fin n)) :
    L.BoundedFormula α n

    Joins two terms t₁, t₂ in a formula representing t₁ < t₂.

    Equations
    • t₁.lt t₂ = t₁.le t₂ (t₂.le t₁).not

    The language homomorphism sending the unique symbol of Language.order to in an ordered language.

    Equations
    • One or more equations did not get rendered due to their size.
    @[simp]
    theorem FirstOrder.Language.orderLHom_onFunction (L : FirstOrder.Language) [L.IsOrdered] {n : } (a : FirstOrder.Language.order.Functions n) :
    L.orderLHom.onFunction a = isEmptyElim a
    @[simp]
    theorem FirstOrder.Language.orderLHom_onRelation (L : FirstOrder.Language) [L.IsOrdered] :
    ∀ (x : ) (x_1 : FirstOrder.Language.order.Relations x), L.orderLHom.onRelation x_1 = match x, x_1 with | .(2), FirstOrder.Language.orderRel.le => FirstOrder.Language.leSymb
    @[simp]
    theorem FirstOrder.Language.orderLHom_leSymb (L : FirstOrder.Language) [L.IsOrdered] :
    L.orderLHom.onRelation FirstOrder.Language.leSymb = FirstOrder.Language.leSymb

    The theory of preorders.

    Equations
    • L.preorderTheory = {FirstOrder.Language.leSymb.reflexive, FirstOrder.Language.leSymb.transitive}
    instance FirstOrder.Language.instIsUniversalPreorderTheory (L : FirstOrder.Language) [L.IsOrdered] :
    L.preorderTheory.IsUniversal
    Equations
    • =

    The theory of partial orders.

    Equations
    • L.partialOrderTheory = insert FirstOrder.Language.leSymb.antisymmetric L.preorderTheory
    instance FirstOrder.Language.instIsUniversalPartialOrderTheory (L : FirstOrder.Language) [L.IsOrdered] :
    L.partialOrderTheory.IsUniversal
    Equations
    • =

    The theory of linear orders.

    Equations
    • L.linearOrderTheory = insert FirstOrder.Language.leSymb.total L.partialOrderTheory
    instance FirstOrder.Language.instIsUniversalLinearOrderTheory (L : FirstOrder.Language) [L.IsOrdered] :
    L.linearOrderTheory.IsUniversal
    Equations
    • =

    A sentence indicating that an order has no top element: x,y,¬yx.

    Equations
    • L.noTopOrderSentence = (((FirstOrder.Language.var Sum.inr) 1).le ((FirstOrder.Language.var Sum.inr) 0)).not.ex.all

    A sentence indicating that an order has no bottom element: x,y,¬xy.

    Equations
    • L.noBotOrderSentence = (((FirstOrder.Language.var Sum.inr) 0).le ((FirstOrder.Language.var Sum.inr) 1)).not.ex.all

    A sentence indicating that an order is dense: x,y,x<yz,x<zz<y.

    Equations
    • One or more equations did not get rendered due to their size.
    def FirstOrder.Language.dlo (L : FirstOrder.Language) [L.IsOrdered] :
    L.Theory

    The theory of dense linear orders without endpoints.

    Equations
    • L.dlo = L.linearOrderTheory {L.noTopOrderSentence, L.noBotOrderSentence, L.denselyOrderedSentence}
    instance FirstOrder.Language.instModelLinearOrderTheoryOfDlo (L : FirstOrder.Language) {M : Type w'} [L.IsOrdered] [L.Structure M] [h : M L.dlo] :
    M L.linearOrderTheory
    Equations
    • =
    instance FirstOrder.Language.instModelPartialOrderTheoryOfLinearOrderTheory (L : FirstOrder.Language) {M : Type w'} [L.IsOrdered] [L.Structure M] [h : M L.linearOrderTheory] :
    M L.partialOrderTheory
    Equations
    • =
    instance FirstOrder.Language.instModelPreorderTheoryOfPartialOrderTheory (L : FirstOrder.Language) {M : Type w'} [L.IsOrdered] [L.Structure M] [h : M L.partialOrderTheory] :
    M L.preorderTheory
    Equations
    • =
    Equations
    • FirstOrder.Language.sum.instIsOrdered = { leSymb := Sum.inr FirstOrder.Language.leSymb }

    Any linearly-ordered type is naturally a structure in the language Language.order. This is not an instance, because sometimes the Language.order.Structure is defined first.

    Equations
    • One or more equations did not get rendered due to their size.
    class FirstOrder.Language.OrderedStructure (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [LE M] [L.Structure M] :

    A structure is ordered if its language has a symbol whose interpretation is .

    Instances
      @[simp]
      theorem FirstOrder.Language.OrderedStructure.relMap_leSymb {L : FirstOrder.Language} {M : Type w'} :
      ∀ {inst : L.IsOrdered} {inst_1 : LE M} {inst_2 : L.Structure M} [self : L.OrderedStructure M] (x : Fin 2M), FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb x x 0 x 1
      instance FirstOrder.Language.instOrderedStructureOfOrderOfIsExpansionOnOrderLHom {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] [L.orderLHom.IsExpansionOn M] :
      L.OrderedStructure M
      Equations
      • =
      instance FirstOrder.Language.instIsExpansionOnOrderLHomOfOrderedStructureOrder {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] :
      L.orderLHom.IsExpansionOn M
      Equations
      • =
      instance FirstOrder.Language.instOrderedStructureSubtypeMemSubstructure {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] (S : L.Substructure M) :
      L.OrderedStructure S
      Equations
      • =
      @[simp]
      theorem FirstOrder.Language.Term.realize_le {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : } [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] {t₁ : L.Term (α Fin n)} {t₂ : L.Term (α Fin n)} {v : αM} {xs : Fin nM} :
      theorem FirstOrder.Language.realize_noTopOrder_iff {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] :
      M L.noTopOrderSentence NoTopOrder M
      theorem FirstOrder.Language.realize_noBotOrder_iff {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] :
      M L.noBotOrderSentence NoBotOrder M
      @[simp]
      theorem FirstOrder.Language.realize_noTopOrder (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] [h : NoTopOrder M] :
      M L.noTopOrderSentence
      @[simp]
      theorem FirstOrder.Language.realize_noBotOrder (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] [h : NoBotOrder M] :
      M L.noBotOrderSentence
      theorem FirstOrder.Language.noTopOrder_of_dlo (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] [M L.dlo] :
      theorem FirstOrder.Language.noBotOrder_of_dlo (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] [M L.dlo] :
      @[simp]
      theorem FirstOrder.Language.orderedStructure_iff {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [FirstOrder.Language.order.Structure M] [FirstOrder.Language.order.OrderedStructure M] :
      L.OrderedStructure M L.orderLHom.IsExpansionOn M
      instance FirstOrder.Language.model_preorder {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] :
      M L.preorderTheory
      Equations
      • =
      @[simp]
      theorem FirstOrder.Language.Term.realize_lt {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : } [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] {t₁ : L.Term (α Fin n)} {t₂ : L.Term (α Fin n)} {v : αM} {xs : Fin nM} :
      (t₁.lt t₂).Realize v xs FirstOrder.Language.Term.realize (Sum.elim v xs) t₁ < FirstOrder.Language.Term.realize (Sum.elim v xs) t₂
      theorem FirstOrder.Language.realize_denselyOrdered_iff {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] :
      M L.denselyOrderedSentence DenselyOrdered M
      @[simp]
      theorem FirstOrder.Language.realize_denselyOrdered {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] [h : DenselyOrdered M] :
      M L.denselyOrderedSentence
      theorem FirstOrder.Language.denselyOrdered_of_dlo (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] [M L.dlo] :
      instance FirstOrder.Language.model_partialOrder {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [PartialOrder M] [L.OrderedStructure M] :
      M L.partialOrderTheory
      Equations
      • =
      instance FirstOrder.Language.model_linearOrder {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LinearOrder M] [L.OrderedStructure M] :
      M L.linearOrderTheory
      Equations
      • =
      instance FirstOrder.Language.model_dlo {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LinearOrder M] [L.OrderedStructure M] [DenselyOrdered M] [NoTopOrder M] [NoBotOrder M] :
      M L.dlo
      Equations
      • =
      def FirstOrder.Language.leOfStructure (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] :
      LE M

      Any structure in an ordered language can be ordered correspondingly.

      Equations
      instance FirstOrder.Language.instOrderedStructure (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] :
      L.OrderedStructure M
      Equations
      • =
      def FirstOrder.Language.decidableLEOfStructure (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [h : DecidableRel fun (a b : M) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b]] :
      DecidableRel fun (x1 x2 : M) => x1 x2

      The order structure on an ordered language is decidable.

      Equations
      • L.decidableLEOfStructure M = h
      def FirstOrder.Language.preorderOfModels (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [h : M L.preorderTheory] :

      Any model of a theory of preorders is a preorder.

      Equations
      def FirstOrder.Language.partialOrderOfModels (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [h : M L.partialOrderTheory] :

      Any model of a theory of partial orders is a partial order.

      Equations
      def FirstOrder.Language.linearOrderOfModels (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [h : M L.linearOrderTheory] [DecidableRel fun (a b : M) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b]] :

      Any model of a theory of linear orders is a linear order.

      Equations
      • L.linearOrderOfModels M = LinearOrder.mk inferInstance decidableEqOfDecidableLE decidableLTOfDecidableLE
      instance FirstOrder.Language.order.instHomClassOfOrderHomClass {M : Type w'} [FirstOrder.Language.order.Structure M] [LE M] [FirstOrder.Language.order.OrderedStructure M] {N : Type u_1} [FirstOrder.Language.order.Structure N] [LE N] [FirstOrder.Language.order.OrderedStructure N] {F : Type u_2} [FunLike F M N] [OrderHomClass F M N] :
      Equations
      • =
      instance FirstOrder.Language.order.instStrongHomClassOrderEmbedding {M : Type w'} [FirstOrder.Language.order.Structure M] [LE M] [FirstOrder.Language.order.OrderedStructure M] {N : Type u_1} [FirstOrder.Language.order.Structure N] [LE N] [FirstOrder.Language.order.OrderedStructure N] :
      FirstOrder.Language.order.StrongHomClass (M ↪o N) M N
      Equations
      • =
      instance FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass {M : Type w'} [FirstOrder.Language.order.Structure M] [LE M] [FirstOrder.Language.order.OrderedStructure M] {N : Type u_1} [FirstOrder.Language.order.Structure N] [LE N] [FirstOrder.Language.order.OrderedStructure N] {F : Type u_2} [EquivLike F M N] [OrderIsoClass F M N] :
      FirstOrder.Language.order.StrongHomClass F M N
      Equations
      • =
      theorem FirstOrder.Language.HomClass.monotone {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] {N : Type u_1} [L.Structure N] {F : Type u_2} [FunLike F M N] [L.HomClass F M N] [Preorder M] [L.OrderedStructure M] [Preorder N] [L.OrderedStructure N] (f : F) :
      theorem FirstOrder.Language.HomClass.strictMono {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] {N : Type u_1} [L.Structure N] {F : Type u_2} [FunLike F M N] [L.HomClass F M N] [EmbeddingLike F M N] [PartialOrder M] [L.OrderedStructure M] [PartialOrder N] [L.OrderedStructure N] (f : F) :
      theorem FirstOrder.Language.StrongHomClass.toOrderIsoClass (L : FirstOrder.Language) [L.IsOrdered] (M : Type u_1) [L.Structure M] [LE M] [L.OrderedStructure M] (N : Type u_2) [L.Structure N] [LE N] [L.OrderedStructure N] (F : Type u_3) [EquivLike F M N] [L.StrongHomClass F M N] :

      This is not an instance because it would form a loop with FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass. As both types are Props, it would only cause a slowdown.

      Any countable nonempty model of the theory of dense linear orders is a Fraïssé limit of the class of finite models of the theory of linear orders.

      The class of finite models of the theory of linear orders is Fraïssé.

      The theory of dense linear orders is ℵ₀-categorical.

      The theory of dense linear orders is ℵ₀-complete.