Consistency of Analysis in Second Order Arithmetic – Proof Theory

foundationslo.logicordinal-numbersproof-theoryreference-request

Is there a proof of the consistency of Analysis (second order arithmetic), which is similar to Gentzen's proof of the consistency of arithmetic?

Update:

Which (different) methods can be used to prove the consistency of Analysis? and where can I find such proofs?

Best Answer

I believe the answer is "no": certainly the proof-theoretic ordinal (the optimal object taking the role of "$\epsilon_0$" in Gentzen's proof) is totally unknown, and my understanding is that there is no non-trivial upper bound on it, either. See also Proof-Theoretic Ordinal of ZFC or Consistent ZFC Extensions?; in particular, my understanding is that we only know the actual proof-theoretic ordinals of theories up to (something around) $\Pi^1_2$-comprehension, and I suspect we don't even have upper bounds for proof-theoretic ordinals as high as $\Pi^1_3$-comprehension.

That said, I also believe this is the only obstacle - that is, if we had the proof-theoretic ordinal $\alpha$ in hand, then we would have a proof of "Analysis is consistent" from "$T$+'induction along $\alpha$'", where $T$ is some reasonable weak base theory and "induction along $\alpha$" is properly formulated. So in some sense, the only real difference between analysis and arithmetic is in the complexity of finding the proof-theoretic ordinal.

. . . however, the use of the word "only" there can be extremely misleading: finding proof-theoretic ordinals of stronger and stronger theories requires increasingly deep ideas, and not just the continued turning of a well-understood crank. So on the one hand, while it's valuable to localize all the difficulty around a single object, it's also true that this is a vastly complex object, and that saying "all we need to do is understand the proof-theoretic ordinal" is less meaningful than it might sound.

Related Question