Skip to main content
1 of 4
Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331

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

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

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

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.


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

Noah Schweber
  • 20.5k
  • 10
  • 110
  • 331