Inequality and Intuitionistic Logic

Question

Let $ x , y \in \mathbb R $. Is the proposition $ x \le y \rightarrow x = y \lor x < y $ true in intuitionistic logic? What about $ x \le y \rightarrow \neg \neg ( x = y \lor x < y ) $ (with $ \neg $ the negation)?

Answer 1

First, note that your question is mathematical, not logical. So, you may ask "Is it true in constructive mathematics using intuitionistic logic?" but not "Is it true in intuitionistic logic?". In logic, there is no "$ \le $" or "$ < $". Also note that for a constructivist, "true" mean "provable".

Back to your question, in constructive mathematics, for $ x , y \in \mathbb R $, $ x \le y $ is usually defined to be equivalent to $ \neg x > y $. By this definition, one can constructively prove $ x \le y \land y \le x \rightarrow x = y $. Note that $ \neg A $ is defined to be equivalent to $ A \rightarrow \bot $, where $ \bot $ is a symbol denoting a contradiction.

Now, you can show that $ x \le y \rightarrow \neg \neg ( x = y \lor x < y ) $ is true constructively. Assume that $ x \le y $. Now, if $ \neg ( x = y \lor x < y ) $ then $ \neg x = y $ and $ x \ge y $. Because $ x \le y $ and $ x \ge y $, therefore $ x = y $. Hence, we proved both $ x = y $ and $ \neg x = y $, which leads to a contradiction. So, assuming $ \neg ( x = y \lor x < y ) $ we proved $\bot$, that means we have a proof of $ \neg \neg ( x = y \lor x < y ) $. Also, assuming $ x \le y $ we proved $ \neg \neg ( x = y \lor x < y ) $, that means we have a proof of $ x \le y \rightarrow \neg \neg ( x = y \lor x < y ) $.

But $ x \le y \rightarrow x = y \lor x < y $ is not provable constructively. For showing this, you can use Brouwerian counterexamples like this one:
Let $ P ( n ) $ denote a statement about a natural number $ n $, which can be proven to be true or false for a given $ n $, but there is no proof for $ \forall n \, P ( n ) $, and also there's no proof for $ \exists n \, \neg P ( n ) $. For instance, $ P ( n ) $ can be equivalent to "$ 2 n + 4 $ is equal to the sum of two prime numbers." (see Goldbach's conjecture). Now, define the sequence $ ( \alpha _ n ) _ { n = 0 } ^ \infty $ of rational numbers in this way:
$ \alpha _ n = 0 $ iff $ P ( n ) $ is true, and $ \alpha _ n = \frac 1 m $ iff $ m \le n $ is the smallest natural number for which $ P ( m ) $ is false.
You can see that $ ( \alpha _ n ) _ { n = 0 } ^ \infty $ is a Cauchy sequence, and hence, represents a unique real number, say $ \beta $.
Now, it's easy to see that $ \beta = 0 $ iff $ \forall n \, P ( n ) $, and $ \beta > 0 $ iff $ \exists n \, \neg P ( n ) $. Also, obviously, $ \beta \ge 0 $. But we chose $ P ( n ) $ in a way that there's no proof for $ \forall n \, P ( n ) $ or $ \exists n \, \neg P ( n ) $. So we can prove $ \beta \ge 0 $ but we can't prove $ \beta > 0 $ or $ \beta = 0 $. that means $ \beta \ge 0 \rightarrow \beta = 0 \lor \beta > 0 $ is not provable.

For more details and other interesting constructive arguments, you can see this book for example.