[FOM] Intuitionists and excluded-middle

[Hendrik Boom]

On Wed, Oct 12, 2005 at 09:40:00AM +0300, praatika at mappi.helsinki.fi wrote:
> Lew Gordeew <legor at gmx.de> wrote:
> 
> > A conventional convincing argument: mathematical proofs using the law of
> > excluded middle might be "useless". Here is a familiar trivial example
> > (quoted by A. S. Troelstra, et al).
> > 
> > THEOREM. There exists an irrational real number x such that x^sqrt(2) is
> > rational.
> 
> 
> I must say that I find such talk of uselessness quite ... well ... 
> useless. To begin with, why should one require that pure mathematics, 
> which is theory building, has to have some use. The general requirement of 
> usefulness of all scientific theories would certainly paralyse science. 
> And certainly uselessness of some piece of knowledge does not make it 
> unjustified or not true. 
> Moreover, it is not clear exactly how the possession of a particular 
> solution is so much more useful... 
> Further, from a theoretical point of view, such a non-constructive proof 
> may be very useful in refuting an universal hypothesis, e.g. "For all x, 
> if x is irrational, then x^sqrt(2) is irrational." Finally, I think that 
> such proofs are quite useful in suggesting that it may be fruitful, and 
> not vain, to search for a particular solution, and a constructive proof.
> (In the standard systems, if the theorem is Pi-0-2, there is one.) 

It's the non-constructive existence that was considered useless, viewed as
not actually proving existence.  The argument can easily be converted to
a constructive one that refutes "For all x, if x is irrational, then
x^sqrt(2) is irrational."

Suppose it were true.  Then sgrt(2)^sqrt(2) is irrational.  Thus
(sqrt(2)^sqrt(2))^sqrt(2), i.e.2, is irational. => <=

The reasoning is shorter, intuitionistically acceptable, and as useful
for your purposes,

-- hendrik