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.

def FirstOrder.Language.order :

FirstOrder.Language

The language consisting of a single relation representing ≤.

Instances For

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

FirstOrder.Language.Structure FirstOrder.Language.order M

instance FirstOrder.Language.Order.Language.instIsRelational :

FirstOrder.Language.IsRelational FirstOrder.Language.order

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

Subsingleton (FirstOrder.Language.Relations FirstOrder.Language.order n)

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

leSymb : FirstOrder.Language.Relations L 2

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

Instances

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

Instances For

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

Instances For

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.

Instances For

instance FirstOrder.Language.instIsOrderedOrder :

FirstOrder.Language.IsOrdered FirstOrder.Language.order

@[simp]

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

FirstOrder.Language.LHom.onRelation (FirstOrder.Language.orderLHom L) 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)

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

FirstOrder.Language.Theory L

The theory of preorders.

Instances For

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

FirstOrder.Language.Theory L

The theory of partial orders.

Instances For

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

FirstOrder.Language.Theory L

The theory of linear orders.

Instances For

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

Instances For

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

Instances For

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

Instances For

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

FirstOrder.Language.Theory L

The theory of dense linear orders without endpoints.

Instances For

@[inline, reducible]

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

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

Instances For

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

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

M ⊨ FirstOrder.Language.preorderTheory FirstOrder.Language.order

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

M ⊨ FirstOrder.Language.partialOrderTheory FirstOrder.Language.order

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

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