[FOM] Intuitionists and excluded-middle

[John McCarthy]

If one adds a sufficiently small rational d to the smaller irrational
a, the sum a + d will still be irrational.  To find a suitable d, one
needs to show that b - a is positive and that there is a smaller
positive rational d.  Any of  several ways of introducing the reals
will suffice for that.  I imagine it can be done for algebraic
irrationals without introducing the reals.