FOM: on constructivity

[Fred Richman]

William Tait wrote in response to van Dalen:

[van Dalen]:

>> 6. ...  What is the use of a classical existence theorem?  Hermann
>> Weyl put it as follows, "it is an incitement to look for a
>> constructive existence proof".
 
> Is it impossible that, for example, there could be a classical but no
> constructive proof of an existence statement yielding an algorithm?

I'm not sure this counts, but there are classical proofs of the
existence of an algorithm with no corresponding constructive proofs in
sight. Given any statement P, there is a classical proof of the
existence of a (primitive recursive) function f such that f(n) = 1 for
all n if P is true and f(n) = 0 for all n if P is false. Hartley
Rogers gives an example of this type in "Theory of recursive functions
and effective computability", with a footnote about excluded middle,
constructivity, and intuitionists.

This classical existence result is uninteresting although a
constructive proof, for certain statements P, might be very
interesting. I would guess that Weyl had more substantial classical
results in mind.
 
> Recursive and constructive mathematics are two different things.
> There is a counterexample to e.g. the intermediate value theorem in
> recursive mathematics. I don't know of any classical theorems that
> are constructively refutable. Brouwer liked to give such examples:
> e.g. every function on the unit continuum is uniformly continuous.
> But his continuum was a different object from the classical one and
> so there is not a refutation here of a classical result, but simply
> an ambiguity.

For some reason I can't resist commenting on this although I believe
that I am basically in agreement with the attitude toward recursive
mathematics, constructive mathematics, and intuitionism expressed
here. What bothers me is the idea that classical theorems are
irrefutable short of showing that classical mathematics is
inconsistent. In particular, that Brouwer's proof that every function
is uniformly continuous (which I am no fan of) is explained away by
saying that his continuum was a different object from the classical
one. Be that as it may, I believe that Brouwer's point here was not to
introduce a new continuum but to describe more accurately our common
intuitive notion of a continuum. This was a rival theory of the same
thing, not a theory of something else. I think that the same can be
said of recursive mathematics in the spirit of Markov.

> My challenge: I would suggest that the distinction between
> constructive and classical mathematics lies not in `philosophical'
> conceptions of mathematics, alien to one another, but simply in the
> fact that the latter and not the former employs the law of excluded
> middle.

I think that's accurate. The problem seems to be the normative aspect.
On what basis does one choose to do mathematics with or without the
law of excluded middle? The facts on the ground are that very few
mathematicians see any point in doing without. That might be taken to
reflect a certain philosophical conception of mathematics.

--Fred