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.orderStructure is the structure on an ordered type, assigning the symbol representing ≤ to the actual relation ≤.
• 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.

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.

def FirstOrder.Language.order : FirstOrder.Language

The language consisting of a single relation representing ≤.

Equations

• FirstOrder.Language.order = FirstOrder.Language.mk₂ Empty Empty Empty Empty Unit

instance FirstOrder.Language.orderStructure {M : Type w'} [LE M] : FirstOrder.Language.Structure FirstOrder.Language.order M

Equations

• FirstOrder.Language.orderStructure = FirstOrder.Language.Structure.mk₂ Empty.elim Empty.elim Empty.elim Empty.elim fun (x : Unit) (x x_1 : M) => x ≤ x_1

instance FirstOrder.Language.Order.Language.instIsRelational : FirstOrder.Language.IsRelational FirstOrder.Language.order

Equations

• FirstOrder.Language.Order.Language.instIsRelational = (_ : FirstOrder.Language.IsRelational (FirstOrder.Language.mk₂ Empty Empty Empty Empty Unit))

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

Equations

• (_ : Subsingleton (FirstOrder.Language.order.Relations n)) = (_ : Subsingleton ((FirstOrder.Language.mk₂ Empty Empty Empty Empty Unit).Relations n))

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

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

• leSymb : L.Relations 2

def FirstOrder.Language.Term.le {L : FirstOrder.Language} {α : Type w} {n : ℕ} [FirstOrder.Language.IsOrdered L] (t₁ : FirstOrder.Language.Term L (α ⊕ Fin n)) (t₂ : FirstOrder.Language.Term L (α ⊕ Fin n)) : FirstOrder.Language.BoundedFormula L α n

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

Equations

• FirstOrder.Language.Term.le t₁ t₂ = FirstOrder.Language.Relations.boundedFormula₂ FirstOrder.Language.leSymb t₁ t₂

def FirstOrder.Language.Term.lt {L : FirstOrder.Language} {α : Type w} {n : ℕ} [FirstOrder.Language.IsOrdered L] (t₁ : FirstOrder.Language.Term L (α ⊕ Fin n)) (t₂ : FirstOrder.Language.Term L (α ⊕ Fin n)) : FirstOrder.Language.BoundedFormula L α n

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

Equations

• FirstOrder.Language.Term.lt t₁ t₂ = FirstOrder.Language.Term.le t₁ t₂ ⊓ FirstOrder.Language.BoundedFormula.not (FirstOrder.Language.Term.le t₂ t₁)

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

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

Equations

• FirstOrder.Language.orderLHom L = FirstOrder.Language.LHom.mk₂ Empty.elim Empty.elim Empty.elim Empty.elim fun (x : Unit) => FirstOrder.Language.leSymb

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

Equations

• FirstOrder.Language.instIsOrderedOrder = { leSymb := () }

@[simp]

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

@[simp]

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

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

Equations

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

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

The theory of preorders.

Equations

• FirstOrder.Language.preorderTheory L = {FirstOrder.Language.Relations.reflexive FirstOrder.Language.leSymb, FirstOrder.Language.Relations.transitive FirstOrder.Language.leSymb}

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

The theory of partial orders.

Equations

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

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

The theory of linear orders.

Equations

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

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

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

Equations

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

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

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

Equations

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

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

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) [FirstOrder.Language.IsOrdered L] : FirstOrder.Language.Theory L

The theory of dense linear orders without endpoints.

Equations

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

@[inline, reducible]

abbrev FirstOrder.Language.OrderedStructure (L : FirstOrder.Language) (M : Type w') [FirstOrder.Language.IsOrdered L] [LE M] [FirstOrder.Language.Structure L M] : Prop

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

Equations

• FirstOrder.Language.OrderedStructure L M = FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.orderLHom L) M

@[simp]

