[FOM] Great Achievements of F.O.M. 1

[Harvey Friedman]

This is intended to be a series in which great achievements in f.o.m.  
are discussed.

My idea is to respond to all doubters of the greatest of these  
achievements by refuting the objections. This often involves proving  
new theorems, or making new conjectures, or setting up new research  
programs.

As a primary example, when I was a Philosophy Professor at Stanford in  
the 1960s, I had my office in the Math Dept. I would often go to tea  
and talk to faculty there about f.o.m.. The lack of interest, and even  
derision, expressed about formal systems was very striking to me.

I set up Reverse Mathematics as a kind of response to these objections  
- "Formal systems have nothing to do with math. Formal systems are  
artificially constructed. And so forth." Actually, my original forms  
of RM were versions of SRM = strict reverse mathematics, which were  
ahead of their time. But that is a rich story for later.

So if, in the course of dealing with doubters of the Great  
Achievements of f.o.m., multiple subjects on the order of RM and SRM  
get founded - as we hope - then this series will have been worthwhile.

In this first posting, I want to present some background for the later  
discussions.

There is a considerable amount of skepticism about f.o.m. in the  
mathematics community. The prevailing wisdom in the Mathematics  
community, which I have run into many times in many forms and  
temperatures, runs like this when most heateds:

"Since mathematics is done on an informal level, formalization is  
pointless, meaningless, useless, misleading, countercultural, and  
backward. Therefore any results in f.o.m. based on any formal system  
is pointless, meaningless, useless, misleading, countercultural,  
worthless, and naive. In fact, formalization is constraining of  
mathematical activity, and in that sense, very dangerous. It is a  
preoccupation that has no place in any self respecting Math  
Department, because it is a preoccupation of third rate minds,  
attracted to rigidity for its own sake. People who work with formal  
systems and formalization know no mathematics, are devoid of any  
understanding of mathematics, and have no talent for real mathematics.  
Consequently, they hide in their inbred formal systems. This activity  
and the people pursuing it must be purged from Mathematics Departments  
in this age of limited resources. Given these truths, these people  
properly belong only in Philosophy Departments. If they can at least  
program a computer, then they might have some place in a Computer  
Science department."

In my experience, this kind of view is predominate in the major  
mathematics departments in the USA. I am measuring this in terms of  
majorities. I know many individuals in these Departments, some of  
which have iconic status in the Math community, who regard the above  
point of view as utterly absurd. But these are just individuals -  
famous and revered as they are.

How did this view come about? What circumstances perpetuate this view?  
What is (can, should, will) be done about it, short term (medium term,  
long term)?

Before getting into that, let me briefly state some highlights of my  
own view.

There is the Foundational Life, and also the Mathematical Life and the  
Philosophical Life. These are very different lives, with vastly  
different intellectual value systems, perspectives, and expectations.  
The two that are farthest apart among these three are the Mathematical  
Life and the Philosophical Life. The Foundational LIfe is about  
equally distant form the other two.

A very brief discussion of these three Intellectual Lives is presented  
in http://www.math.osu.edu/~friedman/manuscripts.html Lecture Notes,  
#55.

There are many other lives which are less relevant to our discussion.  
These include the Scientific Life (which has major traditional  
subdivisions, say into experimental and theoretical), and the Artistic  
Life (which also has major traditional subdivisions, such as  
performance and composition).

Of all of the major Intellectual Lives, it is the Foundational Life  
that is

i. The highest form of Intellectual Life - the deepest, most profound,  
and far reaching. Major full time and part time practitioners include  
Aristotle, Leibniz, Newton, Frege, Russell, Einstein, Goedel.
ii. It requires an unusual combination of very strong technical and  
conceptual powers.
iii. The number of serious practitioners is too small for it to have a  
natural home in the current global academic environment.
iv. It is in a very early stage of development - with a tremendously  
powerful, totally limitless, future.
v. Future developments in the Foundational Life will profoundly  
revolutionize mathematics, science, engineering, politics, economics,  
law, and art.
vi.  Its most highly developed component of the Foundational Life, at  
this time, is, by far, f.o.m.

