FOM: Consistency proofs

[Rick Sommer]

In his March 25 10:06 message John Steel asks:

   The problem of finding  Gentzen-style consistency proofs for 2nd
   order arithmetic and set theory, and identifying the "provable
   ordinals" of these theories, is well known. My question is: is
   there a precise statement of this problem? Are there any precisely
   stated "test questions" which only the right kind of consistency
   proof could answer? 

(John, I don't know if you remember, but you asked me questions of
this form about 8 years ago following a talk I gave in the UCLA logic
colloquium on model theoretic ordinal analysis.) 

My answer, as based on discussions with proof theorists, and
researching the proof theory literature, is that there is no precise
statement of the problem. On the one hand, we can be very precise
about what the proof-theoretic ordinal of a theory is, but it is not
clear what it means to "identify" such an ordinal (in a way that
satisfactorily solves the "problem"). The proof-theoretic ordinal,
alpha_T, of a theory T is (sometimes) defined to be the supremum of
the order types of all T-provable well-order relations --- this
definition describes the ordinal, but it clearly doesn't classify as
an "ordinal analysis of T".

To give my on version of an example noted by John, I note that there
is a "trivial" uniform primitive recursive description of alpha_T
(provably so in PRA), that works for any T that contains a sufficient
amount of arithmetic and is recursively axiomatizable, but these
descriptions (that I have in mind) are heavily metamathematical -- for
example, a prim. rec.  description of an ordering <_T, of type
alpha_T, might include clauses of the following form: a <_T b if a and
b code pairs (p,a') and (p,b'), resp., where p codes a T-proof that
some prim rec linear order is well founded, and a' is less than b'
with respect to that linear order. This is short of a full description
of <_T, but it is an easy exercise to fill it out. Also, I note that
"primitive recursive" can be replaced by polynomial time computable;
the point being that the computational complexity of the description
of alpha_T fails to be a test for classifying what constitutes an
ordinal analysis of a theory.

A satisfactory ordinal analysis should include a mathematical, rather
than metamathematical, description of alpha_T. The purely
combinatorial and simply mathematical descriptions of epsilon_0
clearly satisfy this condition. I wasn't at Cohen's talk, but based on
what I've heard, he did not include a mathematical description of the
proof theoretic ordinal of ZF, even though he hinted that he would in
his abstract --- it would certainly be significant if Cohen has this
result. 

The proof theory community can point to a large number of examples
where the ordinal analysis problem has been "solved", and by pointing
at those, one gets a feel for what constitutes a satisfactory
solution, but no one has been able to put their finger on it in a
precise way. For example, Gentzen's proof that the ordinal of PA is
epsilon_0 is the ideal prototype; it would be great if that could be
imitated in every way for stronger theories. However, the observation
is that the ordinals that go with stronger theories have much more
complicated descriptions, but complicated in what precise sense? To my
knowledge (and I've researched this) no one has answered that. This
higher degree of complicated-ness is allowed to some extent, but to
what extent? Again, to my knowledge, no one has answered that. 

I think these are important and worthwhile questions, and I think that
they need to be further addressed in the proof theory community.
However, I also believe that proof theoretic research, with the goal of
carrying out the ordinal analysis of stronger and stronger theories,
can go on even without a precise definition of the problem. (Isn't
this similar to the situation in many other parts of mathematics; the
inner model program in set theory just being one other example?)

--Rick Sommer