[FOM] Intuitionists and excluded-middle

[Jesse Alama]

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.  Where does the proof fail to be constructive?
(Is it the move from "it is not the case that sqrt(2) is rational" to
"sqrt(2) is irrational"?)

Jesse

-- 
Jesse Alama (alama at stanford.edu)