In constructive mathematics, pseudo-order is a name given to certain binary relations appropriate for modeling continuous orderings. In classical mathematics, its axioms constitute a formulation of a strict total order (also called linear order), which in that context can also be defined in other, equivalent ways.
Examples The constructive theory of the real numbers is the prototypical example where the pseudo-order formulation becomes crucial. A real number is less than another if there exists (one can construct) a rational number greater than the former and less than the latter. In other words, here x < y holds if there exists a rational number z such that x < z < y. Notably, for the continuum in a constructive context, the usual trichotomy law does not hold, i.e. it is not automatically provable. The axioms in the characterization of orders like this are thus weaker (when working using just constructive logic) than alternative axioms of a strict total order, which are often employed in the classical context.
Definition A pseudo-order is a binary relation satisfying the three conditions:
It is not possible for two elements to each be less than the other. That is, for all x {\displaystyle x} and y {\displaystyle y} ,
¬ ( x < y ∧ y < x ) {\displaystyle \neg (x<y\land y<x)}
Every two elements for which neither one is less than the other must be equal. That is, for all x {\displaystyle x} and y {\displaystyle y} ,
¬ ( x < y ∨ y < x ) → x = y {\displaystyle \neg (x<y\lor y<x)\to x=y}
For all x, y, and z, if x < y then either x < z or z < y. That is, for all x {\displaystyle x} , y {\displaystyle y} and z {\displaystyle z} ,
x < y → ( x < z ∨ z < y ) {\displaystyle x<y\to (x<z\lor z<y)}
Auxiliary notation There are common constructive reformulations making use of contrapositions and the valid equivalences ¬ ( ϕ ∧ ψ ) ↔ ( ϕ → ¬ ψ ) {\displaystyle \neg (\phi \land \psi )\leftrightarrow (\phi \to \neg \psi )} as well as ¬ ( ϕ ∨ ψ ) ↔ ( ¬ ϕ ∧ ¬ ψ ) {\displaystyle \neg (\phi \lor \psi )\leftrightarrow (\neg \phi \land \neg \psi )} . The negation of the pseudo-order x < y {\displaystyle x<y} of two elements defines a reflexive partial order y ≤ x {\displaystyle y\leq x} . In these terms, the first condition reads
x < y → x ≤ y {\displaystyle x<y\to x\leq y}
and it really just expresses the asymmetry of x < y {\displaystyle x<y} . It implies irreflexivity, as familiar from the classical theory.
Classical equivalents to trichotomy The second condition exactly expresses the anti-symmetry of the associated partial order,
( x ≤ y ∧ y ≤ x ) → x = y {\displaystyle (x\leq y\land y\leq x)\to x=y}
With the above two reformulations, the negation signs may be hidden in the definition of a pseudo-order. A natural apartness relation on a pseudo-ordered set is given by x # y := ( x < y ∨ y < x ) {\displaystyle x\#y:=(x<y\lor y<x)} . With it, the second condition exactly states that this relation is tight,
¬ ( x # y ) → x = y {\displaystyle \neg (x\#y)\to x=y}
Together with the first axiom, this means equality can be expressed as negation of apartness. Note that the negation of equality is in general merely the double-negation of apartness. Now the disjunctive syllogism may be expressed as ( ϕ ∨ ψ ) → ( ¬ ϕ → ψ ) {\displaystyle (\phi \lor \psi )\to (\neg \phi \to \psi )} . Such a logical implication can classically be reversed, and then this condition exactly expresses trichotomy. As such, it is also a formulation of connectedness.
Discussion
… excerpt ends here. Continue reading the full article.
