# Creative Commons Attribution-Share Alike 3.0 Unported (http://creativecommons.org/licenses/by-sa/3.0/)
# {{modules
# | parameters = [[Interface:Classical propositional calculus|Classical propositional calculus]], [[Interface:First-order logic with quantifiability|first-order logic]]
# | importedby = [[First-order linear order defined via nonstrict inequality]]
# | exportedby = [[Basic arithmetic]]
# }}
#
# A ''[[w:total order|linear order]]'' or ''total order'' has an ordering predicate which lets us compare any two elements for order.
#
# Here we define a linear order in terms of what is called non-strict inequality, or "less than or equal to".
#
# This is a first-order presentation (that is, not built on set theory).
#
# We start by importing propositional and predicate logic.
param (PROPOSITIONAL Classical_propositional_calculus.ghi () "")
param (FIRSTORDER First-order_logic_with_quantifiability.ghi (PROPOSITIONAL) "")
#
# == Non-strict order ==
# There is an order which obeys the usual equality axioms.
tvar (object x y z x0 y0 z0 x1 y1 z1)
term (formula (≤ x y))
stmt (LessEqualBuilder () () (→ (∧ (= x0 x1) (= y0 y1)) (↔ (≤ x0 y0) (≤ x1 y1))))
#
# It is antisymmetric, transitive, and total.
stmt (LessEqualAntisymmetry () () (→ (∧ (≤ x y) (≤ y x)) (= x y)))
stmt (LessEqualTransitivity () () (→ (∧ (≤ x y) (≤ y z)) (≤ x z)))
stmt (LessEqualTotality () () (∨ (≤ x y) (≤ y x)))
#
# That is sufficient. These properties imply the theorems in [[Interface:First-order linear order]].
#
# {{DEFAULTSORT:{{PAGENAME}}}}
# [[Category:Total order]]