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.

source

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

Instances For

source

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

FirstOrder.Language.order.Structure 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

source

instance FirstOrder.Language.Order.Language.instIsRelational :

FirstOrder.Language.order.IsRelational

Equations

FirstOrder.Language.Order.Language.instIsRelational = ⋯

source

instance FirstOrder.Language.Order.Language.instSubsingleton {n : ℕ} :

Subsingleton (FirstOrder.Language.order.Relations n)

Equations

⋯ = ⋯

source

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

Type v

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

leSymb : L.Relations 2

Instances

source

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₂

Instances For

source

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

Instances For

source

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

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

Instances For

source

instance FirstOrder.Language.instIsOrderedOrder :

FirstOrder.Language.order.IsOrdered

Equations

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

source

@[simp]

theorem FirstOrder.Language.orderLHom_leSymb {L : FirstOrder.Language} [L.IsOrdered] :

L.orderLHom.onRelation FirstOrder.Language.leSymb = FirstOrder.Language.leSymb

source

@[simp]

theorem FirstOrder.Language.orderLHom_order :

FirstOrder.Language.order.orderLHom = FirstOrder.Language.LHom.id FirstOrder.Language.order

source

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 }

source

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}

Instances For

source

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

L.Theory

The theory of partial orders.

Equations

L.partialOrderTheory = {FirstOrder.Language.leSymb.reflexive, FirstOrder.Language.leSymb.antisymmetric, FirstOrder.Language.leSymb.transitive}

Instances For

source

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

L.Theory

The theory of linear orders.

Equations

L.linearOrderTheory = {FirstOrder.Language.leSymb.reflexive, FirstOrder.Language.leSymb.antisymmetric, FirstOrder.Language.leSymb.transitive, FirstOrder.Language.leSymb.total}

Instances For

source

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

Instances For

source

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

Instances For

source

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.

Instances For

source

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}

Instances For

source

@[reducible, inline]

abbrev 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

Equations

L.OrderedStructure M = L.orderLHom.IsExpansionOn M

Instances For

source

@[simp]

theorem FirstOrder.Language.orderedStructure_iff {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [LE M] [L.Structure M] :

L.OrderedStructure M ↔ L.orderLHom.IsExpansionOn M

source

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

FirstOrder.Language.order.OrderedStructure M

Equations

⋯ = ⋯

source

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

M ⊨ FirstOrder.Language.order.preorderTheory

Equations

⋯ = ⋯

source

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

M ⊨ FirstOrder.Language.order.partialOrderTheory

Equations

⋯ = ⋯

source

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

M ⊨ FirstOrder.Language.order.linearOrderTheory

Equations

⋯ = ⋯

source

@[simp]

theorem FirstOrder.Language.relMap_leSymb {L : FirstOrder.Language} {M : Type w'} [L.IsOrdered] [L.Structure M] [LE M] [L.OrderedStructure M] {a : M} {b : M} :

FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b] ↔ a ≤ b

source

@[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₂

source

@[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} :