FOM: on constructivity

[William Tait]

Ii was a pleasure to read Dirk van Dalen's remarks on constructivity; 
but I have some comments.


>1.    All of mathematics has ultimately to be based on more than a mere
>formalism (unless one is a hard-core formalist).  For a platonist it is the
>interplay between the mathematical reality and human cognition, for the
>constructivist it is human (mental) constructive activity.


Rather than saying that, for the platonist, mathematics is based on 
the interplay between mathematical reality and human cognition, I 
would rather say that, for the platonist, mathematics is *about* 
mathematical reality. But for a constructivisdt, too, mathematics is 
about mathematical reality. e.g., natural numbers, numerical 
functions, etc.---and *proofs*. Clearly both classical and 
constructive mathematics are in one sense `based on human (mental) 
constructive activity'; but I hope that Dirk does not want to claim 
that constructivist propositions which are ostensibly about numbers, 
proofs, etc., are really disguised statements about our activity.

>2. ... Martin-Loef's type theory (and typed lambda calculus) have turned
>this founding of logic on constructions into a systematic practice.

I would rather cite Curry-Howard here for the basic insight---along 
perhaps with Lauchli.

>3.  ...  Ever since Kleene, Goedel and Kreisel we
>have a number of specific proposals for `construction', which all have their
>computational or proof theoretical virtues.


Kreisel's proposal, suggested originally by Goedel and pursued e.g. 
by Nick Goodman, was for a type-free theory of constructions. This 
seems to have been largely abandoned in favor of the Curry-Howard 
type theory.


>4.    By grounding Logic on `constructions' one has put the burden of truth,
>arguments, ... back where it belongs: in mathematics.  Now it is a matter of
>conviction, introspection, or whatever one wants to call it to find acceptable
>principles.


This grounding of logic is not special to constructive logic, but is 
an equally valid way of thinking about classical logic. It is 
entirely consistent with the classical point of view that the only 
warrant for a mathematical proposition is a proof.


>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?

>Since, however, many classical existence theorems can be refuted in
>intuitionistic or recursive mathematics, this rule of the thump does not
>really help.  Here one really needs refined proof theoretical arguments to see
>if there are suitable transfer results.

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.Leaving aside the more exotic features of Brouwer's 
theory of choice sequences, his whole theory of analysis is perfectly 
intelligible classically.

Certainly, there is nothing proved in Bishop-Bridges which is not 
classically true.

>7. The choice of constructive principles is a matter of personal
>conviction (or convenience).  Bishop has sound arguments for a minimal
>constructivism, but there is nothing wrong with adopting particular
>constructive principles, or objects.  After all, even a constructive
>mathematician has an obligation to explore his mathematical universe.
>There is a similarity with, say, platonism.  A set theorist considers
>arguments for certain objects, e.g. large cardinals.  A constructivist may
>look for arguments for certain real functions, or natural number sequences.
>

Presumably the reflection principles of Martin-Loef correspond to 
some (small) large cardinal axioms.


>8. ...pragmatic constructivism in the sense of Kreisel's 'unwinding 
>proofs', the
>analysis of ordinary classical proofs and procedures, as practiced, for
>example, very successfully by Luckhardt and Kohlenbach. This branch of
>constructive mathematics/logic is legitimate mainly on the basis of 
>its success.
>It is a wonderful program, but it belongs to another tradition.

The tradition of the (extended) Hilbert's program, although the 
pragmatic element is certainly due to Kreisel..

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. The rest is metaphor and hot wind. Where one thinks one sees 
a philosophical ground distinguishing them, e.g. Dummett's argument 
based on the analysis of meaning, it is just bad philosophy.

This is not, of course a challenge to the virtue of having 
constructive existence proofs, yielding algorithms.

Bill Tait
-- 
William W. Tait
Professor Emeritus of Philosophy
University of Chicago
wwtx at midway.uchicago.edu
Home:
5522 S. Everett Ave
Chicago, IL 60637
(773) 241-7288