Why do stacked quantifiers in PA correspond to ordinals up to $\epsilon_0$?

Question

I am trying to understand why induction up to exactly $\epsilon_0$ is necessary to prove the cut-elimination theorem for first-order Peano Arithmetic; or, as I understand, equivalently, why the length of a PA-proof with all cuts eliminated grows (in the worst case) as fast as $f_{\epsilon_0}$ in the fast-growing hierarchy.

I can understand why use of an induction axiom corresponds to ordinal multiplication by $\omega$. As induction axioms are written in the sequent calculus, as a premise we have a proof of $\phi(x)\vdash\phi(Sx)$ for a free variable $x$, and as a conclusion we get $\phi(0)\vdash\phi(y)$ for any term $y$.

Then if the proof of $\phi(x)\vdash\phi(Sx)$ has the ordinal $\omega^\alpha$, the proof with the conclusion $\phi(0)\vdash\phi(y)$ is assigned the ordinal $\omega^{\alpha+1}$. E.g. if the proof of the induction step had ordinal $\omega^0 = 1$, then the conclusion $\phi(y)$ has the ordinal $\omega^1 = \omega$.

This part makes perfect sense to me, because if I wanted to eliminate the use of an induction rule (CJ sequent) I might just start with $\phi(0)$ and repeatedly go through the part of the proof that I used to prove $\phi(x)\vdash\phi(Sx)$. Say, I'd repeat the sub-proof of the induction step 17 times, e.g. with $\phi(14)\vdash\phi(15)$ and so on, until I got to $\phi(17)$, or whichever number I wanted to prove $\phi$ about.

I don't quite understand how this corresponds to eliminating cuts, per se (it seems to create a host of new cuts, in fact). But it is still very intuitive to me that Peano Arithmetic's power to invoke the induction axiom would correspond to multiplication by $\omega$. If we take a proof in PA that ends with a single use of the induction axiom to get $\phi(y)$, and we want to translate it into a proof in an arithmetic theory that doesn't have induction, then we might have to multiply the PA-proof-length by any finite number (e.g. multiply it by 17) to get the proof length in the inductionless theory.

Repeated multiplication by $\omega$ only takes us up to $\omega^\omega$ as a proof-theoretic ordinal, though.

According to Gentzen, when we use cuts on formulas involving quantifiers, e.g. $\forall p:\exists q:\psi(p,q)$, this corresponds to ordinal exponentiation. If the proof above the cut has ordinal $\alpha$ and we cut a formula with one quantifier, then the proof below the cut has ordinal $\omega^\alpha$. If we cut on two quantifiers, the proof below the cut has ordinal $\omega^{\omega^\alpha}$. This fits with other things I've heard about how PA using formulas with only N quantifiers can be proven consistent by PA using only N+1 quantifiers. (As a side issue I'd be interested in knowing how you use N quantifiers to prove wellfoundedness of an ordinal notation for a stack of $\omega$s N layers high.)

What I don't understand is why the ability to use quantifiers corresponds to ordinal exponentiation. I can guess in a vague sense that if we have a proof using $\forall p:\phi(p)\vdash\phi(17)$, and we want to eliminate the use of $\forall p:\phi(p)$, then we need to repeat that part of the proof each time we want to prove $\phi(17)$, $\phi(q)$, and so on. But this would again just imply that we needed to repeat that part of a proof a finite number of times, and iterating this takes us up to only $\omega^\omega$, not the desired $\epsilon_0$, so I must be missing something.

I asked a friend to help with this and she's read through Gentzen's relevant papers, and she's shown me the relevant parts, and I'd previously checked several standard texts on proof theory and Googled around, and she's also shopped the question around the logic department of a major university, and we still don't know any answer to this except "because Gentzen says to use ordinal exponentiation".

We also can't find any examples of cut-elimination being carried out on a proof with cut on a quantified formula, which shows how the size of the resulting cut-free proof could grow faster than $f_{\omega^\omega}$. An example like this for some particular proof would be very helpful, even if, of necessity, the repeated steps for eliminating the cut are sketched more than shown. I can understand why the length of a Kirby-Paris hydra game grows at the same rate as the Goodstein sequence, and visualize both processes insofar as a human being possibly can. I cannot visualize why the length of a PA-proof heading for cut-freeness would grow at that same rate as cuts were repeatedly eliminated. (Mapping the process onto a Kirby-Paris hydra game of starting height at least 3 would answer the question!)

Answer 1

