FOM: applications of proof theory

[Stephen G Simpson]

This is a followup to my FOM posting of 1 Apr 1998 12:27:29 on
applications of Gentzen-style proof-theoretic ordinal analysis.

1. Consistency proofs

In my posting of 1 Apr 1998 12:27:29, I wrote:

 > Traditionally, Gentzen-style proof-theory has been viewed as
 > providing "consistency proofs" for various subsystems of second
 > order arithmetic.  In my opinion, this is not a very good way to
 > view the matter, because the ordinal analysis itself (Feferman,
 > Sch"utte, Takeuti, Feferman-Aczel, Rathjen) is very complicated and
 > therefore unconvincing with respect to consistency of the systems
 > considered.

Two comments on this:

(i) The deemphasis of consistency proofs is not only my opinion.
Feferman and other eminent proof-theorists have expressed similar
opinions.  Indeed, are there any proof-theorists who still take the
traditional view?  (By the traditional view, I mean the view that
consistency proofs are a principal reason to be interested in
Gentzen-style ordinal analysis.)

Would some of the other proof-theorists on the FOM list (Tait,
Rathjen, Friedman, Pohlers, Takeuti, Sommer, Sieg, Buss, Kohlenbach,
Pfeiffer, Fine, ...) care to commment on this matter?

(ii) Yesterday Harvey Friedman posted an abstract of his remarkable
recent work giving mathematical characterizations of the provable
ordinals of ZFC and stronger systems.  It's hard to predict the
long-term implications of this, but I'm wondering whether there could
be any implications for consistency proofs.  Harvey, could you please
comment?

2. Other applications

In my posting of 1 Apr 1998 12:27:29, I emphasized applications of
Gentzen-style proof theory to combinatorial independence results.  But
Gentzen-style proof theory also has other important applications.  I'm
thinking of applications where one foundationally significant formal
system is reduced to another.  For instance, in

    Harvey Friedman, Kenneth McAloon, and Stephen G. Simpson, A
    finite combinatorial principle which is equivalent to the
    1-consistency of predicative analysis, in: Logic Symposion I
    (Patras), edited by G. Metakides, North-Holland, Amsterdam, 1982,
    pp. 197-220.

it is shown that ATR_0 is reducible to IR, in the sense that ATR_0 is
conservative over IR for Pi^1_1 sentences.  This involves the
proof-theoretic ordinal Gamma_0.

The foundational significance of these systems is as follows.  IR is
Feferman's system of predicative analysis.  ATR_0 is a subsystem of
second order arithmetic that frequently arises in reverse mathematics
and is equivalent to many mathematical statements, e.g. the open
Ramsey theorem, the perfect set theorem, Ulm's theorem, the K"onig
duality theorem for countable bipartite graphs, etc etc.  ATR_0 is
discussed thoroughly in chapter V of my forthcoming book on subsystems
of 2nd order arithmetic and reverse mathematics.

The reduction of ATR_0 to IR has been described as contributing to a
foundational program of predicative reductionism.  See my paper
"Friedman's research on subsystems of second order arithmetic", pages
137-159 of the Harvey Friedman volume, North-Holland, 1985.  I'd like
to hear further comment on this aspect.
    
-- Steve