Boise, Idaho, 9 Nov.
It is a privilege to be able to insert occasional annotations into
deBruijn's remarks from the standpoint of what he calls an
A-Platonist.
DB:
Eindhoven, 9 November 1994.
Dear QED,
The interest in philosophical problems arrising in the QED
discussion is quite remarkable, and enjoyable. Some of the items are
very essential for the structure of QED, but on top of that there are
items which are psychologically valuable without having consequences
for the way we do our work.
Holmes: It certainly is fun to talk about it. I'm interested in
seeing what it has to do with how QED is implemented.
[...]
DB:
straightjacket. It would be quite something else if the two authors
would disagree on the mathematical basis, on the derivation rules or
on the style in which the paper has to be written, on what to
consider important, what as interesting, what as beautiful.
Holmes: It is interesting to explore the ground which makes us all
believe that practical agreement on this level is possible between
people whose _fundamental_ views as to what is going on are apparently
completely different. This is relevant to QED, since the possibility
of agreeing on one system rests on this phenomenon.
DB:
I think that the larger part of the discussion on the role of
intuition belongs in the category of "emotionally valuable but
irrelevant for QED".
Holmes: Agreed.
DB:
There appears to be quite some interest in Mathematical Platonism.
In the discussion I note some different ideas about this, quite far
apart. Let me give them names.
A-Platonism is the opinion that our mathematical objects have a
real existence in some real world.
Holmes: I would only modify this to say _the_ real world.
DB:
B-platonism is the idea that there is, or there should be, a fixed
basis for mathematics, and that such a basis will be satisfactory for
ever.
Holmes: I don't agree with this at all! (i.e., I'm not a B-Platonist!)
DB:
C-platonism is the idea that mathematics should be described in a
fixed object language. Metalanguage (called "syntactic") should not
be allowed in the bag of proof tools. The idea to label this point of
view as platonism was expressed by David McAllester in his email of
27 Oct 94; I had never seen it before.
Holmes: Nor am I a C-Platonist! (see below)
[...]
I suppose that we all agree that A-platonism is irrelevant for
QED. And I think that many people will admit that A-platonism is a
bit dangerous as well. It makes believers believe that there is no
need for an absolute level of accuracy. Their idea may be that for
the time being they can get away with sloppy definitions. They might
believe that whenever any hard question comes up they can inspect the
objects a bit closer and adjust the definitions a bit.
Holmes: This phenomenon goes on, but I'm not sure it correlates so
closely with explicit A-Platonism. I would say "How can I inspect the
objects closely without using the definitions?" -- this is analogous
to allowing our belief in the reality of the stars to weaken our
commitment to looking at them carefully with our eyes.
[...]
There is a stronger form of A-platonism: the idea that in the real
world of mathematical objects there is an absolute notion of truth,
even for cases which will always remain undecidable for human beings.
A-platonism is the idea that when we are talking mathematical
language, we talk ABOUT something. That "something" is called real
by A-platonists, imaginary by others. With metalanguage this is
different, since metalanguage talks about the texts in the
language, and those texts can have an actual existence in a
physical sense. They can be recorded in the physical world (like on
a magnetic disk); retreiving them we get them back in the original
form. So when we talk about the mathematical texts instead of about
the mathematical objects, it seems quite reasonable to be
platonistic. This is so trivial that it is hardly worth while
mentioning.
Holmes: I don't think this is trivial at all. Reasoning in
metalanguage can involve "texts" which cannot be produced physically
at all; certainly there are no restrictions on reasoning in
metalanguage which respect physical feasibility of production of texts
(in most work in this field, at any rate). I maintain that for
metalinguistic reasoning of a classical type we need at least the
degree of Platonism which regards the natural numbers as real, and
probably somewhat more than this. Of course, metalinguistic reasoning
supporting QED might have to take feasibility into account!
DB:
[...]
And even if we believe in the possibility, should we take a
particular fixed system as the base for the QED system? A serious
alternative is the idea of the very liberal Automath Restaurant.
Believers in B-platonism can eat there without any trouble.
Is it possible to do mathematics without believing in
B-platonism? Could one really turn oneself into a Relativistic
Mathematician? I think one can. One can get into any kind of mood
by just trying long enough.
Holmes: Even A-Platonists can be relativistic mathematicians; I am.
DB:
The matter of C-platonism seems to become more and more important
these days. I think it has to be a key item in the discussion about
what a proof is.
Using pieces of metalanguage or metatheory can work wonders.
Nevertheless it should be admitted that in many cases it is not
essential, just a matter of making proofs faster and shorter.
Quite often the ideas used in the metalanguage can be pushed back
into the language, but even if it might be true that this reduction
is always possible one might ask whether it will always be
manageable.
I think that during the 20th century most logicians and mathematicians
(including myself) have been in favour of C-platonism, but this may
change. If methods different from our traditional proof rules will
still give satisfactory confidence, why fight rear-guard actions?
For non-mathematical customers it is confidence that counts, not
formal proof.
Related to the matter of C-platonism is the use of computer
programs. If a mathematical fact is established by the execution of a
computer program for which a correctness proof is available, we may
have a very strong confidence in the correctness of the result, and
yet we have to admit that we have not produced a proof according to
our proof rules. This is different in those cases where there is a
program whose execution actually produces a formal mathematical proof
in terms of our own proof system, a proof that can be computer-checked
in the next stage. In such cases the correctness proof of the program
plays no role any more.
Holmes: I think that one is dealing with Platonic reality in
meta-linguistic reasoning as much as in reasoning within an object
language. Wouldn't it be the case that if we have a _constructive_
correctness proof for the correctness of this computer program, we
would be able to produce a computer proof in our system for the
disputed result? But, of course (here's where one's ontological
commitments come into play) even a constructive proof might not be
computationally feasible: I the Platonist may be convinced by a proof
that there is a QED checkable proof of theorem X with 10**10**100
steps that theorem X is a theorem acceptable to QED, while another
customer of QED might not be convinced of this at all. Another
customer might be convinced by the aforementioned proof if it comes
with an algorithm for constructing all 10**10**100 steps of this proof
(of course, we do not have the budget to actually print it out :-( ),
while the most conservative customer would not admit the existence or
relevance of any proof whatever with 10**10**100 steps :-)
DB:
N.G. de Bruijn.
Holmes (his most radically Platonist signature, not to be taken too
seriously):
And God posted an angel with a flaming sword | Sincerely,
at the gates of Cantor's paradise, that | M. Randall Holmes
the slow-witted and the deliberately obtuse | Boise State U. (disavows all)
might not glimpse the wonders therein. | holmes@math.idbsu.edu