# mathlib3documentation

model_theory.order

# Ordered First-Ordered Structures #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4. This file defines ordered first-order languages and structures, as well as their theories.

## Main Definitions #

• first_order.language.order is the language consisting of a single relation representing ≤.
• first_order.language.order_Structure is the structure on an ordered type, assigning the symbol representing ≤ to the actual relation ≤.
• first_order.language.is_ordered points out a specific symbol in a language as representing ≤.
• first_order.language.ordered_structure indicates that the ≤ symbol in an ordered language is interpreted as the actual relation ≤ in a particular structure.
• first_order.language.linear_order_theory and similar define the theories of preorders, partial orders, and linear orders.
• first_order.language.DLO defines the theory of dense linear orders without endpoints, a particularly useful example in model theory.

## Main Results #

• partial_orders model the theory of partial orders, linear_orders model the theory of linear orders, and dense linear orders without endpoints model Theory.DLO.
@[protected]

The language consisting of a single relation representing ≤.

Equations
Instances for first_order.language.order
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
@[class]

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

Instances of this typeclass
Instances of other typeclasses for first_order.language.is_ordered
• first_order.language.is_ordered.has_sizeof_inst
def first_order.language.term.le {L : first_order.language} {α : Type w} {n : } [L.is_ordered] (t₁ t₂ : L.term fin n)) :
n

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

Equations
def first_order.language.term.lt {L : first_order.language} {α : Type w} {n : } [L.is_ordered] (t₁ t₂ : L.term fin n)) :
n

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

Equations

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

Equations
Instances for first_order.language.order_Lhom
@[protected, instance]
Equations
@[simp]
@[protected, instance]
Equations

The theory of preorders.

Equations
Instances for first_order.language.preorder_theory

The theory of partial orders.

Equations
Instances for first_order.language.partial_order_theory

The theory of linear orders.

Equations
Instances for first_order.language.linear_order_theory

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

Equations

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

Equations

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

Equations

The theory of dense linear orders without endpoints.

Equations
Instances for first_order.language.DLO
@[reducible]

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

@[protected, instance]
@[protected, instance]
@[protected, instance]
@[protected, instance]
@[simp]
@[simp]
theorem first_order.language.term.realize_le {L : first_order.language} {α : Type w} {M : Type w'} {n : } [L.is_ordered] [L.Structure M] [has_le M] [L.ordered_structure M] {t₁ t₂ : L.term fin n)} {v : α M} {xs : fin n M} :
(t₁.le t₂).realize v xs
@[simp]
theorem first_order.language.term.realize_lt {L : first_order.language} {α : Type w} {M : Type w'} {n : } [L.is_ordered] [L.Structure M] [preorder M] [L.ordered_structure M] {t₁ t₂ : L.term fin n)} {v : α M} {xs : fin n M} :
(t₁.lt t₂).realize v xs <
@[simp]
@[simp]
@[protected, instance]