FOM: proof-theoretic ordinals (correction and follow-up)

[Stephen G Simpson]

In my posting of 13 Apr 1998 10:59:01 I wrote:

 > 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.

After consultation with Harvey Friedman, I think I was wrong about
this.  According to Harvey, we don't yet know how to reduce the
classical ID_2, ID_3, ..., ID_{<omega} to their intuitionistic
counterparts, except via ordinal notations.

However, in the case of some stronger theories, the reductions are
accomplished by other methods.  For instance, double negation
transforms are used to reduce classical second order arithmetic to
intuitionistic second order arithmetic, classical ZF to intuitionistic
ZF, etc.  In these cases, the appropriate ordinal notation systems are
unavailable.

Another question in my mind is, how generally interesting are these
intuitionistic systems anyway?  It seems difficult to explain the
interest of intuitionistic formal systems to most mathematicians.
Issues of constructivity do engage the attention of many
mathematicians, but the interest is expressed mainly in terms of
questions about bounds, which can be answered any methods including
classical ones.  The relevance of intuitionistic formal systems is
unclear.

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.

-- Steve