[FOM] Intuitionists and excluded-middle

[Lew Gordeew]

Arnon Avron wrote:
>>> Despite of almost 100 years of desperate attempts, they have failed to
>>> provide any convincing argument for rejecting excluded middle (except
>>> "Because I say so").
>>
>> 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.
>>  
>> PROOF. Suppose sqrt(2)^sqrt(2) is rational. Then take x:=sqrt(2).
>> Otherwise, take x:=sqrt(2)^sqrt(2); hence x^sqrt(2) =
>> sqrt(2)^(sqrt(2)*sqrt(2)) = sqrt(2)^2 = 2 - a rational.
>> Q.E.D. by the law of excluded middle.
>>  
>> Now obviously this proof says "nothing" about the desired solution x. 
>
> I find this "convincing argument" very strange indeed. First, we were
> talking about the logical validity of excluded middle, not about its
> usefulness. Second, the fact that *some* applications of a law *might*
> be useless is certainly not a reason to reject it.

Logic validity itself is rather academic a matter (actually I prefer
Lukasiewicz's fuzzy validity), but the laws of deduction are regarded
universal for the whole mathematics. Now mathematics prefers constructive
solutions, so if LEM as a law of deduction can't fulfill natural
mathematical expectation of constructivity then it can be characterized as
quasi-useless. Of course there are various -- some more, some less
"militant" --  types of rejecting usefulness of this or that tool ... 

> Third, excluded middle is an extremely useful rule, used in proofs of
> many central theorems of Analysis, like the *classical*
> intermediate-value theorem, the theorem that any continuous function on
> a closed interval has a maximum, etc (yes, I know that intuitionists
> have alternative proofs to a sort of alternative theorems, but reading
> these alternatives only makes it clear what a useful principle excluded
> middle is!). Moreover:
> excluded middle is used even in simple definitions of Analysis.
> Thus the defintion of the useful function \lambda x. sgn x (which the
> intuitionists do not accept as well-defined) relies on excluded middle,
> and so does the definition of the extremely useful \lambda x.|x|
> (-x if x< 0, x otherwise. Here I guess that the intuitionists have
> some "alternative" strange definition. So what?).

Surely, in most cases it is useful. But there are also exceptions, as above.
So it all depends on the underlying evaluation of 'law' - should it be
universally valid or not? If we agree to admit that exceptions are always
legitimate, then you are right. Otherwise, you are wrong. Or else -- 
rejecting LEM! -- we are both somewhere in the middle. :-)

> Finally, and perhaps most importantly, I find the proof you quote
> above as a good example how *useful* excluded middle is! In fact, the
> theorem you mention is not very interesting. What is interesting is
> the existence of two irrational numbers a, b such that a^b is rational.
> This fact has real g.i.i. because it is a good example that our
> intuitions might mislead us. But it is only the *existence* of such a, b
> that is interesting. The exact identity of them is not important at all
> (to me, at least).

But this is very important for most mathematicians. Most students of
mathematics immediately ask "hey, but which x is the solution - sqrt(2) or
sqrt(2)^sqrt(2)?" Now Analysis says it is sqrt(2)^sqrt(2), but clearly the
LEM proof does no good to this end. I must confess though that our comp sci
students are less concerned with the answer because they don't know much
about irrational numbers. :-) :-(

Regards,
LG

-- 
Lust, ein paar Euro nebenbei zu verdienen? Ohne Kosten, ohne Risiko!
Satte Provisionen für GMX Partner: http://www.gmx.net/de/go/partner