# 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 = none yet
# | exportedby = [[First-order linear order defined via nonstrict inequality]]
# }}
#
# Here we provide theorems for a [[w:total order|linear order]] for use in a proof module which has already exported [[Interface:First-order linear order defined via nonstrict inequality]].
#
# We start by importing propositional and predicate logic.
#
param (PROPOSITIONAL Classical_propositional_calculus.ghi () "")
param (FIRSTORDER First-order_logic_with_quantifiability.ghi (PROPOSITIONAL) "")
#
# We also have as a parameter [[Interface:First-order linear order defined via nonstrict inequality]].
param (DEFINED First-order_linear_order_defined_via_nonstrict_inequality.ghi (PROPOSITIONAL FIRSTORDER) "")
#
# == Strict order ==
# There is a less-than predicate which obeys the usual equality axioms.
tvar (object x y z x0 y0 z0 x1 y1 z1)
var (object v v0 v1 v2)
term (formula (< x y))
#
# It is irreflexive, transitive, and total.
stmt (LessThanIrreflexivity () () (¬ (< x x)))
stmt (LessThanTransitivity () () (→ (∧ (< x y) (< y z)) (< x z)))
stmt (LessThanTotality () () (∨ (∨ (< x y) (= x y)) (< y x)))
#
# We also provide greater-than, which is just an abbreviation for less-than with the order of the arguments reversed.
term (formula (> x y))
stmt (GreaterThan () () (↔ (> x y) (< y x)))
#
# === Trichotomy ===
# Exactly one of `x < y`

, `x = y`

, or `y < x`

hold. Our propositional logic doesn't have a notation which directly states "exactly one of three propositions holds" and even if it did, it might be inconvenient to work with. So we provide multiple theorems to express this idea.
stmt (LessThanEquality () () (→ (< x y) (¬ (= x y))))
stmt (LessThanGreaterThan () () (→ (< x y) (¬ (> x y))))
stmt (EqualityLessThan () () (→ (= x y) (¬ (< x y))))
#
# == Less than or equal to ==
# The predicate `≤`

for less than or equal to was defined in [[Interface:First-order linear order defined via nonstrict inequality]], which also provides the builder `LessEqualBuilder`

, transitivity, antisymmetry, and totality. We add some consequences and convenience theorems.
#
# One consequence is reflexivity.
stmt (LessEqualReflexivity () () (≤ x x))
#
# We also provide greater-than-or-equal, which is just an abbreviation for less-than-or-equal with the order of the arguments reversed.
term (formula (≥ x y))
stmt (GreaterEqual () () (↔ (≥ x y) (≤ y x)))
#
# == Relationships between less-than, less-equal, and equality ==
stmt (LessThanLessEqual () () (↔ (< x y) (∧ (≤ x y) (¬ (= x y)))))
stmt (LessEqualLessThan () () (↔ (≤ x y) (∨ (< x y) (= x y))))
stmt (LessThanLessEqualImplication () () (→ (< x y) (≤ x y)))
stmt (EqualityLessEqual () () (→ (= x y) (≤ x y)))
stmt (LessEqualLessThanTransitivity () () (→ (∧ (≤ x y) (< y z)) (< x z)))
#
# == Builders ==
# Both predicates obey the usual builders. `LessEqualBuilder`

was already defined, so it is the only one not defined here.
stmt (LessThanBuilder () () (→ (∧ (= x0 x1) (= y0 y1)) (↔ (< x0 y0) (< x1 y1))))
stmt (LessThanBuilderLL () () (→ (= y0 y1) (↔ (< x y0) (< x y1))))
stmt (LessThanBuilderRR () () (→ (= x0 x1) (↔ (< x0 y) (< x1 y))))
stmt (buildLessThan () ((= x0 x1) (= y0 y1)) (↔ (< x0 y0) (< x1 y1)))
stmt (buildLessThanLL () ((= y0 y1)) (↔ (< x y0) (< x y1)))
stmt (buildLessThanRR () ((= x0 x1)) (↔ (< x0 y) (< x1 y)))
stmt (LessEqualBuilderRR () () (→ (= x0 x1) (↔ (≤ x0 y) (≤ x1 y))))
stmt (LessEqualBuilderLL () () (→ (= y0 y1) (↔ (≤ x y0) (≤ x y1))))
stmt (buildLessEqual () ((= x0 x1) (= y0 y1)) (↔ (≤ x0 y0) (≤ x1 y1)))
stmt (buildLessEqualRR () ((= x0 x1)) (↔ (≤ x0 y) (≤ x1 y)))
stmt (buildLessEqualLL () ((= y0 y1)) (↔ (≤ x y0) (≤ x y1)))
#
# {{DEFAULTSORT:{{PAGENAME}}}}
# [[Category:Total order]]