FOM: on constructivity

[Prof. dr. D. van Dalen]

There has been a drawn-out discussion on the nature of constructive
mathematics.  Although Richman has already pointed out a number of salient
points, let me try to give a few comments that might be clarifying.

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.
2.    Constructivists acknowledge the role and usefulness of logic and
language for mathematical purposes, be it under a constructive
interpretation.  This interpretation is basically the
Brouwer-Heyting-Kolmogorov proof interpretation.  That is: the ground for
asserting a mathematical statement  A  is a proof (or construction) for  A,
("a : A") . Martin-Loef's type theory (and typed lambda calculus) have turned
this founding of logic on constructions into a systematic practice.
3.  "Construction" is an open-ended notion for constructivists, it is not
fixed in some calculus forever.  Ever since Kleene, Goedel and Kreisel we
have a number of specific proposals for `construction', which all have their
computational or proof theoretical virtues.  One might,  e.g., say  "a : A"
means in a certain context "a realizes A".
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.  Examples are Markov's Principle, Church's Thesis, Brouwer's
Continuity Principle.
5.  Since intuitionistic logic is sound for the proof interpretation, that
basic part of logic is acceptable to all constructivists.  Completeness is a
matter of a philosophical nature, it depends on the semantics and meta
principles.
6. One has to be careful about semantical arguments, as there is a host of
semantics.  Moreover, a constructivist needs to argue constructivity in and
about his semantics.
\item
  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".  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.
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.
8. So far I discussed 'constructive mathematics' as a doctrine, or a
foundational
program. There is, of course, a modern variant that does not worry about such
issues as 'conceptual basis' or 'origin of mathematics'. That is the part of
logic (and computer science) dealing with feasibility and complexity, and
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.

Prof . Dr. D. van Dalen
Department of Philosophy
Utrecht University
P.O. Box  80.126
3508 TC  Utrecht     The Netherlands
tel. 030-2531834, fax 030-2532816
030-6663857(home)