[FOM] Formalism/Platonism

[Harvey Friedman]

I would like to start a thread here on the FOM in which

1. Descriptions of various kinds of formalism and Platonism are spelled out
and analyzed.

2. Arguments for and against these positions are spelled out and analyzed.

3. New research projects suggested by 1,2 are spelled out, and perhaps to
some extent carried out.

Formalism/Platonism is an old classical topic, but I believe that when
considered in the light of modern f.o.m., this can be very fruitful.

I think we should first try to deal with extremes of the two. Let us call
them ultraformalism and ultraplatonism.

In the interests of productivity, I don't think we should - at least at
first - say too much about formalist positions that are so extreme that they
deny any sense to the meaningfulness of, say, bit strings of length 2, or
for that matter, bits. Or deny any sense to standard mathematical discourse
about bit strings of length 2, say with the use of the connective "and".
That may already be interesting, but is so different than what happens when
you accept a very minimal amount of apparatus that it would make the
discussion too unfocused, too unruly, and probably totally unproductive.
Such truly extreme positions are far beyond those taken by anyone publicly
on the list, including Sazonov.

So the framework that I am thinking about for spelling out kinds of
formalist positions is reasonably standard. There is an acceptance of the
objectivity of lots of mathematical statements about lots of mathematical
entities. Perhaps not too many statements about too many entities. But
nonetheless a good healthy number.

The general formalist idea is that, beyond a certain amount - perhaps
minimal amount - of very concrete contexts, mathematics becomes a kind of
game with prescribed rules in the form of formal systems. Under this view,
mathematical activity  - in the sense of finished mathematical productivity
- consists only in episodic announcements that one has "won the game" in the
form of having a derivation of some formalized statement or other, and
particularly when pressed, actually producing the claimed derivation in
print or nowadays, by electronic communication. Under the formalist view,
the mathematical record consists of such produced derivations.

Under the formalist view, a conjecture is nothing more than a prediction
that someone will be able to find a derivation of the associated
formalization within the prescribed rules - within some prescribed amount of
time.

Note that if we all agree on what the prescribed rules are, then it is not
clear whether there is any practical difference between the formalist and
the non formalist (a non formalist may or may not even have a position, may
or may not be a Platonist, etcetera). It would seem that both would operate
the same way. 

However, this is not quite true. The formalist and the non formalist are
likely to differ about what they think is important to get derivations of.
This point has previously been made on the FOM by John Steel.

So I would like to pin this down. Steel, a card carrying ultraplatonist, is
deeply interested in certain mathematical questions that do not seem to be
so easily characterized in terms of playing a game. E.g., Steel is
interested in the continuum hypothesis. He is not interested in working on
the continuum hypothesis in any particular formal system, as the formal
systems that Steel is interested in are well known to leave the continuum
hypothesis untouched.

Instead, Steel is interested in settling the continuum hypothesis - although
this is not his main research interest at the moment. This seems to defy the
model of mathematical activity that the ultraformalist has. So perhaps the
ultraformalist would say that this research interest of Steel's is
meaningless? incomprehensible? wrong-headed? what?

Steel is also interested in settling the relationship between various large
set theoretic statements; e.g., strongly compact cardinals and supercompact
cardinals. E.g., 

is ZFC + "there exists a supercompact cardinal" interpretable in ZFC +
"there exists a strongly compact cardinal"?

This is an arithmetical statement that Steel suspects is decided within very
weak fragments of PA, so weak that even Sazonov would almost certainly
accept a likely proof of this statement or its negation.

QUESTION: Does Sazonov accept the proof that, e.g., ZFC is interpretable in
ZF? 

However, as Steel suggested in his recent posting, maybe the crucial
difference between he and Sazonov is that Sazonov would be very
disinterested - on principle - in a question like

is ZFC + "there exists a supercompact cardinal" interpretable in ZFC +
"there exists a strongly compact cardinal"?

regardless of how concrete the (proof of the) answer is.

One challenge to the ultraformalist is: how are we to choose the 'rules of
the game'? On what basis? Have you, the ultraformalist, accepted the 'rules
of the game', or at least some of the rules of the game, and in what sense
accepted?
 
I am not a Platonist. I am not a formalist. I am an investigator.

For me, the crucial issue is: what kind of work in f.o.m. will shed light -
not necessarily settle - this dispute? Or at least, what kind of work in
f.o.m. will be deeply relevant to this dispute?

Fortunately I think I have some promising ideas about this. But I will stop
here to see how things progress.

Harvey Friedman