8/14: Substantially edited in response to comments: added to 1st part, added new 2nd and 4th parts

There's also some discussion underneath, and a link to a partial write-up of a case of cut-elimination involving the Ackermann function

If you haven't found the Gentzen-style proof illustrative, I recommend trying the infinitary proof. (Not everyone likes it, but it's at least an alternate perspective on it.) Pohlers "Proof Theory: An Introduction" gives a nice presentation of the proof, and it includes the proof in PA that ordinals below $\epsilon_0$ are well-founded. (This includes that fact that you use $N$-quantifier induction to proof well-foundedness up to $N+1$ exponents, and provides some insight into way additional quantifiers make it have the effect they do.)

One nice feature of the infinitary proof is that the ordinals are outright bounds on the heights of proofs, so if you're comfortable visualizing infinitary proofs, the source of the increase in bounds is quite explicit.

It's worth noting that "infinitary" is a bit of a misnomer. The infinitary proof takes the perspective that a proof of $\forall x\phi(x)$ should be a computable function $f$ so that, for each $n$, $f(n)$ is a proof of $\phi(n)$. Since the functions are all computable, there's nothing genuinely infinitary about it. People usually ignore the "computable" part for expository purposes, since it makes sense without that requirement, at which point it does look infinitary, but this is just because many of the ideas are clearer without constantly rechecking that the operations we're describing really are computable.

$ $

A follow-up point about what ordinals mean in proof theory. As pointed out in the comments, $\omega$ doesn't really mean "infinite" it means "an unspecified fixed integer". Similarly, $\omega+3$ really means "not only is this integer unspecified, but it will take three steps to figure out which integer it is". So in the infinitary proof of cut-elimination, when we say that a proof has height $\omega$, we mean that it is a proof of, say, $\forall x\phi(x)$, where the height of proof of $\phi(n)$ is $g(n)$ with $g(n)\rightarrow\infty$.

A proof of height $\omega+3$ is a proof with three additional steps below a proof of height $\omega$. More interestingly, a proof of height $\omega+\omega$ might be a proof of $\forall x\phi(x)\vee\forall y\psi(y)$ where for each $n$, we have a proof of $\phi(n)\vee\forall y\psi(y)$ of height $\omega+n$. To find a quantifier-free instantiation of this proof, we'd have to first plug in an $n$ for $x$ and then, at the appropriate level, an $m$ for $y$ to get a proof of $\phi(n)\vee\psi(m)$ of height $g(n)+h(n,m)$.

$ $

Speaking very loosely, the intuitions you describe above are perfectly sensible, but they basically only correspond to what's happening with fairly simple (mostly one quantifier) formulas. Cut-elimination corresponds to extracting computable information, and when you cut formulas with multiple quantifiers together, information has to flow back and forth between the two sides.

Informally, I think of it like this: suppose I want to cut a proof of $$(\forall x\exists y\phi)\vee\psi$$ with a proof of $$(\exists x\forall y\neg\phi)\vee\psi'$$ (cut-elimination is usually easier to think of in a one-sided form). The second proof produces a first proposal for a value of $x$ witnessing $\forall y\neg\phi$. The first proof might refute it by exhibiting a $y$. The second proof can now use that value of $y$ to compute a second guess at what $x$ is, the first proof refutes it again, and so on back and forth. This could go back and forth a large number of times (on the order of the ordinal of the second proof---that is, not just a fixed number of times, but, if the ordinal is something like $\omega+1$, a number of times based on the value of the first $y$, or if it's $\omega+\omega+1$, the first $y$ tells us how many steps we go before a value of $y$ which tells us how many steps we go, etc.)

This description is literally true when viewed through the lens of the functional interpretation. When viewed in terms of infinitary cut-elimination, these "back and forths" correspond to interleaved cuts: we place many copies of the first proof (more precisely, proofs of $\exists y\phi(n,y)\vee\psi$ for various values of $n$) throughout the second proof. Each of these creates new cuts, which correspond to taking sections of the second proof and placing them inside the many copies of the first proof which we've just created.

$ $

I think your indexing on the relationship between the fast growing hierarchy and proof-theoretic ordinals is off by an exponential. The proof theoretic ordinal of $I\Sigma_1$ is $\omega^\omega$, but it only proves the primitive recursive functions total (i.e. $f_n$ with $n<\omega$ in the fast-growing hierarchy). I'm not finding a reference on the exact relationship, but I would guess that the gap is consistent---that in the way two quantifier induction is like $\omega^{\omega^n}$, the Conway chain notation is like $\omega^{\omega^2}$. So, while two quantifier induction suffices, dealing with Conway chain notation will look like a substantial use of two-quantifier induction (indeed, I think it involves three levels of nested induction, two of which are over two-quantifier formulas, which would line up well with an ordinal of $\omega^{\omega^2}$).