We are of course going to focus on the f.o.m. component, as this is  
the FOM email list.

However, let me just say in passing that I regard a number of my other  
intellectual activities as part of my Foundational Life. These include

Concept Calculus (mutual interpretation of: i) groups of principles  
about informal concepts; ii) abstract mathematical principles (via set  
theory).
Software Verification (directed toward programming language design).
Interactive Educational Software (for teaching mathematical rigor).
Music Performance/Recording (includes both real time and non real time  
piano performance, directed toward understanding musical  
microstructure).

I have devoted my Intellectual Life to the Foundational Life. In the  
earlier years focusing entirely on the f.o.m. component, and in later  
years, branching out. However, there has been increasingly rapid  
progress in the f.o.m. component of my efforts. The original intention  
in graduate school was to spend about 5 years in f.o.m. before moving  
on to a succession of areas within the Foundational Life. The 5 years  
became 45 years (time flies!). I now look forward to substantial  
expansion of my Foundational Life - better late than never.

This component, f.o.m., in turn grew out of the Philosophical Life. At  
some point, it became rather evident that if f.o.m. is going to come  
to grips with substantial mathematical issues of various kinds, then  
it will need a rather substantial mathematical development on several  
fronts. This spawned the development of mathematical logic - a spinoff  
of f.o.m., where fundamental structures and notions arising from  
f.o.m. are investigated for their own sake, and also for their  
connections with various topics in mathematics proper.

So f.o.m. migrated from Philosophy Departments to Mathematics  
Departments, where it morphed into mathematical logic. Currently,  
there is very little f.o.m. being done in Mathematics Departments or  
in Philosophy Departments - or anywhere. The remnants of f.o.m. are  
Mathematical Logic in Mathematics Departments and Philosophical Logic  
in Philosophy Departments. Yet there is a substantial interest in  
f.o.m., as witnessed by the FOM email list which I founded as early as  
1997 (with help from Steve Simpson, the first Moderator). There is a  
hunger out there. Kurt Goedel continues to be revered.

The distinction between mathematical logic and f.o.m. is clear but  
perhaps subtle; many people are not sensitive to this distinction,  
particularly those in mathematical logic who grew up in an environment  
where the f.o.m. perspective had long since virtually disappeared.  
Yes, students generally have some sort of feeling that there is some  
kind of huge difference between Goedel's work and current mathematical  
logic. But this is rarely identified by students for what it is: a  
major, even profound, shift in perspective. Away from profound  
matters, and toward specialized matters.

So let us return to our questions: How did this view of mathematicians  
come about? What circumstances perpetuate this view? What is (can,  
should, will) be done about it, short term (medium term, long term)?

The (preponderance of) mathematician's repudiation of f.o.m. also  
includes some "profound indifference". There is a set idea that  
logical issues simply, on principle, cannot be of any importance, and  
are a waste of time. This profound indifference may not be accompanied  
by the kind of open hostility represented by the above diatribe in  
quotes (starting with "Since"). However, when pressed to opine, in  
some context or another, an at least partial expression of the above  
diatribe surfaces. Often no verbalization is required among so many  
like minded scholars. It is simply understood to be the case.

My theory as to what perpetuates this view goes as follows. Consider  
how long mathematics flourished before even the serious beginnings of  
the instillation of rigor - let alone the construction of ZFC. Clearly  
there are great obstacles for most of even the greatest of  
mathematicians to getting a sense of how formalization works, and just  
how many ways there are of formalizing things. So the natural state of  
affairs is to rely on one's intuition and not be concerned with  
formalization - and never get schooled in just how surprisingly  
flexible formalization really is.

Consequently, there is a widespread and mostly silent suspicion about  
formalization among mathematicians. That formalization is somehow  
inflexible and restrictive and artificial.

