FOM: foundational significance of proof theory

[Stephen G Simpson]

Dear FOM subscribers,

During the last few months I allowed the FOM list to slide, because
I've been working hard on my book.  Now that the book is done, I want
to rev up FOM again.  Subscribers, could you please help out?  We need
some exciting, provocative postings.  I'd like to thank Joe Shipman
and a few others for their recent postings, but we need more.

In 24 Jan 1998 18:09:39 I presented a non-exhaustive list of topics to
be discussed on the FOM list.  One of the topics was:

 > What can technical work in mathematical logic contribute to
 > f.o.m. research?  More specifically:
 > 
 >   a. What can model theory do for f.o.m.?
 > 
 >   b. What can proof theory do for f.o.m.?
 > 
 >   c. What can recursion theory do for f.o.m.?
 > 
 >   d. What can set theory do for f.o.m.?

The background for this is that, historically, mathematical logic grew
out of foundational considerations, but some of the modern technical
developments seem to have left foundations far behind.  My question
is, is there any foundational juice left in these fields?  

As an example, let's focus on proof theory.  Historically, proof
theory originated as a search for consistency proofs in the light of
Hilbert's program.  But much of modern proof theory seems to consist
of technical questions on ordinal notations, and to the outsider, the
connection to the original foundational issues may be unclear.

Just to get the discussion going, could one or more proof theorists
please comment on the foundational significance, if any, of one or
more recent technical developments in proof theory?  What foundational
conclusions emerge from technical achievements such as Rathjen's work
on the ordinal of Pi^1_2 comprehension, Martin-Lof constructive type
theory, Kohlenbach's unwindings in analysis, etc etc.?

Best regards,
-- Steve

Name: Stephen G. Simpson
Position: Professor of Mathematics
Institution: Penn State University
Research interest: foundations of mathematics
More information: www.math.psu.edu/simpson/