FOM: on constructivity

[Prof. dr. D. van Dalen]

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

        It was an even greater pleasure to see Bill Tait's comments.

        I will distribute some comments on comments below.


>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 constructivist, 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.

+++++++++++++++++++++++++++++++++++++++++++++++
--1.  Tait's claim "platonist mathematics is 'about' mathematical reality"
avoids the so-called "interplay between mathematical reality and human
cognition", but it leaves open what and where platonist mathematics is.
Is it purely a formalism describing mathematical reality, or takes it place
in our thoughts (and is subsequently described in some language)?

--  Constructivists indeed argue about the mathematical universe.  Here one
has to make some distinctions: a platonist constructivist would argue about
the objects in the platonist universe, and stick to 'constructive'
procedures and arguments.  The more intuitionistically inclined
mathematician would argue about the intuitionistic universe, which differs
in various respects of the platonist universe, (e.g. it is open ended,
allows dynamic objects (choice sequences, etc.), and which is 'home made'.
So the latter kind of constructivist deals with objects she constructs
herself. (warning: already the natural numbers involve a high degree of
abstraction, think of Brouwer's "empty two-ity").
+++++++++++++++++++++++++++++++++++++++++++++++

>2. ... Martin-Löf'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.

--2. Point taken, that was actually what I meant by  typed lambda calculus.

>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 Gödel 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.

+++++++++++++++++++++++++++++++++++++++++++++++
--4. 3.  On the grounding of constructive and classical logic:  Tait is
quite right.  The distinction is 'what proofs'?  The constructivist
identifies conceptual proof with constructions, whereas the classical
mathematician identifies 'proof' with 'derivation' in a suitable system.
But even if he chose to operate in an intuitionistic calculus he would, to
quote a quote of Kreisel, 'do the right thing for the wrong reason'.
+++++++++++++++++++++++++++++++++++++++++++++++


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

+++++++++++++++++++++++++++++++++++++++++++++++
--6. This was answered by Richman.  It shows that the question has to be
refined.  For lots of intuitionistic formal systems  T, the classical
version  T^c  and T  have the same provably recursive functions.  But that
does not answer the 'absolute' question' : are the classes of classical and
intuitionistic (say, numerical) algorithms the same?'. It would be good to
know some more about this matter.
+++++++++++++++++++++++++++++++++++++++++++++++

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

+++++++++++++++++++++++++++++++++++++++++++++++
--4.  On existence theorems and classical, recursive, intuitionistic math.
(i)  Bishop-Bridges was specifically designed to be a neutral part of both
classical and constructive versions of mathematics. So Tait is right by
definition.
(ii)  The refutation of classical theorems in versions of constructive
mathematics follows from the fact that they have their own mathematical
universe, which forces another logic onto them.  This is something one has
to live with; after all Brouwer's choice sequences are no more exotic than,
say, large cardinals.
I guess Tait has a constructive mathematics in mind, which is a subsystem
of classical mathematics.  For such a universe one can formulate
constructive results, e.g. a continuous function on a close interval has an
infimum, (i.e. the infimum is algorithmically computable), and refutations,
e.g. there are continuous functions on [0, ], for which no algorithm
computes the minimum.  But Brouwer's theory of analysis is indeed
intelligible only of one dismisses some of its characteristic principles.
This probably comes to adopting the Bishop-Bridges viewpoint.
The point to be distinguished is that intuitionistic mathematics is
dictated by a particular philosophical viewpoint.  The nature of the
continuum and its total functions is an intrinsic feature of intuitionism.
As Tragesser has pointed out in his FOM letter the 'flowing' character of
the continuum is a key-feature of intuitionism, and a thing that Brouwer
wanted to incorporate at any cost.  So an intuitionism without choice
sequences would fall short of the conceptual intentions.

The historical  point is that  in the twenties people saw intuitionism as
an impoverished classical mathematics, and hence a classical existence
proof could be hoped to point to an effective existence proof (Weyl).
However, the Brouwerian counterexamples already showed that  classical
existence theorems failed in an intuitionist setting.
+++++++++++++++++++++++++++++++++++++++++++++++

>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-Löf 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.


+++++++++++++++++++++++++++++++++++++++++++++++
-- 8.   I grant Tait that his no-nonsense approach has its attractions, but
in the end everyone has to make up her mind about the nature of
mathematical objects.  For those who don't like philosophical reflections
on the mathematical universe, there is enough to be done without making
choices, but if has to make a choice, Brouwer's approach is a perfectly
coherent one, certainly not inferior to the classical viewpoint.

To define constructive mathematics as 'classical mathematics minus the law
of the excluded middle' is fine as a rough rule of the thump.  The problem
is that one would have to make up one's mind about the multitude of
intermediate principles.  Moreover it denies the constructive mathematician
any characteristic constructive mathematical principles.  Perhaps it would
be closer to Tait's intention to say that classical mathematics is
constructive mathematics plus the law of the excluded middle.  That would,
however, put the burden on constructive mathematics.
+++++++++++++++++++++++++++++++++++++++++++++++

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)