Ordinal Exponentiation in Genzen's Sequent Calculus

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?

Answer 1

(My main source for what follows is Michael Rathjen's paper, "The Art of Ordinal Analysis" http://www.icm2006.org/proceedings/Vol_II/contents/ICM_Vol_2_03.pdf.)

I believe there are a couple points of confusion here. First, the "proof-theoretic ordinal" of a theory $T$ usually means the least ordinal $\alpha$ such that, in some fixed notation system (e.g., Kleene's $\mathcal{O}$), there is no name for $\alpha$ which $T$ proves to be well-founded. So in principal, this has nothing to do with the lengths of deductions.

Second, at least if we want to talk about cut elimination in the context of proof complexity, the relevant theory is not $PA$ -- which has finite deduction trees but does not admit cut elimination (theorem 10.4.12 in Troelstra and Schwichtenberg's Basic Proof Theory; in general, the failure of cut elimination is due to axioms which break the symmetry of the logical inference rules, and in particular the induction axioms -- with their unbounded quantifier depth -- are especially problematic) -- but rather the infinitary theory $PA_\omega$, which has infinite deduction trees and does admit cut elimination.

$PA_\omega$ is $PA$ together with the $\omega$-rule: from $\varphi(0), \varphi(1), . . . $, we can deduce $\forall i\varphi(i)$. This is an infinitistic deduction rule, so proof trees are now infinite; on the plus side, now the induction axioms are deducible just using the logical rules.

Note that at the very least, deductions correspond to well-founded trees, i.e. trees without an infinite path. These trees have a nice notion of height: the height of a tree $t$ is defined inductively by $$ ht(t)=\sup\lbrace ht(t_a): \langle a\rangle\in t\rbrace, \quad\mbox{where}\quad t_a=\lbrace \sigma: \langle a\rangle^\frown\sigma\in t\rbrace.$$ So the height of the tree with just one root is 1, and the height of the tree $\lbrace \sigma: \vert\sigma\vert=\sigma(0)\rbrace$ is $\omega$. Note that even though all trees considered are countable objects -- in fact, subtrees of $\omega^{<\omega}$ -- the height of a well-founded tree can be an arbitrary countable ordinal. (This height is usually called the "rank" of the tree, but in this context that term is somewhat confusing.)

Now a given deduction $\mathcal{D}: \Gamma\implies\Delta$ in $PA_\omega$, viewed as a tree, has two ordinals associated to it: its height (defined above) and its cut rank, which is the supremum of the lengths of cut formulae in $\mathcal{D}$ (where length is defined inductively: quantifiers and Boolean combinations increase rank by 1). If $\mathcal{D}$ is a deduction of $\Gamma\implies\Delta$ with height $\alpha$ and cut rank $k$, we write $$\mathcal{D}\vdash_{\alpha, k}\Gamma\implies\Delta.$$

Cut elimination can be proved for $PA_\omega$, as follows: if $$\mathcal{D}\vdash_{\alpha, k+1}\Gamma\implies\Delta,$$ then there is some deduction $$\mathcal{E}\vdash_{\omega^\alpha, k}\Gamma\implies\Delta.$$ Removing cuts explodes the size of the proof tree, and this provides the connection between the proof-theoretic ordinal as usually defined, and the rank of deductions mentioned by the OP.

At this point there are two questions: why is this supremum of rank equal to the proof-theoretic ordinal, and why is cut elimination so costly? Towards the first question, I have no idea; it seems obvious to me that this supremum should be at least the proof-theoretic ordinal, but I don't see a clear reason why they should be the same. (Maybe they aren't always?) Towards the second question, I believe using instances of the induction axioms as cut formulae will give examples of proof trees which "blow up" quickly.

---

On the chance that the intended question is just, "Why is the proof-theoretic ordinal of $PA$ equal to $\epsilon_0$?" I have added the following:

The proof-theoretic ordinal of $PA$, $po(PA)$, is defined to be the least ordinal $\gamma$ such that $PA$ does not prove transfinite induction along a well-ordering of length $\gamma$. (It doesn't quite make sense to talk about $PA$ proving that something is well-founded, since well-foundedness is a second-order property and $PA$ cannot directly talk about second-order objects; hence the focus on transfinite induction.) There are now two parts to the proof that $po(PA)=\epsilon_0$.

The first part, the lower bound argument, is elementary: we can show in $PA$ that $\omega^{\omega^{\omega^{...}}}$ is well-founded for any finite tower of exponents, so $po(PA)\ge\epsilon_0$.

The second part is Gentzen's proof of $Con(PA)$ inside a weak fragment of $PA$ together with transfinite induction along $\epsilon_0$; this is essentially the proof of cut elimination in $PA_\omega$, together with the embedding theorem that for every sequent $\Gamma\implies\Delta$, there are some $\alpha, k$ such that $$ [PA\vdash \Gamma\implies \Delta ]\rightarrow[PA_\omega\vdash_{\alpha, k}\Gamma\implies\Delta].$$ Now by Goedel's Theorem, we must have that $PA$ cannot prove transfinite induction along any well-ordering of length $\epsilon_0$, so $po(PA)\ge\epsilon_0$. And we are done.

---

CAVEAT: I may have misunderstood the question; also, since proof theory is not my field, this may all be wrong.