The model theory of total preorders

The theory of total preorders in mathlib's Language.order — preorderTheory plus the totality sentence, one antisymmetry axiom short of linearOrderTheory — and the round-trip between its models and the working bundle Core.Order.TotalPreorder. The canonical semantic-ordering object is the model-theoretic one (a Language.order.Structure satisfying this theory, the same shape as every other model in the first-order substrate); the bundle is its decidable, proof-transparent presentation, and toStructure/ofModel exchange the two.

def FirstOrder.Language.totalPreorderTheory (L : Language) [L.IsOrdered] : L.Theory

The theory of total preorders: preorderTheory plus totality. Sits strictly between preorderTheory and linearOrderTheory (antisymmetry).

Equations

• L.totalPreorderTheory = insert FirstOrder.Language.leSymb.total L.preorderTheory

instance FirstOrder.Language.instModelPreorderTheoryOfTotalPreorderTheory {L : Language} [L.IsOrdered] {M : Type u_1} [L.Structure M] [h : M ⊨ L.totalPreorderTheory] : M ⊨ L.preorderTheory

@[implicit_reducible]

def Core.Order.TotalPreorder.toStructure {α : Type u_1} (ord : TotalPreorder α) : FirstOrder.Language.order.Structure α

The Language.order-structure a bundle presents: leSymb is ord.le.

Equations

• ord.toStructure = FirstOrder.Language.orderStructure α

theorem Core.Order.TotalPreorder.toStructure_model {α : Type u_1} (ord : TotalPreorder α) : α ⊨ FirstOrder.Language.order.totalPreorderTheory

The presented structure models the total-preorder theory: the bundle is a decidable presentation of the model-theoretic object.

def Core.Order.TotalPreorder.ofModel {α : Type u_1} [FirstOrder.Language.order.Structure α] [h : α ⊨ FirstOrder.Language.order.totalPreorderTheory] : TotalPreorder α

A model of the total-preorder theory presents a bundle: the two presentations round-trip.

Equations

• Core.Order.TotalPreorder.ofModel = { le := fun (a b : α) => FirstOrder.Language.Structure.RelMap FirstOrder.Language.leSymb ![a, b], isPreorder := ⋯, total := ⋯ }