The truth of the matter is that it is extremely flexible. However, in  
most ways of going about it, it is indeed artificial, since one is  
generally forced to make a bunch of choices that make absolutely no  
difference whatsoever, and never need be reconsidered. There are also  
ways of formalizing which are trickier, but which largely remove these  
artificialities. The artificialities, for the preponderance of  
foundational purposes, are of course entirely harmless. Naturally, one  
can investigate artificial-free formalization as a topic in itself (in  
which I am interested), and that is a different story.

By far the most straightforward and well understood autonomous  
formalization is through set theory. Here there is a great deal of  
useful flexibility. One can also sugar it by adding a judiciously  
chosen list of new primitives, with appropriate axioms, and then prove  
appropriately formulated existence and uniqueness theorems. But for  
the Great Achievements of F.O.M. that we have now, it is generally  
simplest to avoid such sugar, and proceed in the well known  
straightforward manner, accepting artificialities that don't cause any  
problems. One proves that the artificialities don't cause any problems  
by appropriate uniqueness and isomorphism theorems.

The usual foundation for mathematics via set theory - in particular  
ZFC - employs a sharp demarcation between the so called logical part,  
and the so called set theoretic part.

There are some serious delicate issues regarding just why things are  
done in this way, and why the logical part is what it is - which is  
first order predicate calculus with equality. In practice, it must be  
heavily sugared. There is the problem of saying something interesting  
about just what we mean by sugar. A major component of sugar is of  
course abbreviation facilities. Without it, you can't really actually  
formalize anything.

There is also the issue of just what is meant by "mathematics is  
formalized in ZFC". There are several dimensions to this question.  
First of all, it is false, if taken literally. People write papers,  
which are not really formal at all. So one usually says "mathematics  
can be formalized in ZFC". But what does "can" mean?

Let me insert a fact. When I interacted about a paper of mine with  
Charles Fefferman, acting as Editor of the Annals of Mathematics, he  
made a very clear and definite statement as follows.

"In order for a paper to be accepted by the Annals of Mathematics (as  
far as he was involved), the proofs must be readily formalizable in  
ZFC. Any further assumptions must be explicitly stated. Any assumption  
that is part of ZFC does not need to be stated."

Let me move on to: What is (can, should, will) be done about it, short  
term (medium term, long term)?

I classify what is happening now in logic in Math Depts in the  
following rough categories.

1. Pursuit of Mathematical Logic for its own sake, as a spinoff of  
f.o.m. Here connections with mathematics proper are besides the point.  
Rather, one is interested in a kind of normal intense development of  
the deep legacy of structures and concepts spawned by f.o.m. - in  
which they are naturally extended and generalized - in a way  
(allegedly) similar to what is going on in other highly specialized  
areas of mathematics.

2. Pursuit of connections of Mathematical Logic with mathematics  
proper. Here there is usually a rejection of any intrinsic interest of  
Mathematical Logic development in 1, and the aim is toward connections  
and applications (new proofs, simplified proofs, and new findings).

3. Foundations of Mathematics. Here the investigations are driven by  
deep and systematically framed conceptual/philosophical considerations  
of great general interest, following Goedel's modus operandi. However,  
there is very little work generated in this way. Rarely is anything in  
line 1 of general interest, even to mathematicians. Rarely is anything  
in line 2 of general interest outside mathematics. F.O.M., at the top  
level, is of great general interest - and, generally speaking, of  
considerably higher general interest than major developments in either  
Mathematics or Philosophy. This was clear in the 1930's with Kurt  
Goedel.

Inevitably, things are not entirely black and white, and there is  
blurring. Sometimes line 1 finds, perhaps accidentally, something in  
line 2, which is opportunistically pursued somewhat before going back  
to line 1. Or sometimes line 2 finds that it needs a period of line 1  
development, with the expectation that it will eventually be in line  
2. I mean this both at the people level and at the group level.

Line 3 may unexpectedly draw from line 1 and even sometimes line 2,  
but only for a clearly stated higher purpose.

I am going to stop here. This will give you an idea of how I want to  
talk about the Great Achievements of F.O.M., and how a careful  
consideration of them, in detail, leads to an enormous number of new  
(an old, and somewhat new) research directions in f.o.m.

Harvey Friedman