[FOM] Intuitionists and excluded-middle

[Andrej Bauer]

Jesse Alama wrote:
> Andrej Bauer <Andrej.Bauer at andrej.com> writes:
> 
>> P.S. What is the best way to prove constructively that sqrt(2) is
>> distinct from every rational? The usual classical proof only shows that
>> sqrt(2) is _not_ rational? (Note that x is distinct from y
>> constructively if there is a rational in between.)
> 
> Isn't the usual classical proof also "constructive"?  We begin by
> assuming that sqrt(2) is rational and get a contradiction; so we can
> conclude, even in a constructive setting, that it is not the case that
> sqrt(2) is rational.

In constructive mathematics there is distinction between "it is not the
case that x = y" and "x is different from y". The former means that x=y
implies false, and the latter that there is a rational number strictly
between x and y (or between 0 and |x-y|, if you prefer). Inequality of
reals in this senese is an example of an apartness relation, which is
the constructive substitute for classical inequality.

Thus the usual classical definition of irrationality is not (on the face
of it) equivalent to the constructive definition of irrationality:
- classical: x is irrational if for all rational q, not x = q
- constructive: x is irrational if for all rational q, x is different
  from q.

> Where does the proof fail to be constructive?

The proof simply does not prove that sqrt(2) is irrational according to
the above constructive definition. Instead, one has to prove, as simply
as possible: for every rational p there is a rational q such that
q is between p and sqrt(2). I think a suitable zero-finding method for
the equation x^2 - 2 = 0 will do the trick.

Andrej Bauer