[FOM] Classical logic and the mathematical practice

[Andrej Bauer]

I really do not wish to repeat old discussions about classical logic,
but I feel compelled to respond to Arnon Avron's reasons for preferring
classical logic, as they propagate the usual misonceptions about
constructive mathematics. Since this is a political debate the winner is
the one who has the last word. I am hoping the moderator will close the
discussion after my post :-)

Arnon gives the Intermediate value theorem as an example of a
classically valid theorem which he does not want to give up. He bases
his conviction on the inutitive idea that continuous functions are the
sort of things one can draw on paper without lifting the pen.

First, I should say that there are many continuous functions which are
far from the sort of thing that people imagine drawing. First year math
undergraduates usually imagine that continuous functions are something
like piece-wise differentiable functions--which is closer to what humans
actually imagine and draw. (It is important here what humans imagine
because we are talking about intuitions on which mathematical
convictions are based.) For many restricted classes of continuous
functions there are constructive versions of the Intermediate value
theorem. And usually the problem is not that the zeroes might not exist,
but rather that there might be too many to choose from! In summary, I am
not so sure Arnon's example is a good one to argue against constructive
mathematics.

Second, there is a constructive Intermediate value theorem saying that
one can get "arbitrarily close to an intermediate value". From many
points of view (computer science, physics) this is a very sensible
theorem, because it is in accordance with actual practice of computing
intermediate values.

Third, when a constructive mathematician reads the Intermediate Value
Theorem, his understanding of "there exists an intermediate value" is
"we can compute an intermediate value". Even classical numerical
analysts will tell you that having (classical) existence of a zero is
one thing, and actually computing it is another. A lot of
misunderstanding of constructive mathematics comes from the fact that
the language of constructive and classical mathematics is the same, but
the meaning of the words is different.

Finally, Paul Taylor wrote a paper about the intermediate value theorem
(and other aspects of real analysis) in a constructive setting, which
gives a fresh view on these matters and may be of some interest to this
discussion. The paper can be found at
http://www.cs.man.ac.uk/~pt/ASD/#ASD/lamcra

Best regards,

Andrej