FOM: Consistency proofs

[Harvey Friedman]

Reply to Steel 10:06AM 3/25/98.

I think that everyone on the fom list very much appreciates that you have
taken the trouble to inform us of what Paul Cohen had to say at Berkeley
last week.

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

There are a number of proofs now, including a distinctly model theoretic
approach of Avigad and Sommer, who are on the fom. But none of these go up
to full 2nd order arithmetic, let alone set theory as of now. The model
theoretic approach as of now stops just beyond the predicative systems.

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

I heard that a copy was left at Berkeley. Can you copy one for me and send
it by snailmail?

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

The only test questions I know of surround the mysterious highly
impredicative proofs that are currently used to prove some combinatorial
theorems. I'm thinking of such things as  a) the Nash-Williams infinite
tree theorem; b) Kriz's theorem answering a conjecture of mine about the
well quasi ordering of finite trees with embeddings with gap condition; c)
idempotent ultrafilters and a combinatorial theorem of Carlson; d) related
theorems from wqo and bqo theory e) perhaps also various theorems from
ergodic theory. These proofs all go beyond the subsystems of 2nd order
arithmetic for which one has an accepted proof theory - or at least seem to
butt right up against them.

The background is that I used proof theory somewhat lower down - in the
pi-1-1 comprehension level - in order to get independence results in well
quasi ordering theory such as Kruskal's finite tree theorem, some
extensions of Kruskal's theorem based on embeddings with gap condition, and
the graph minor theorem due to Robertson/Seymour. And to this day, there is
no known way to get rid of the use of proof theoretic ordinal analysis to
get these results.

So one would like to use proof theory to show that the above theorems a) -
d) are very impredicative - well into delta-1-2 comprehension + full
induction, at least. I think they currently use pi-1-2 comprehension to
prove at this time.

>  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?)

Yes. My methods are purely model theoretic.

>How about at lower consistency-strength levels --
>what kind of applications does the existing ordinal analysis of, say,
>predicative analysis have?

See above.

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

This seems difficult to defend in light of the complexity of the ordinal
notations even for relatively weak systems.