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é.
• FirstOrder.Language.aleph0_categorical_dlo shows that the theory of dense linear orders is ℵ₀-categorical, and thus complete.

inductive FirstOrder.Language.orderRel : ℕ → Type

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

• le : orderRel 2

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

Equations

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

def FirstOrder.Language.order : Language

The relational language consisting of a single relation representing ≤.

Equations

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

instance FirstOrder.Language.instorderIsRelational : Language.order.IsRelational

Equations

• ⋯ = Empty.instIsEmpty

@[simp]

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

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

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

instance FirstOrder.Language.order.instUniqueSigmaNatRelations : Unique ((n : ℕ) × Language.order.Relations n)

Equations

• FirstOrder.Language.order.instUniqueSigmaNatRelations = { default := ⟨2, FirstOrder.Language.orderRel.le⟩, uniq := FirstOrder.Language.order.instUniqueSigmaNatRelations._proof_3 }

instance FirstOrder.Language.order.instUniqueSymbols : Unique Language.order.Symbols

Equations

• FirstOrder.Language.order.instUniqueSymbols = { default := Sum.inr default, uniq := FirstOrder.Language.order.instUniqueSymbols._proof_6 }

@[simp]

theorem FirstOrder.Language.order.card_eq_one : Language.order.card = 1

class FirstOrder.Language.IsOrdered (L : 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 : Language.order.IsOrdered

Equations

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

theorem FirstOrder.Language.order.relation_eq_leSymb (R : Language.order.Relations 2) : R = leSymb

def FirstOrder.Language.Term.le {L : Language} {α : Type w} {n : ℕ} [L.IsOrdered] (t₁ 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 : Language} {α : Type w} {n : ℕ} [L.IsOrdered] (t₁ 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

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

@[simp]

theorem FirstOrder.Language.orderLHom_onRelation (L : Language) [L.IsOrdered] (x✝ : ℕ) (x✝¹ : Language.order.Relations x✝) : L.orderLHom.onRelation x✝¹ = match x✝, x✝¹ with | .(2), orderRel.le => leSymb

@[simp]

theorem FirstOrder.Language.orderLHom_leSymb (L : Language) [L.IsOrdered] : L.orderLHom.onRelation leSymb = leSymb

@[simp]

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

def FirstOrder.Language.preorderTheory (L : 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 : Language) [L.IsOrdered] : L.preorderTheory.IsUniversal

def FirstOrder.Language.partialOrderTheory (L : 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 : Language) [L.IsOrdered] : L.partialOrderTheory.IsUniversal

def FirstOrder.Language.linearOrderTheory (L : 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 : Language) [L.IsOrdered] : L.linearOrderTheory.IsUniversal

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

A sentence indicating that an order has no top element: $\mathrm{\forall }x,\mathrm{\exists }y,\mathrm{\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 : Language) [L.IsOrdered] : L.Sentence

A sentence indicating that an order has no bottom element: $\mathrm{\forall }x,\mathrm{\exists }y,\mathrm{\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 : Language) [L.IsOrdered] : L.Sentence

A sentence indicating that an order is dense: $\mathrm{\forall }x,\mathrm{\forall }y,x<y\to \mathrm{\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 : 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 : Language) {M : Type w'} [L.IsOrdered] [L.Structure M] [h : M ⊨ L.dlo] : M ⊨ L.linearOrderTheory

instance FirstOrder.Language.instModelPartialOrderTheoryOfLinearOrderTheory (L : Language) {M : Type w'} [L.IsOrdered] [L.Structure M] [h : M ⊨ L.linearOrderTheory] : M ⊨ L.partialOrderTheory

instance FirstOrder.Language.instModelPreorderTheoryOfPartialOrderTheory (L : Language) {M : Type w'} [L.IsOrdered] [L.Structure M] [h : M ⊨ L.partialOrderTheory] : M ⊨ L.preorderTheory

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

Equations

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

def FirstOrder.Language.orderStructure (M : Type w') [LE M] : 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 : 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) : Structure.RelMap leSymb x ↔ x 0 ≤ x 1

instance FirstOrder.Language.instOrderedStructureOfOrderOfIsExpansionOnOrderLHom {L : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [Language.order.Structure M] [Language.order.OrderedStructure M] [L.orderLHom.IsExpansionOn M] : L.OrderedStructure M

instance FirstOrder.Language.instIsExpansionOnOrderLHomOfOrderedStructureOrder {L : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] [Language.order.Structure M] [Language.order.OrderedStructure M] : L.orderLHom.IsExpansionOn M

instance FirstOrder.Language.instOrderedStructureSubtypeMemSubstructure {L : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] (S : L.Substructure M) : L.OrderedStructure ↥S

@[simp]

theorem FirstOrder.Language.Term.realize_le {L : Language} {α : Type w} {M : Type w'} {n : ℕ} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] {t₁ t₂ : L.Term (α ⊕ Fin n)} {v : α → M} {xs : Fin n → M} : (t₁.le t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ ≤ realize (Sum.elim v xs) t₂

theorem FirstOrder.Language.realize_noTopOrder_iff {L : 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 : 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 : 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 : 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 : 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 : 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 : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [Language.order.Structure M] [Language.order.OrderedStructure M] : L.OrderedStructure M ↔ L.orderLHom.IsExpansionOn M

instance FirstOrder.Language.model_preorder {L : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] : M ⊨ L.preorderTheory

@[simp]

theorem FirstOrder.Language.Term.realize_lt {L : Language} {α : Type w} {M : Type w'} {n : ℕ} [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] {t₁ t₂ : L.Term (α ⊕ Fin n)} {v : α → M} {xs : Fin n → M} : (t₁.lt t₂).Realize v xs ↔ realize (Sum.elim v xs) t₁ < realize (Sum.elim v xs) t₂

theorem FirstOrder.Language.realize_denselyOrdered_iff {L : 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 : 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 : Language) (M : Type w') [L.IsOrdered] [L.Structure M] [Preorder M] [L.OrderedStructure M] [M ⊨ L.dlo] : DenselyOrdered M

instance FirstOrder.Language.model_partialOrder {L : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [PartialOrder M] [L.OrderedStructure M] : M ⊨ L.partialOrderTheory

instance FirstOrder.Language.model_linearOrder {L : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LinearOrder M] [L.OrderedStructure M] : M ⊨ L.linearOrderTheory

instance FirstOrder.Language.model_dlo {L : Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LinearOrder M] [L.OrderedStructure M] [DenselyOrdered M] [NoTopOrder M] [NoBotOrder M] : M ⊨ L.dlo

def FirstOrder.Language.leOfStructure (L : 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 : Language) (M : Type w') [L.IsOrdered] [L.Structure M] : L.OrderedStructure M

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

The order structure on an ordered language is decidable.

Equations

• L.decidableLEOfStructure M = h

def FirstOrder.Language.preorderOfModels (L : 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 = { toLE := L.leOfStructure M, lt := fun (a b : M) => a ≤ b ∧ ¬b ≤ a, le_refl := ⋯, le_trans := ⋯, lt_iff_le_not_le := ⋯ }

def FirstOrder.Language.partialOrderOfModels (L : 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 = { toPreorder := L.preorderOfModels M, le_antisymm := ⋯ }

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

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

Equations

• One or more equations did not get rendered due to their size.

instance FirstOrder.Language.order.instHomClassOfOrderHomClass {M : Type w'} [Language.order.Structure M] [LE M] [Language.order.OrderedStructure M] {N : Type u_1} [Language.order.Structure N] [LE N] [Language.order.OrderedStructure N] {F : Type u_2} [FunLike F M N] [OrderHomClass F M N] : Language.order.HomClass F M N

instance FirstOrder.Language.order.instStrongHomClassOrderEmbedding {M : Type w'} [Language.order.Structure M] [LE M] [Language.order.OrderedStructure M] {N : Type u_1} [Language.order.Structure N] [LE N] [Language.order.OrderedStructure N] : Language.order.StrongHomClass (M ↪o N) M N

instance FirstOrder.Language.order.instStrongHomClassOfOrderIsoClass {M : Type w'} [Language.order.Structure M] [LE M] [Language.order.OrderedStructure M] {N : Type u_1} [Language.order.Structure N] [LE N] [Language.order.OrderedStructure N] {F : Type u_2} [EquivLike F M N] [OrderIsoClass F M N] : Language.order.StrongHomClass F M N

theorem FirstOrder.Language.HomClass.monotone {L : 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 : 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 : 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) [Language.order.Structure M] [M ⊨ Language.order.linearOrderTheory] (N : Type w') [Language.order.Structure N] [N ⊨ Language.order.dlo] [Nonempty N] : Language.order.IsExtensionPair M N

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

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

theorem FirstOrder.Language.isFraisseLimit_of_countable_nonempty_dlo (M : Type w) [Language.order.Structure M] [Countable M] [Nonempty M] [M ⊨ Language.order.dlo] : IsFraisseLimit {M : CategoryTheory.Bundled Language.order.Structure | Finite ↑M ∧ ↑M ⊨ 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 : IsFraisse {M : CategoryTheory.Bundled Language.order.Structure | Finite ↑M ∧ ↑M ⊨ Language.order.linearOrderTheory}

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

theorem FirstOrder.Language.aleph0_categorical_dlo : Cardinal.aleph0.Categorical Language.order.dlo

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

theorem FirstOrder.Language.dlo_isComplete : Language.order.dlo.IsComplete

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