FOM: proof-theoretic ordinals

[Stephen G Simpson]

Anton Setzer 10 Apr 1998 22:27:06 writes:

 > Although I belong to the ... in the list proof theorists above, ...

Anton Setzer is an accomplished proof theorist and I'm very glad to
have him on board FOM.  An even more prominent one is Helmut
Schwichtenberg!  Again, my apologies to all the proof theorists on FOM
whom I neglected to mention by name.

Setzer's posting is very useful and raises some good points.  In
particular, he touches on a very nice aspect of Martin-Lof
constructive type theory, namely the fact that one can develop a good
theory of constructive large cardinals with the right consistency
strength.  For instance, one can apparently prove equiconsistency of
(1) Martin-Lof type theory with constructive Mahlo cardinals and (2)
Kripke-Platek set theory with recursively Mahlo admissible ordinals,
via (3) well-foundedness of appropriate Feferman-Aczel-style ordinal
notation systems inspired by Mahlo cardinals.  I heard Rathjen speak
about this at an AMS special session in Milwaukee last fall.  I find
it very interesting.  I view it as a remarkable vindication of the
Gentzen-Feferman-Aczel-style ordinal analysis.

But, the question arises as to whether (3) is really essential here.
Can we bypass the ordinal notations in (3) and directly prove
equiconsistency of (1) and (2), via appropriate translations?  I don't
know the state of the art here.  Can someone fill me in?

There is precedent for this.  Ordinal notations have been used many
times to prove that a foundationally interesting theory is in some
sense reducible to or equiconsistent with another foundationally
interesting theory, but in at least some cases the ordinal notations
were later replaced by direct translations or interpretations.  Wasn't
this the case for classical and intuitionistic ID_{<omega}?  Please
correct me if I'm wrong.  But this is not to say that the ordinal
notations are useless.  In this case, they found an impressive
application in the Friedman-Robertson-Seymour independence result
(graph minors).

Setzer writes:
 > ... I was all the time facing the criticism, that proof theory is
 > too technical and nobody can understand it any longer. ....

Such criticism becomes moot when the technical developments are
justified by some impressive applications that can be appreciated by
outsiders.

-- Steve