theorem FirstOrder.Language.orderedStructure_iff {L : FirstOrder.Language} {M : Type w'} [FirstOrder.Language.IsOrdered L] [LE M] [FirstOrder.Language.Structure L M] : FirstOrder.Language.OrderedStructure L M ↔ FirstOrder.Language.LHom.IsExpansionOn (FirstOrder.Language.orderLHom L) M

instance FirstOrder.Language.orderedStructure_LE {M : Type w'} [LE M] : FirstOrder.Language.OrderedStructure FirstOrder.Language.order M

Equations

• (_ : FirstOrder.Language.OrderedStructure FirstOrder.Language.order M) = (_ : FirstOrder.Language.OrderedStructure FirstOrder.Language.order M)

instance FirstOrder.Language.model_preorder {M : Type w'} [Preorder M] : M ⊨ FirstOrder.Language.preorderTheory FirstOrder.Language.order

Equations

• (_ : M ⊨ FirstOrder.Language.preorderTheory FirstOrder.Language.order) = (_ : M ⊨ FirstOrder.Language.preorderTheory FirstOrder.Language.order)

instance FirstOrder.Language.model_partialOrder {M : Type w'} [PartialOrder M] : M ⊨ FirstOrder.Language.partialOrderTheory FirstOrder.Language.order

Equations

• (_ : M ⊨ FirstOrder.Language.partialOrderTheory FirstOrder.Language.order) = (_ : M ⊨ FirstOrder.Language.partialOrderTheory FirstOrder.Language.order)

instance FirstOrder.Language.model_linearOrder {M : Type w'} [LinearOrder M] : M ⊨ FirstOrder.Language.linearOrderTheory FirstOrder.Language.order

Equations

• (_ : M ⊨ FirstOrder.Language.linearOrderTheory FirstOrder.Language.order) = (_ : M ⊨ FirstOrder.Language.linearOrderTheory FirstOrder.Language.order)

@[simp]

theorem FirstOrder.Language.relMap_leSymb {L : FirstOrder.Language} {M : Type w'} [FirstOrder.Language.IsOrdered L] [FirstOrder.Language.Structure L M] [LE M] [FirstOrder.Language.OrderedStructure L M] {a : M} {b : M} : FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b] ↔ a ≤ b

@[simp]

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

@[simp]

theorem FirstOrder.Language.Term.realize_lt {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : ℕ} [FirstOrder.Language.IsOrdered L] [FirstOrder.Language.Structure L M] [Preorder M] [FirstOrder.Language.OrderedStructure L M] {t₁ : FirstOrder.Language.Term L (α ⊕ Fin n)} {t₂ : FirstOrder.Language.Term L (α ⊕ Fin n)} {v : α → M} {xs : Fin n → M} : FirstOrder.Language.BoundedFormula.Realize (FirstOrder.Language.Term.lt t₁ t₂) 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 {M : Type w'} [LE M] : M ⊨ FirstOrder.Language.noTopOrderSentence FirstOrder.Language.order ↔ NoTopOrder M

@[simp]

theorem FirstOrder.Language.realize_noTopOrder {M : Type w'} [LE M] [h : NoTopOrder M] : M ⊨ FirstOrder.Language.noTopOrderSentence FirstOrder.Language.order

theorem FirstOrder.Language.realize_noBotOrder_iff {M : Type w'} [LE M] : M ⊨ FirstOrder.Language.noBotOrderSentence FirstOrder.Language.order ↔ NoBotOrder M

@[simp]

theorem FirstOrder.Language.realize_noBotOrder {M : Type w'} [LE M] [h : NoBotOrder M] : M ⊨ FirstOrder.Language.noBotOrderSentence FirstOrder.Language.order

theorem FirstOrder.Language.realize_denselyOrdered_iff {M : Type w'} [Preorder M] : M ⊨ FirstOrder.Language.denselyOrderedSentence FirstOrder.Language.order ↔ DenselyOrdered M

@[simp]

theorem FirstOrder.Language.realize_denselyOrdered {M : Type w'} [Preorder M] [h : DenselyOrdered M] : M ⊨ FirstOrder.Language.denselyOrderedSentence FirstOrder.Language.order

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

Equations

• (_ : M ⊨ FirstOrder.Language.dlo FirstOrder.Language.order) = (_ : M ⊨ FirstOrder.Language.dlo FirstOrder.Language.order)