[FOM] Platonism and Formalism

[Karlis Podnieks]

I will try to represent the most extreme formalist point of view, filling in
the f.o.m.-ism questionaire set up by Harvey Friedman
(http://www.cs.nyu.edu/pipermail/fom/2003-September/007352.html).

As the main principle, the formalist philosophy allows investigation of any
formalizable theories, independently of what some other people might think
of their "truth". Of course, not all theories of this kind are worth of
investigation. How do we select? The most popular criteria:  a theory should
be useful, fruitful, beautiful, successful, etc. Such "-ful" theories are
not meaningless - normally, they have some vision (intuition) behind. But
these visions never possess an absolute value, they are corrected and
refined during their formalization. And after formalization, the axioms can
be modified - even irrespective of any visions (just for experiment etc.).
Usually we develop new visions (intuitions) according to these
modifications.

High level f.o.m. and low level f.o.m.

This process of setting up mathematical theories is an essential aspect of
real mathematics - currently, disregarded in most discussions about f.o.m.
(Corfield). I would call investigation of this aspect the "high level
f.o.m." - in contrast to the traditional "low level f.o.m." where we are
trying to explain the nature of mathematics and its unique position among
other branches of science. Accepting formalist philosophy does make high
level f.o.m. less interesting.

Kripkenstein's argument (as put by Timothy Chow)

I think that extreme formalists, who are (of course) baffled by "the
standard model of N", must be equally baffled by the concept of "rules". If
you present your 10 page proof of your new theorem, then I could (perhaps)
verify its correctness as a referee. If your computer would propose a 10
billion character proof of Goldbach's Conjecture, then my computer could
verify its correctness. Of course, it would be good to verify also the
correctness of my proof verification program... But, if we wish to have more
than this (for example, if we wish to discuss consistency, completeness,
etc.), then we arrive to the same baffling very theoretical concept of the
induction rule. Consistency cannot be verified empirically, it could only be
proved theoretically. But, saddly enough: such theoretical consistency
proofs can be only relative, not absolute (my interpretation of Godel's
Second Theorem).

Thus, the extreme formalist philosophy, as presented above, is, in fact,
trivial. Is this why most people do not wish to accept it?

Now, the questionaire.

2) For me, accepting the extreme formalist philosophy makes the world of set
theory more colorful. Of course, a formalist may follow the mainstream (ZFC,
ZFC + there is an inaccessible cardinal, ..., ZFC + there is a measurable
cardinal, ..., ZFC + there is a contradiction). But, in parallel, a
formalist may also investigate seriously (at least) ZF+V=L and ZF+AD as
well. From my sideview point, these new "worlds of sets" look even more
interesting than the older mainstream "world".

Formalism and real mathematics? Formalists not only accept using computers
ir mathematical proofs as a normal behavior. I believe that future
mathematical proofs will contain an ever growing percentage of
computer-aided steps. To remain competitive, mathematicians should not
ignore this trend (remember the sad history of chess playing...).

3) Formalists are regarding as very valuable the relative consistency proofs
(like, Con(ZF)->Con(ZF+V=L)), and proofs that some consistency proofs are
impossible (like Con(ZF) does not imply Con(ZFC + there is an inaccessible
cardinal)). Why? As a necessary guidance in the world of possible axioms.

Yes! An extreme formalist would be pleased by a contradiction found (best of
all) in PA (but ZFC + a measurable cardinal also will do). It would destroy
the vision behind PA ("the standard model of N", finally!). But it would not
mean the end of mathematics. It would mean only that we must improve the
axioms... Why do we need believing in advance that PA is consistent?

And, of course, formalists are regarding as very valuable the projects of
computer-aided formalized mathematics (see the Mizar project at
http://mizar.uwb.edu.pl/).

4) Formalism seems to be bolstered by: non-Euclidean geometries, continuous
nowhere differentiable functions, paradoxes of set theory, Skolem's paradox,
Banach-Tarski paradox, Godel's incompleteness theorems, non-standard models
of PA, the formal concept of algorithm, the independence of CH and other
famous hypotheses from ZFC, the unsolvability of the 10th Hilbert problem,
the natural independence phenomenon. But, perhaps, any other -ism could
declare almost the same list of bolsters?

5) I agree that a philosophy without external consequences cannot remain
generally interesting for a long time.

P/S. Currently, the above-mentioned mainstream in set theory is much longer
(as a "stream") than other branches (ZF+V=L and ZF+AD), thus yielding an
impression of "stability". Couldn't we derive from this a high level
explanation of the modern Platonism in set theory?

Best wishes,
Karlis.Podnieks at mii.lu.lv
www.ltn.lv/~podnieks
Institute of Mathematics and Computer Science
University of Latvia