The theory of total preorders

This file defines the first-order theory of total preorders in an ordered language, which is preorderTheory together with the totality sentence. It sits strictly between preorderTheory and linearOrderTheory, one antisymmetry axiom short of the latter. A preorder whose ≤ is total models it, and every model of it is a model of preorderTheory. [UPSTREAM] candidate for Mathlib.ModelTheory.Order.

Main declarations

• FirstOrder.Language.totalPreorderTheory: the theory of total preorders.
• FirstOrder.Language.model_totalPreorder: a total preorder is a model of the theory.

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

The theory of total preorders is preorderTheory together with totality.

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

instance FirstOrder.Language.model_totalPreorder {L : Language} [L.IsOrdered] {M : Type u_1} [L.Structure M] [Preorder M] [Std.Total fun (x1 x2 : M) => x1 ≤ x2] [L.OrderedStructure M] : M ⊨ L.totalPreorderTheory

A preorder whose ≤ is total is a model of the theory of total preorders.

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

A linear order models the theory of total preorders.