FOM: answer to question about proof theory vs f.o.m.

[Stephen G Simpson]

Mark Steiner 17 January 2000:

 > >Harvey (or anybody) what's the difference between f.o.m. as you
 > >understand and what used to be called "proof theory"?

Harvey Friedman 17 Jan 2000:

 > Time for Simpson to answer this, since he has been so quiet.

OK, I will answer it, but I am not sure this is what Steiner is
looking for.

F.o.m. is the study of the most basic mathematical concepts (number,
shape, set, function, algorithm, mathematical definition, mathematical
proof, ...) and the logical structure of mathematics, with an eye to
the unity of human knowledge.

The study of mathematical proof is part of f.o.m., and this was the
origin of proof theory as initiated by Hilbert.  But later proof
theory (like other branches of mathematical logic) developed in
directions that do not always reflect its f.o.m. origin.  For
instance, some of the work on proof-theoretic ordinal notations is
technical and its impact on f.o.m. questions remains to be seen.  On
the other hand, many papers in proof theory are motivated explicitly
by f.o.m. considerations.  Examples: work on Hilbert's program of
finitistic reductionism; natural deduction as an attempt to closely
model the structure of actual proofs; etc.

I would say that, due perhaps to initial directions set by Hilbert
Brouwer and Heyting, proof theorists and intuitionists as a group tend
to be more interested in and motivated by f.o.m. than other
mathematical logicians: recursion theorists, model theorists, set
theorists.  But of course there is also a lot of fine f.o.m. research
outside proof theory and intuitionism.  For instance, in set theory
there are consistency and independence results (Cohen, etc) and
various kinds of research trying to justify a choice of axioms.  In
recursion theory there is work on Church's thesis, the structure of
algorithms, computational complexity, etc.  In model theory, there is
Robinson's analysis of infinitesimals and the non-standard real number
system, there is Lindstrom's theorem characterizing predicate calculus
as an abstract logic, etc.

-- Steve