FOM: proof-theoretic ordinals

[Stephen G Simpson]

Wilfried Buchholz writes:
 > On pp.222-291 of [B,F,P,S] I have proved without using ordinal
 > notations that ID_\nu(classical) is conservative over
 > ID_\nu(intuitionistic,strictly positive) for negative arithmetic
 > sentences. The corresponding result for ID_{<lambda} (lambda a
 > limit ordinal) has also been proved by Sieg in Ch.III of [B,F,P,S].

Thanks Wilfried, that's what I wanted to know.  As usual, Wilfried
Buchholz is the indispensable source of reliable information on proof
theory.  (Sorry Wilfried, I'm not trying to embarrass you, but the
truth is the truth.)

So, it seems that ordinal notations have been eliminated from many
reductions of classical systems to intuitionistic systems.  This again
raises the broader question: what good are by proof-theoretic
ordinals, anyway?

People can have different opinions on this broader question.  In 13
April 1998 23:22:35 I provocatively opined as follows:

 > I still think that, if we are looking for impressive applications of
 > ordinal notation systems, the best successes to date have been in the
 > area of finite combinatorial independence results, as discussed in my
 > posting of 1 Apr 1998 12:27:29.

Could you and the other proof-theorists please comment?

Also, what have you and the other proof-theorists got to say in
response to Harvey's "logical equations" posting of 17 Apr 1998
13:25:10?  My impression is that Harvey's characterizations of the
provably recursive ordinals of ZF etc are radically different from
earlier work on provably recursive ordinals, too new and different to
be evaluated properly as yet.  Is that correct?

-- Steve

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