For Genzen's sequent calculus, why is the proof-theoretic ordinal /epsilon_0? I understand why we need at least omega, but not why ordinal exponentiation is necessary.