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$.


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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.