[FOM] Intuitionists and excluded-middle

[Neil Tennant]

On Sun, 23 Oct 2005, Alexei E Angelides wrote:

> I understand the "usual" proof to go:
> 
> Assume sqrt(2) is rational
> [insert reductio]
> Hence, sqrt(2) is irrational.
> 
> Whereas I understand an acceptable constructive proof to go:
> 
> Assume sqrt(2) is rational
> [insert reductio]
> Hence, sqrt(2) is not rational.
> 
> The "constructive" proof only yields that sqrt(2) is not rational.
> Constructively showing that sqrt(2) is irrational would require a suitable
> constructive definition of "irrational" and then would require finding an
> example of such a number with that property satisfying the definition. 

I had understood the constructive predicate "x is irrational" to be
defined as "it is not the case that x is rational", with "it is not the
case that..." (and other logical terms, such as the existential
quantifier) constructively understood. It would then be in order to give
the usual reductio proof in order to show that the square root of 2 is
irrational; and your distinction between the two schematic proofs above
would be to no purpose.

I was taking the distinctness or difference of x and y to be a
logical notion, expressed by the usual formula

	not(x=y).

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))).

Neil Tennant