[FOM] Intuitionists and excluded-middle
jeremy.clark at wanadoo.fr
Mon Oct 24 03:42:36 EDT 2005
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.)
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
More information about the FOM