FOM: role of formalization in f.o.m.

[Stephen G Simpson]

Martin Davis 26 May 1999 13:46:41 

 > Working out carefully what can be formalized where is of the
 > essence of the reverse mathematics program (in which Steve has
 > played such an important role).

Yes.  But figuring out what can be formalized where is important not
only in reverse mathematics (see Part A of my book ``Subsystems of
Second Order Arithmetic'' <http://www.math.psu.edu/simpson/sosoa>) but
also in a lot of other contemporary f.o.m. research.

For example, if Holmes and Forster want to show that NFU is viable as
a foundational setup for mathematics, they need to sketch how various
mathematical topics can be formalized in NFU.

Also, formalization is of the essence whenever consistency strength is
an issue.  Just to name a few instances: (1) Harvey's work on the
necessary use of large cardinals in finite combinatorics, (2) the
Martin-Steel-Woodin theorem relating large cardinals to projective
determinacy; (3) relative consistency results in set theory,
e.g. Shelah's proper forcing stuff; (4) model-theoretic proofs of
relative consistency results for subsystems of second order
arithmetic, as in Part B of my book.

This is part of why I find the dismissal of formalization by Conway
and others so irritating.

 > Of course, if you look at Steve's book, you won't see much at the
 > level of predicate calculus (= 1st-order logic). Steve, quite
 > properly assumes that the details of the formalization have become
 > routine ...

Yes, many of the details are routine and can be passed over lightly or
omitted, but that doesn't mean that formalization is a non-issue.
Generally speaking, much of the fabric of contemporary f.o.m. research
consists of verifying that various mathematical arguments are
formalizable in various formal theories.

-- Steve