[FOM] Intuitionists and excluded-middle

[Ritwik Bhattacharya]

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. 

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.

Ritwik