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.
For example, two people can write a paper together, where the
first one believes that the results aleady existed and are just now
being discovered, whereas the other one believes that everything is
created on the spot for the first time. Or, the first one may be
working in the spirit of Love for Nature and Absolute Truth, and the
other one may just be driven by the desire to get a better rating in
the Citation Index in a scientifically honest way. In spite of the
different basic attitudes, the collaboration can be fine, and it
should not be tried to push the two into a common philosophical
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.
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".
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.
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.
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.
There may be many more definitions of platonism. One definition
I've seen is that a Platonist is someone who accepts the natural
numbers plus power set axiom plus a general comprehension axiom.
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.
The claim has been made that A-platonism agrees with the
psychology of the mathematicians: during their work they imagine that
the things they are talking about are real objects. Indeed, there are
such emotions, but these are essentially the same feelings that a
novelist has when writing imaginary stories about imaginary people
and imaginary situations. An essential difference is that the
mathematician may even be cheating: he starts with some assumptions
that he wants to disprove, in the course of the argument he constructs
objects, treats them psychologically as existing things, until at the
end a contradiction is reached and the whole edifice falls into
pieces. (This cheating is a point I miss in the Podnieks' chapter.)
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.
B-platonism is by no means irrelevant for QED. It calls for
action: if we believe in the possibility of a fixed basis for
mathematics, what should it be? The word possibility has both a
mathematical and a social meaning here.
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.
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.
N.G. de Bruijn.