Return to Question

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?

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?

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?

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?

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.

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?