[FOM] Intuitionists and excluded-middle

[Arnon Avron]

> > 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. Will intuitionists
reject the intoduction rules for i-or only because making the inference of 
"2+2+4 i-or 2+2=5" from  "2+2=4" is not a very useful thing to do? 
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?).

  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).

  Let me add also that saying that "obviously this proof says "nothing"
about the desired solution x" is a  big exaggeration. Will a police
investigator who got data which reduces the number of suspects from
5 to 2 (to say nothing of reducing it from infinity to 2!) discard
that data as useless???


Arnon Avron
of this theorem