[FOM] Intuitionists and excluded-middle
Neil Tennant
neilt at mercutio.cohums.ohio-state.edu
Sun Oct 23 16:54:32 EDT 2005
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
More information about the FOM
mailing list