FOM: Current Status of f.o.m. #1

[Harvey Friedman]

I have developed a talk called "Current Status of Foundations of
Mathematics" for a general philosophical audience. I just gave this talk at
the Stanford Philosophy Colloquium. A copy of the lecture notes for this
talk will be placed at the preprint server I am using for all of my
polished and semi-polished papers and lecture notes, within a week:

http://www.mathpreprints.com/

Of course, there are severe time constraints on lectures, and so I only
briefly touch on the many topics in these lecture notes.

My plan is to post a long series of edited and expanded excerpts from these
lecture notes. The hope is that this will generate discussion on the FOM
list. This is the first installment of this series.

The lecture notes start with "Introductory Remarks", and an outline of the
main body of the talk.

*************************************************

INTRODUCTORY REMARKS.

It goes without saying that only a limited number of topics in f.o.m. can
only be briefly discussed in this talk.

A great deal is known about f.o.m., much more so than the foundations of
any other subject. Furthermore, the quality of this knowledge is
extraordinary, backed up with a huge complex of sophisticated rigorously
proved theorems.

As a purely mathematical subject, independently of its philosophical
purposes, f.o.m. holds its own as a major branch of mathematics in terms of
depth, power, and complexity.

However, thinking about f.o.m. independently of its philosophical purposes
- or, if you prefer, its general intellectual purposes - is fundamentally
wrongheaded and severely limiting.

Major progress in f.o.m. generally requires an unusual combination of
mathematical and philosophical abilities that is hard to nurture in the
current overdepartmentalized University structures.

***FOM readers: What has been your experience with mathematics/philosophy
crossover? E.g., how does it work at Berkeley, UCLA, Madison, Harvard/MIT,
Stanford, and other places?***

There is much in f.o.m. of interest to the philosopher who has no intention
of working directly in f.o.m. These include

i) History of f.o.m. Many logic oriented philosophers have taken this up,
with in depth studies concerning, e.g., Brouwer versus Hilbert on
constructivity and intuitionism, Hilbert's intentions in his flawed
Hilbert's program, the Godel/Wittgenstein controversy as to the meaning and
significance of the incompleteness theorems, etcetera. Various topics in
history of philosophy arise.

***FOM readers: It would be nice if you could post a list of recommended
publications along these lines, together with some critical remarks of your
own. E.g., Dirk van Dalen's book on Brouwer, Godel's Collected Works edited
by Feferman, et al.***

ii) Using developments in f.o.m. in connection with positions in the
philosophy of mathematics.

***FOM readers: It would be nice if you could post a list of recommended
publications along these lines, perhaps with some critical remarks of your
own. Example: Maddy's books on Realism and Naturalism.***

iii) Critical philosophical analysis of important notions that have arisen
in f.o.m. For example, the notions of effectively computable, (first order)
logical truth, finitary proof, constructive proof, predicative proof, etc.

***FOM readers: It would be nice if you could post a list of recommended
publications along these lines, perhaps  with some critical remarks of your
own. Example: Feferman's numerous articles on predicativity - see the
Feferfest volume that is just about to appear.***

iv) Use of the extraordinarily successful development of f.o.m. as guidance
for the development of the foundations of other subjects, such as
foundations of physics, statistics, computer science, law, etc.

***FOM readers: It would be nice if you could post a list of places where
this point of view is implicitly or explicitly presented or used, perhaps
with some critical remarks of your own.***

In my opinion, these are most profitably pursued through collaboration
between philosophers and f.o.m. experts, and lead to new questions of a
formal character that can be substantively addressed by f.o.m. experts.

SOME F.O.M. DEVELOPMENTS.

1. Formalization of mathematics.
	a. Importance of formalization.
	b. Architecture of the usual formalization.
	c. Logical versus mathematical. Completeness.
	d. Meaning of formalization. Automated proof checking.
2. Consistency of mathematics.
	a. Unprovability of consistency.
	b. Unprovability of feasible consistency.
	c. Relative consistency. Interpretability.
	d. Reactions to unprovability.
3. Consistency proofs of restricted mathematics.
	a. Additive arithmetic.
	b. Elementary algebra and geometry.
	c. Higher objects.
4. Logical analysis of standard mathematics. Reverse mathematics.
5. Incompleteness in the formalization of mathematics.
	a. Completeness for simple sentences.
	b. Incompleteness for relevant sentences.
	c. Boolean relation theory.
	d. The varying parameters program.
6. The metamathematical hierarchy.
	a. Polynomially bounded arithmetic.
	b. Exponentially bounded arithmetic.
	c. First and second order arithmetic.
	d. Type theory, Zermelo set theory.
	e. ZFC.
	f. Large cardinals.
	g. Robustness.