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

Equations
Instances For
Equations

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

• leSymb : L.Relations 2
Instances
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
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

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

Equations
Instances For
@[simp]
theorem FirstOrder.Language.orderLHom_leSymb {L : FirstOrder.Language} [L.IsOrdered] :
L.orderLHom.onRelation FirstOrder.Language.leSymb = FirstOrder.Language.leSymb
@[simp]
Equations
• FirstOrder.Language.sum.instIsOrdered = { leSymb := Sum.inr FirstOrder.Language.leSymb }

The theory of preorders.

Equations
• L.preorderTheory = {FirstOrder.Language.leSymb.reflexive, FirstOrder.Language.leSymb.transitive}
Instances For

The theory of partial orders.

Equations
• L.partialOrderTheory = {FirstOrder.Language.leSymb.reflexive, FirstOrder.Language.leSymb.antisymmetric, FirstOrder.Language.leSymb.transitive}
Instances For

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

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

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

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
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
@[reducible, inline]
abbrev FirstOrder.Language.OrderedStructure (L : FirstOrder.Language) (M : Type w') [L.IsOrdered] [LE M] [L.Structure M] :

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

Equations
• L.OrderedStructure M = L.orderLHom.IsExpansionOn M
Instances For
@[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
Equations
• =
Equations
• =
Equations
• =
Equations
• =
@[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
@[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 nM} :
(t₁.le t₂).Realize v xs
@[simp]
theorem FirstOrder.Language.Term.realize_lt {L : FirstOrder.Language} {α : Type w} {M : Type w'} {n : } [L.IsOrdered] [L.Structure M] [] [L.OrderedStructure M] {t₁ : L.Term (α Fin n)} {t₂ : L.Term (α Fin n)} {v : αM} {xs : Fin nM} :
(t₁.lt t₂).Realize v xs <
@[simp]
theorem FirstOrder.Language.realize_noTopOrder {M : Type w'} [LE M] [h : ] :
M FirstOrder.Language.order.noTopOrderSentence
@[simp]
theorem FirstOrder.Language.realize_noBotOrder {M : Type w'} [LE M] [h : ] :
M FirstOrder.Language.order.noBotOrderSentence
@[simp]
theorem FirstOrder.Language.realize_denselyOrdered {M : Type w'} [] [h : ] :
M FirstOrder.Language.order.denselyOrderedSentence
instance FirstOrder.Language.model_dlo {M : Type w'} [] [] [] [] :
Equations
• =