Total order on constructive real numbers

Question

Is there a definition of the real numbers in constructive or intuitionistic logic such as the order is total, ie $$ \forall x,y\in\mathbb{R},\; x \leq y \lor y \leq x $$ The classical proof of this totality usually starts with an excluded middle, asserting that either $x\leq y$ or not. The negative case leads to $y\leq x$. But in constructive logic we cannot use this excluded middle.

According to this page, the definitions of the real numbers by Cauchy sequences or Dedekind cuts are not equivalent. Maybe one has the total order and not the other.

Without a total order I don't think we can say much about real numbers. For example, would a $x\in\mathbb{R}$ even have decimal expansion or integer part ? Usually those involve finding the smallest integer greater than $x$.

Answer 1

In intuitionistic mathematics, what we have is $$\forall x,y\quad x\#{}y\to x<y \lor y<x$$ where $\#$ is the intuitionistic notion of apartness. Now, if we define equality in terms of apartness and negation $$x=y\equiv{\lnot{x\# y}}$$ we have $$\forall{x,y}\quad \lnot (\lnot (x\leq y) \land \lnot (y\leq x))$$ which is classically, but not intuitionistically, equivalent to $$\forall x,y\quad x\leq y \lor y\leq x$$

Naturally, intuitionistic real numbers, which are defined by computable Cauchy sequences, can still have decimal expansions and integer parts.