For Genzen's sequent calculus, 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?