# Documentation

Mathlib.ModelTheory.Order

# 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.

The language consisting of a single relation representing ≤.

Instances For
• leSymb :

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

Instances

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

Instances For

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

Instances For

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

Instances For
@[simp]
theorem FirstOrder.Language.orderLHom_leSymb {L : FirstOrder.Language} :
FirstOrder.Language.LHom.onRelation () FirstOrder.Language.leSymb = FirstOrder.Language.leSymb

The theory of preorders.

Instances For

The theory of partial orders.

Instances For

The theory of linear orders.

Instances For

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

Instances For

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

Instances For

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

Instances For

The theory of dense linear orders without endpoints.

Instances For
@[inline, reducible]

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

Instances For
@[simp]
@[simp]
theorem FirstOrder.Language.relMap_leSymb {L : FirstOrder.Language} {M : Type w'} [LE 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 : } [LE M] {t₁ : FirstOrder.Language.Term L (α Fin n)} {t₂ : FirstOrder.Language.Term L (α Fin n)} {v : αM} {xs : Fin nM} :
@[simp]
theorem FirstOrder.Language.Term.realize_lt {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : } [] {t₁ : FirstOrder.Language.Term L (α Fin n)} {t₂ : FirstOrder.Language.Term L (α Fin n)} {v : αM} {xs : Fin nM} :
<
@[simp]
theorem FirstOrder.Language.realize_noTopOrder {M : Type w'} [LE M] [h : ] :
@[simp]
theorem FirstOrder.Language.realize_noBotOrder {M : Type w'} [LE M] [h : ] :
@[simp]
instance FirstOrder.Language.model_dlo {M : Type w'} [] [] [] [] :