[FOM] Intuitionists and excluded-middle
hendrik at pooq.com
Wed Oct 12 17:23:40 EDT 2005
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,
More information about the FOM