[FOM] Intuitionists and excluded-middle

[Jeremy Clark]

Just for the record, here is the constructive proof of the  
irrationality of sqrt(2).

Define x < y iff there is positive integer n s.t. y-x > 1/n.
Define x neq y iff x<y or y<x (or equivalently abs(x-y) > 0).
Define x irrational iff for all rational a/b, x neq a/b. (Note that  
this is stronger than not(x=y).)

Consider rational a/b. We can prove (by usual means) that a^2 - 2b^2  
neq 0. (This is integer neq, of course.)
Now,

abs( a/b - sqrt(2) ) = abs( (a/b + sqrt(2)) )^-1 b^-2  abs (a^2 -  
2b^2) > ((abs(a)+2)b^2)^-1

So we get a/b neq sqrt(2) for all rational a/b, so sqrt(2) is  
irrational.

Regards,

Jeremy Clark