[FOM] Intuitionists and excluded-middle
ritwik at cs.utah.edu
Wed Oct 12 17:02:20 EDT 2005
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
> 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.
Ah, but the argument being made was that the *proof* might be useless,
not that the theorem itself was useless. So nobody is suggesting that
mathematics/mathematical "facts" need to have use, but a proof, by
definition, must have the "use" of convincing the reader of the proof.
> Moreover, it is not clear exactly how the possession of a particular
> solution is so much more useful...
Quite simply because it is far more convincing, in this case, to have in
hand a number of the type that the theorem claims there exists, than to
have a purported 'proof' of the existence of such a number.
> 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.
This is true, and I agree that such proofs do have this use.
More information about the FOM