A binary relation $⧣$ on a set $A$ is called an apartness relation if it satisifies the following three properties:
- irreflexivity: for all $x \in A$, $\neg (x ⧣ x)$;
- symmetry: for all $x,y \in A$, if $x ⧣ y$ then $y ⧣ x$;
- comparison: for all $x,y,z \in A$, if $x ⧣ y$ then $x ⧣ z$ or $y ⧣ z$.
Apartness relations are not much considered in classical mathematics (where they are just the complements of equivalence relations) but are important in constructive mathematics, where they serve as a sort of "positive inequality" that can have nicer properties than simple inequivalence. For example, if one defines two real numbers to be constructively apart when there exists a rational number strictly between them, one can prove for all $x,y \in \mathbb{R}$ that $(x ⧣ y) \to (x < y) \vee (y < x)$, whereas the usual $(x \neq y) \to (x < y) \vee (y < x)$ cannot be proven without excluded middle.
In some typical constructive setting (say IZF for concreteness' sake), let's consider a strict partial order $<$ on some set: that is, $<$ is irreflexive and transitive (and therefore asymmetric). Define $R$ to be the union of $<$ with its converse; that is, $$x \mathbin{R} y \;\textrm{iff}\; (x < y) \vee (y < x). $$
What additional conditions are needed, either on $<$ or on $A$, so that $R$ is an apartness relation?
($R$ is easily proven irreflexive and symmetric, so this is really just about the comparison property.)
Being newish to constructive thinking, I at first naïvely thought that it would necessarily be one, but I quickly realized that this is true only classically. Knowing that $x \mathbin{R} y$ does not in general tell us, for any $z$, which of $x \mathbin{R} z$ or $y \mathbin{R} z$ holds; so without additional conditions it doesn't seem to me we can prove the disjunction. Certainly decidability of $<$ is a sufficient condition (Edit: not true, see Mark Savings' response below!), but I'd be interested in knowing if some weaker one suffices.
The comparison property under your assumptions can easily be restated as $x < y \to x < z \lor z < y$. I don’t really know how that can be simplified further.
You are incorrect that decidability of $<$ is sufficient. Consider $< = \{(1, 2)\} \subseteq \{0, 1, 2\}^2$. Then $1 < 2$ but neither $1<0$ nor $0<2$.
A fourth condition which is often discussed is “tightness”. This condition is $\neg (x \# y) \to x = y$. Classically, a tight apartness relation is necessarily $\neq$. In the particular case of a transitive, irreflexive relation $<$, we see that classically, tightness is equivalent to trichotomy ($x = y \lor x < y \lor y < x$), which in turn implies comparison.
However, constructively, this is not necessarily true. The partial order $\ngeq \subseteq \mathbb{R}^2$ is always transitive and irreflexive, and the tightness condition is also satisfied. However, the comparison condition can fail in some weird models.