Having said that, your question is still perfectly sensible: how does the back and forth I described above get things that are very fast growing. Suppose the first proof, of $(\forall x\exists y\phi)\vee\psi$, has a sensible rate of growth, say, exponential. The second proof is iterating the rate of growth of the first proof, and can iterate it an ordinal number of times based on the height of the second proof. Since the second proof could easily (given perhaps some additional cuts over smaller formulas) have, say, height $\omega^2$. That is, if we take $f_0(n)=n^n$, $f_{\alpha+1}(n)=f_\alpha(f_\alpha(n))$, and $f_\lambda(n)=f_{\lambda[n]}(n)$, we should hit around level $f_{\omega^2}(n)$ in this hierarchy.

Answer 2

As a side issue I'd be interested in knowing how you use $N$ quantifiers to prove well foundedness of an ordinal notation for a stack of $\omega$'s $N$ layers high.

I set myself this as a challenge a few years ago when I was learning this material; here is the solution I came up with. I hope there aren't any bugs.

---

Let's first check that we agree on the setup:

Let $X$ be an ordered set with order relation $\leq$. Then $\omega^X$ is the set of functions $X \to \omega$ such that all but finitely many elements of $X$ map to $0$. We'll write elements of $\omega^X$ to look like sequences: $(a_i)_{i \in X}$, where $i$ maps to $a_i$. We have $(a_i) > (b_i)$ if there is an index $d$ with $a_d > b_d$ and $a_e = b_e$ for $e > d$. (Expressing this in PA requires tons of $\beta$-encoding, but I am going to assume you are already completely comfortable with that and brush those issues under the rug.) The symbol $0$ will denote the minimal element of $\omega$, the minimal element of $X$ and the minimal element of $\omega^{X}$; which one I mean should be clear from context.

Let $\phi$ be a first order statement with a free variable $x$ ranging over $X$. Let $I(x,X,\phi)$ denote the statement: $$ \left( \exists x \in X : \phi(x) \right) \implies \exists z \in X : \phi(z) \ \wedge \ \forall w \in X : \phi(w)\! \implies \! w \geq z $$ In other words, if any element of $X$ obeys $\phi$, then there is a least element of $X$ obeying $\phi$. We say that PA proves $X$ is well-ordered if, for any $\phi$, PA proves $I(x,X,\phi)$.

We want to show that, if PA proves that $X$ is well-ordered, then PA also proves that $\omega^X$ is well ordered.

---

The strategy of the proof is the only thing it could be. I will describe a recipe which, given a first order sentence $\phi(x)$, with $x$ ranging over $\omega^X$, produces a first order sentence $\phi'(x')$ with $x'$ ranging over $X$. I'll then show that $I(x', X, \phi')$ implies $I(x,\omega^X, \phi)$. The sentence $\phi'$ will have three occurrences of $\phi$: One preceded by $\forall \neg$, one preceded by $\exists$ and one preceded by $\exists \forall \neg$. If $\phi$ is in $\Sigma_n$, then these are in $\Pi_n$, $\Sigma_n$ and $\Sigma_{n+1}$ respectively. I think this shows that this construction takes $\Sigma_n$ to $\Sigma_{n+1}$ (but I must admit that I am not fully confident in this argument.)

Write $\omega \uparrow n$ for a towers of $\omega$'s stacked $n$ high. Then this argument reduces proving $I(x,\omega \uparrow n, \phi)$ to proving $I(x', \omega \uparrow (n-1), \phi')$, and the reduces that to $I(x'', \omega \uparrow (n-2), \phi'')$ etcetera, until we finally reach $I(x^{n-1}, \omega, \phi^{n-1})$. In the process, we have added turned a $\Sigma_k$ statement into a $\Sigma_{k+n}$ statement. Of course, $I(x^{n-1}, \omega, \phi^{n-1})$ is an axiom of PA, so we will then be done.

---

For readability, I'll change the notations $\phi'$ and $x'$ to $\delta$ and $d$. In general, I will try to use letters from the beginning of the alphabet for elements of $X$ and letters from the end for elements of $\omega^X$.

