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?