Return to Answer

The proof-theoretic ordinal of $PA$, $po(PA)$, is defined to be the supremum of the ordinals $PA$ proves to be well-founded. More usefully, $po(PA)$ is the least ordinal $\gamma$ such that $PA$ does not prove transfinite induction along a well-ordering of length $\gamma$. (I believe these two notions are not always the same, but $PA$ is strong enough that in this context they are equivalent.) There are now two parts to the proof that $po(PA)=\epsilon_0$.

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$.

$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 (so in particular, the rank of a proof tree can be infinite); on the plus side, now the induction axioms are deducible just using the logical rules.

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.

$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.

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.

I believe the point of confusion here (besides the definition of proof-theoretic ordinal) is about the theory $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), versus the infinitary theory $PA_\omega$, which has infinite deduction trees and does admit cut elimination.

Now a given deduction $\mathcal{D}: \Gamma\implies\Delta$ in $PA_\omega$ has two ordinals associated to it, its height (which is just the rank of $\mathcal{D}$ as a well-founded tree) 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.$$

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.

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.

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.$$

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 supremum of the ordinals $PA$ proves to be well-founded. More usefully, $po(PA)$ is the least ordinal $\gamma$ such that $PA$ does not prove transfinite induction along a well-ordering of length $\gamma$. (I believe these two notions are not always the same, but $PA$ is strong enough that in this context they are equivalent.) 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.