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.

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

    The relational language consisting of a single relation representing .

    Equations
    Instances For
      @[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₂
        Instances For
          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
          Instances For

            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.
            Instances For
              @[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}
              Instances For
                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
                Instances For
                  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
                  Instances For
                    instance FirstOrder.Language.instIsUniversalLinearOrderTheory (L : FirstOrder.Language) [L.IsOrdered] :
                    L.linearOrderTheory.IsUniversal
                    Equations
                    • =

                    A sentence indicating that an order has no top element: $\forall x, \exists y, \neg y \le x$.

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

                      A sentence indicating that an order has no bottom element: $\forall x, \exists y, \neg x \le y$.

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

                        A sentence indicating that an order is dense: $\forall x, \forall y, x < y \to \exists z, x < z \wedge z < y$.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          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}
                          Instances For
                            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.
                            Instances For
                              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
                                Instances For
                                  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
                                  Instances For
                                    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
                                    Instances For
                                      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
                                      Instances For
                                        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
                                        Instances For
                                          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.