For Genzen's sequent calculus with PA axioms, why is the proof-theoretic ordinal /epsilon_0? This seems to hinge on what exactly it means for the level of a cut or CJ inference figure to be higher than that of a lower sequent, because it is when we encounter such a situation that the complexity represented by the ordinal alpha is used to denote the new complexity: omega^alpha (or omega^omega^omega^alpha, if the level of the lower line is three lower rather than just one). According to my current understanding, a proof theoretic ordinal of omega means there are potentially omega lines in the proof. What is it about eliminating cuts that might lead to proofs with more than omega lines?
Ordinal Exponentiation in Genzen's Sequent Calculus
vertigo
- 21
- 2