Ordered First-Ordered Structures

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

Main Definitions

• FirstOrder.Language.order is the language consisting of a single relation representing ≤.
• FirstOrder.Language.IsOrdered points out a specific symbol in a language as representing ≤.
• FirstOrder.Language.OrderedStructure indicates that the ≤ symbol in an ordered language is interpreted as the actual relation ≤ in a particular structure.
• FirstOrder.Language.linearOrderTheory and similar define the theories of preorders, partial orders, and linear orders.
• FirstOrder.Language.dlo defines the theory of dense linear orders without endpoints, a particularly useful example in model theory.
• FirstOrder.Language.orderStructure is the structure on an ordered type, assigning the symbol representing ≤ to the actual relation ≤.
• Conversely, FirstOrder.Language.LEOfStructure, FirstOrder.Language.preorderOfModels, FirstOrder.Language.partialOrderOfModels, and FirstOrder.Language.linearOrderOfModels are the orders induced by first-order structures modelling the relevant theory.

Main Results

• PartialOrders model the theory of partial orders, LinearOrders model the theory of linear orders, and dense linear orders without endpoints model Language.dlo.
• Under L.orderedStructure assumptions, elements of any L.HomClass M N are monotone, and strictly monotone if injective.
• Under Language.order.orderedStructure assumptions, any OrderHomClass has an instance of L.HomClass M N, while M ↪o N and any OrderIsoClass have an instance of L.StrongHomClass M N.
• FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo shows that any countable nonempty model of the theory of linear orders is a Fraïssé limit of the class of finite models of the theory of linear orders.
• FirstOrder.Language.isFraisse_finite_linear_order shows that the class of finite models of the theory of linear orders is Fraïssé.

inductive FirstOrder.Language.orderRel : ℕ → Type

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

• le: FirstOrder.Language.orderRel 2

instance FirstOrder.Language.instDecidableEqOrderRel : {a : ℕ} → DecidableEq (FirstOrder.Language.orderRel a)

Equations

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

def FirstOrder.Language.order : FirstOrder.Language

The relational language consisting of a single relation representing ≤.

Equations

• FirstOrder.Language.order = { Functions := fun (x : ℕ) => Empty, Relations := FirstOrder.Language.orderRel }

@[simp]

theorem FirstOrder.Language.order.forall_relations {P : (n : ℕ) → FirstOrder.Language.order.Relations n → Prop} : (∀ {n : ℕ} (R : FirstOrder.Language.order.Relations n), P n R) ↔ P 2 FirstOrder.Language.orderRel.le

instance FirstOrder.Language.order.instSubsingleton {n : ℕ} : Subsingleton (FirstOrder.Language.order.Relations n)

Equations

• ⋯ = ⋯

instance FirstOrder.Language.order.instIsEmptyRelationsOfNatNat : IsEmpty (FirstOrder.Language.order.Relations 0)

Equations

• FirstOrder.Language.order.instIsEmptyRelationsOfNatNat = ⋯

class FirstOrder.Language.IsOrdered (L : FirstOrder.Language) : Type v

A language is ordered if it has a symbol representing ≤.

• leSymb : L.Relations 2

  The relation symbol representing ≤.

instance FirstOrder.Language.instIsOrderedOrder : FirstOrder.Language.order.IsOrdered

Equations

• FirstOrder.Language.instIsOrderedOrder = { leSymb := FirstOrder.Language.orderRel.le }

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

