[FOM] Intuitionists and excluded-middle

[Alexei E Angelides]

Quoting Jesse Alama <alama at stanford.edu>:

> Andrej Bauer <Andrej.Bauer at andrej.com> writes:
>
> > P.S. What is the best way to prove constructively that sqrt(2) is
> > distinct from every rational? The usual classical proof only shows that
> > sqrt(2) is _not_ rational? (Note that x is distinct from y
> > constructively if there is a rational in between.)
>
> Isn't the usual classical proof also "constructive"?  We begin by
> assuming that sqrt(2) is rational and get a contradiction; so we can
> conclude, even in a constructive setting, that it is not the case that
> sqrt(2) is rational.  Where does the proof fail to be constructive?
> (Is it the move from "it is not the case that sqrt(2) is rational" to
> "sqrt(2) is irrational"?)
>
> Jesse

I don't think so. In a constructive proof, one must find or specify an
object that has a certain property by using a method for finding or
creating (an example of) such an object with that property.

Hence, to a constructivist, assuming that an already given object does not
have some property and then deriving a contradiction does not show that it
has some other property (or the negation of the property it was assumed to
have). Such a proof merely shows that it does not have the property we
assumed it to have.

Consider, as an analogy, another classically non-constructive argument:

By definition, a transcendental number is a real number that is not
algebraic. The set of real numbers is uncountable. But the algebraic
numbers are countable. Hence, there must be some real numbers that are not
algebraic. By definition, these are transcendental.

The above proof fails to be constructive because we have not exhibited a
method for finding or creating a transcendental number.

One might reformulate Bauer's question as follows: what is the best way to
exhibit that sqrt(2) is not equal to each rational. A constructivist would
have to begin the answer with: it is to exhibit a method by which we can
find every rational number to be distinct from sqrt(2).

Alexei Angelides