Here is the crucial sentence $\delta(d)$: $$\left( \exists x \in \omega^X : \phi(x) \right) \implies \\ {\big[} \exists z \in \omega^X : \phi(z) \ \wedge \ \forall w \in \omega^X : \phi(w)\! \implies \! \left( w \geq z \ \vee \ \forall_{e \geq d} : w_e=z_e \right) {\big]} $$ In other words, $\delta(d)$ is essentially the induction claim $I(x,\omega^X, \phi)$, but we are allowed to have $w<z$ as long as $w$ and $z$ agree on the part of $X$ past $d$.

Rewritten without $\implies$, this is of the form $$\forall_x \neg \phi(x) \vee \exists_z \left( \phi(z) \wedge \forall_w \neg \phi(w) \vee (\mbox{stuff without }\ \phi) \right).$$ So $\delta$ precedes $\phi$ with $\forall \neg$, with $\exists$ and with $\exists \forall \neg$ as promised.

---

What remains is to show that $I(d, \delta, X)$ implies $I(x, \phi, \omega^X)$. You might enjoy doing this yourself more than reading my solution.

If $\phi(x)$ is false for all $x$, then $I(x, \phi, \omega^X)$ is vacuously true. So we may assume that there is an $x$ obeying $\phi(x)$.

Choose $d_1$ large enough that $x_e=0$ for all $e \geq d_1$. Then $\delta(d_1)$ is true because, for any $w \in \omega^X$, we either have $w \geq x$ or $ \forall_{e \geq d_1} : w_e=0$. So there is some $d$ which makes $\delta$ true. Let $d$ be the least element of $X$ which makes $\delta$ true.

If $d=0$, we are done, since $\delta(0)$ is precisely $I(x,X, \phi)$. So assume for the sake of contradiction that $d>0$.

Let $\bar{z} \in \omega^X$ be the element which is promised to exist according to $\delta(d)$. There are only finitely many $i$ for which $\bar{z}_i$ is nonzero. Let $c$ be the greatest such $i$ which is less than $d$. So $\bar{z}$ looks like $$(\ldots, 0,0,0,\bar{z}_c, 0,0, \ldots, 0,0, \ldots, 0,0, \bar{z}_d, 0, 0, \ldots).$$ If $\bar{z}_i$ is zero for all $i<d$, then take $c=0$. Our goal is to prove $\delta(c)$; this will contradict the minimality of $d$ and thus complete the proof.

Let $\ell$ be the smallest element of $\omega$ such that there exists $y \in \omega^X$ with the following properties: $$\phi(y) \ \wedge \ y_c=\ell \ \wedge \ \forall_{e > c} : y_e = \bar{z}_e$$ There is at least one such $\ell$, since we can take $y=\bar{z}$ and $\ell = \bar{z}_c$, so there is a least such $\ell$ because $\omega$ is well ordered. Let $y$ be the element of $\omega^X$ as above.

I claim that taking $y$ in place of $z$ makes $\delta(c)$ true. Let $w$ obey $\phi(w)$. So either $w \geq \bar{z}$ or $\forall_{e \geq d} w_e = \bar{z}_e$. We must show that either $w \geq y$ or $\forall_{e \geq c} w_e = y_e$.

Case 1 There is some $e \geq d$ with $w_e \neq \bar{z}_e$.

Then $w > \bar{z}$. Since $\forall_{f \geq d} : y_f=\bar{z}_f$, we also have $w > y$, as desired.

Case 2 For all $e \geq d$ we have $w_e = \bar{z}_e$. However, there is an $e$ with $c < e < d$ and $w_e \neq \bar{z}_e$.

For $e$ in this range, $\bar{z}_e = y_e = 0$. So $w > y$, as desired.

Case 3: For all $e > c$, we have $w_e = \bar{z}_e$. However, $w_c \neq y_c$.

By the construction of $y$, we have $w_c > y_c$ and thus $w>y$.

Case 4: For all $e \geq c$, we have $w_e =y_e$.

This is the other case in which $\delta(c)$ is true.

We have now proved that $\delta(c)$ is true, contradicting that $d$ was minimal. So, instead, $d$ was $0$. As described above, this concludes the proof. $\square$.

---

I'm afraid I don't understand cut elimination, but Will Sawin suggests above that this is also an answer to your main question.

Answer 3

I like H. Jervell's draft book on proof theory:

• http://folk.uio.no/herman/bevisteori.ps

It explains the use of $\varepsilon_0$ and as a non-expert I found it quite readable. Unfortunately I don't think I can reconstruct the argument from memory, but I thought I'd recommend the book to you.