FOM: Consistency proofs

[steel@math.berkeley.edu]

  Paul Cohen recently gave a talk at Berkeley in which he outlined a
a consistency proof for Peano Arithmetic (PA) using induction up to
epsilon_0, and discussed possible extensions of his method to 2nd order
arithmetic and to set theory. 
  I cannot judge to what extent Cohen's proof differs from Gentzen's, as I
don't have the latter fully at hand. They seem close. At the least,
Cohen's proof did seem clean and nicely exposited. He has it written up.
  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? ( For
example, one central open problem in set theory is: develop an inner model
theory for supercompact cardinals. This is vague, but there is a host of
precisely stated questions whose solution presumably needs such a theory--
e.g., does Con(PFA) imply Con(supercompact). Without these test questions,
it would be less clear what the inner model program is aiming at.)
  As to precise statements of the consistency-proof problem, I can't think
of any that don't have trivial solutions. For example, isn't it easy to
construct a recursive linear order of omega defined by the wff theta such
that (i) in ZFC (or something much weaker) + "ZFC is Pi_1^1 correct" one
can prove "theta defines a wellorder whose order type is the sup of the
provable-in-ZFC ordinals", (ii) for any n in omega, ZFC proves "the
initial segment of the order defined by theta below n is a wellorder", and
(iii) ZFC (or something much weaker) proves "Con(ZFC) iff the order
defined by theta has no "periodic" descending chains". ( I omit the def.
of "periodic". If you put "recursive" instead, I think you get an
equivalent of omega-consistency.) The idea here is just to amalgamate all
the provable-in-ZFC recursive wellfounded relations, and then go to the
Brouwer-Kleene normal form.
  As to test questions, one would think that the possible applications of
a consistency proof for set theory would lie in establishing
consistency-strength lower bounds for concrete combinatorial ( Pi^0_1 or
Pi^0_2 ) statements whose strength is at the level of 2nd order arithmetic
or set theory. As I understand it, the only results of this kind now known
are due to Harvey, and the lower-bound arguments don't use proof-theoretic
methods.  (True?) How about at lower consistency-strength levels --
what kind of applications does the existing ordinal analysis of, say,
predicative analysis have?
   On a more lofty level, I wonder what people on the list think of the
"Gentzen Program" of giving "as-constructive-as-possible" consistency
proofs for strong systems like 2nd order arithmetic and set theory.


John Steel