pseudo-order

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.

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$ and $y$,

:

• Every two elements for which neither one is less than the other must be equal. That is, for all $x$ and $y$,

:

• For all {{mvar|x}}, {{mvar|y}}, and {{mvar|z}}, if {{math|x < y}} then either {{math|x < z}} or {{math|z < y}}. That is, for all $x$, $y$ and $z$,

:

There are common constructive reformulations making use of contrapositions and the valid equivalences $\backslash neg(\backslash phi\backslash land\backslash psi)\backslash leftrightarrow(\backslash phi\backslash to\backslash neg\backslash psi)$ as well as $\backslash neg(\backslash phi\backslash lor\backslash psi)\backslash leftrightarrow(\backslash neg\backslash phi\backslash land\backslash neg\backslash psi)$. The negation of the pseudo-order

:

and it really just expresses the asymmetry of

The second condition exactly expresses the anti-symmetry of the associated partial order,

:$(x\; \backslash le\; y\; \backslash land\; y\; \backslash le\; x)\; \backslash 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 . With it, the second condition exactly states that this relation is tight,

:$\backslash neg(x\; \backslash \#\; y)\; \backslash 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 $(\backslash phi\backslash lor\backslash psi)\; \backslash to\; (\backslash neg\backslash phi\backslash to\backslash 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.

The non-contradiction principle for the partial order states that $\backslash neg\backslash big(x\; \backslash le\; y\; \backslash land\; \backslash neg(x\; \backslash le\; y))$ or equivalently , for all elements. Constructively, the validity of the double-negation exactly means that there cannot be a refutation of any of the disjunctions in the classical claim , whether or not this proposition represents a decidable problem.

Using the asymmetry condition, the above also implies $\backslash neg\backslash neg(x\backslash le\; y\backslash lor\; y\backslash le\; x)$, the double-negated strong connectedness. In a classical logic context, "$\backslash le$" thus constitutes a (non-strict) total order.

The contrapositive of the third condition exactly expresses that the associated relation $x\backslash le\; y$ (the partial order) is transitive. So that property is called co-transitivity. Using the asymmetry condition, one quickly derives the theorem that a pseudo-order is actually transitive as well. Transitivity is common axiom in the classical definition of a linear order.

The condition also called is comparison (as well as weak linearity): For any nontrivial interval given by some $x$ and some $y$ above it, any third element $z$ is either above the lower bound or below the upper bound. Since this is an implication of a disjunction, it ties to the trichotomy law as well. And indeed, having a pseudo-order on a Dedekind-MacNeille-complete poset implies the principle of excluded middle. This impacts the discussion of completeness in the constructive theory of the real numbers.

This section assumes classical logic. At least then, following properties can be proven:

If R is a co-transitive relation, then

• R is also quasitransitive;
• R satisfies axiom 3 of semiorders;For symmetric R, semiorder axiom 3 even coincides with co-transitivity.
• incomparability w.r.t. R is a transitive relation;Transitivity of incomparability is required e.g. for strict weak orderings. and
• R is connex iff it is reflexive.unless the domain is a singleton set

Sufficient conditions for a co-transitive relation R to be transitive also are:

• R is left Euclidean;
• R is right Euclidean;
• R is antisymmetric.

A semi-connex relation R is also co-transitive if it is symmetric, left or right Euclidean, transitive, or quasitransitive. If incomparability w.r.t. R is a transitive relation, then R is co-transitive if it is symmetric, left or right Euclidean, or transitive.

• Constructive analysis
• Indecomposability (intuitionistic logic)
• Linear order

{{reflist|group=note}}

• {{cite book|last=Heyting|first=Arend|author-link=Arend Heyting|title=Intuitionism: an introduction|url=https://archive.org/details/intuitionismintr1966heyt|url-access=registration|edition=2nd|year=1966|publisher=North-Holland Pub. Co.|location=Amsterdam|page=[https://archive.org/details/intuitionismintr1966heyt/page/106 106]}}

{{reflist}}

Category:Constructivism (mathematics)

Category:Order theory