[FOM] Intuitionists and excluded-middle

[Andrej Bauer]

Neil Tennant wrote:
> But if one uses, instead of "not(x=y)", the binary formula
> 
> 	there exists z (z is rational & ((x<z & z<y) v (y<z & z<x))),
> 
> then of course more will be needed for the proof of the "irrationality" of
> the square root of 2. For then the sought result is
> 
> 	for all x there exists z
> 	(z is rational & ((x<z & z < sqrt(2)) v (sqrt(2)<z & z<x))).

As I wrote in a post to FOM, constructivists do in fact use the
apartness relation which you mention above in place of negation of
equality. In this sense the usual classical proof of sqrt(2) does not
prove that sqrt(2) is irrational, only "not rational".

I can think of a proof that between sqrt(2) and a rational there is
always another rational, but my proof is not particularly elegant.

Andrej