@[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_onFunction (L : FirstOrder.Language) [L.IsOrdered] {n : ℕ} (a : FirstOrder.Language.order.Functions n) : L.orderLHom.onFunction a = isEmptyElim a

def FirstOrder.Language.orderLHom (L : FirstOrder.Language) [L.IsOrdered] : FirstOrder.Language.order →ᴸ L

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_leSymb (L : FirstOrder.Language) [L.IsOrdered] : L.orderLHom.onRelation FirstOrder.Language.leSymb = FirstOrder.Language.leSymb

@[simp]

theorem FirstOrder.Language.orderLHom_order : FirstOrder.Language.order.orderLHom = FirstOrder.Language.LHom.id FirstOrder.Language.order

def FirstOrder.Language.preorderTheory (L : FirstOrder.Language) [L.IsOrdered] : L.Theory

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

• ⋯ = ⋯

def FirstOrder.Language.partialOrderTheory (L : FirstOrder.Language) [L.IsOrdered] : L.Theory

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

• ⋯ = ⋯

def FirstOrder.Language.linearOrderTheory (L : FirstOrder.Language) [L.IsOrdered] : L.Theory

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

• ⋯ = ⋯

def FirstOrder.Language.noTopOrderSentence (L : FirstOrder.Language) [L.IsOrdered] : L.Sentence

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

def FirstOrder.Language.noBotOrderSentence (L : FirstOrder.Language) [L.IsOrdered] : L.Sentence

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

def FirstOrder.Language.denselyOrderedSentence (L : FirstOrder.Language) [L.IsOrdered] : L.Sentence

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.

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

• ⋯ = ⋯

instance FirstOrder.Language.sum.instIsOrdered {L : FirstOrder.Language} : (L.sum FirstOrder.Language.order).IsOrdered

Equations

• FirstOrder.Language.sum.instIsOrdered = { leSymb := Sum.inr FirstOrder.Language.leSymb }

def FirstOrder.Language.orderStructure (M : Type w') [LE M] : FirstOrder.Language.order.Structure M

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] : Prop

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

• relMap_leSymb : ∀ (x : Fin 2 → M), FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb x ↔ x 0 ≤ x 1

@[simp]

theorem FirstOrder.Language.OrderedStructure.relMap_leSymb {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [LE M] [L.Structure M] [self : L.OrderedStructure M] (x : Fin 2 → M) : 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 { x : M // x ∈ 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 n → M} : (t₁.le 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_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] : NoTopOrder M

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] : NoBotOrder M

@[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 n → M} : (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] [h : M ⊨ L.dlo] : DenselyOrdered M

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

• L.leOfStructure M = { le := fun (a b : M) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b] }

instance FirstOrder.Language.instOrderedStructure (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] : L.OrderedStructure M

Equations

• ⋯ = ⋯

instance FirstOrder.Language.instDecidableRelLeOfRelMapLeSymbVecConsVecEmpty (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 LE.le

Equations

• L.instDecidableRelLeOfRelMapLeSymbVecConsVecEmpty M = h

def FirstOrder.Language.preorderOfModels (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [L.Structure M] [h : M ⊨ L.preorderTheory] : Preorder M

Any model of a theory of preorders is a preorder.

Equations

• L.preorderOfModels M = Preorder.mk ⋯ ⋯ ⋯

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

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

Equations

• L.partialOrderOfModels M = PartialOrder.mk ⋯

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]] : LinearOrder M

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] : FirstOrder.Language.order.HomClass 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) : Monotone ⇑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) : StrictMono ⇑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] : OrderIsoClass 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.

theorem FirstOrder.Language.dlo_isExtensionPair (M : Type w) [FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.linearOrderTheory] (N : Type w') [FirstOrder.Language.order.Structure N] [N ⊨ FirstOrder.Language.order.dlo] [Nonempty N] : FirstOrder.Language.order.IsExtensionPair M N

instance FirstOrder.Language.instInfiniteOfModelDloOrderOfNonempty (M : Type w) [FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.dlo] [Nonempty M] : Infinite M

Equations

• ⋯ = ⋯

theorem FirstOrder.Language.dlo_age (M : Type w') [FirstOrder.Language.order.Structure M] [Mdlo : M ⊨ FirstOrder.Language.order.dlo] [Nonempty M] : FirstOrder.Language.order.age M = {M : CategoryTheory.Bundled FirstOrder.Language.order.Structure | Finite ↑M ∧ ↑M ⊨ FirstOrder.Language.order.linearOrderTheory}

theorem FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo (M : Type w) [FirstOrder.Language.order.Structure M] [Countable M] [Nonempty M] [M ⊨ FirstOrder.Language.order.dlo] : FirstOrder.Language.IsFraisseLimit {M : CategoryTheory.Bundled FirstOrder.Language.order.Structure | Finite ↑M ∧ ↑M ⊨ FirstOrder.Language.order.linearOrderTheory} M

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.

theorem FirstOrder.Language.isFraisse_finite_linear_order : FirstOrder.Language.IsFraisse {M : CategoryTheory.Bundled FirstOrder.Language.order.Structure | Finite ↑M ∧ ↑M ⊨ FirstOrder.Language.order.linearOrderTheory}

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