From cut elimination to reverse mathematics

This post explains how methods from ordinal analysis can be used to prove results in reverse mathematics. It may be surprising that this is possible, given that the traditional aims of the two areas are somewhat different: reverse mathematics proves implications between different statements about infinite sets, while ordinal analysis eliminates the infinite from proofs of results about finite objects.

The ordinal analysis of Peano arithmetic

Before we can apply them to reverse mathematics, we need to recall some basic considerations from ordinal analysis itself. This will be done in the present section. Let us begin by considering the following argument for the consistency of Peano arithmetic ( $\mathbf{PA}$ ):

(1) All axioms of $\mathbf{PA}$ are true in the standard structure of the natural numbers.
(2) The axioms and rules of predicate logic are sound.
(3) In view of (1) and (2), we can use induction over proofs to show that all theorems of $\mathbf{PA}$ are true.
(4) Any contradictory statement is false. Hence (3) entails that $\mathbf{PA}$ proves no contradiction.

In view of Gödel’s second incompleteness theorem, it cannot be possible to formalize this argument in $\mathbf{PA}$ . What goes wrong? From the work of Tarski we know that the truth predicate for formulas of first order arithmetic cannot be represented by a formula of the same class. This suggests that we may not be able to formalize the required notion of truth.

On the other hand, it is very much possible to define truth for formulas of bounded quantifier complexity. Why can we not use such a partial truth definition to show that $\mathbf{PA}$ does not prove $0=1$ , given that this formula contains no quantifiers at all? The point is that a proof of a quantifier free formula may still contain intermediate formulas of high quantifier complexity. For the induction in (3), our truth predicate would need to cover these formulas as well.

Cut elimination removes detours through complex intermediate formulas (see this post by Anupam Das). So why does it not save our argument? The problem is that even the (induction) axioms of $\mathbf{PA}$ have unbounded quantifier complexity.

Can we somehow get rid of the induction axioms? We can, even though it requires a somewhat radical step: let us extend our proof system by the infinitary $\omega$ -rule, which allows us to infer $\forall_{x\in\mathbb N}\psi(x)$ once we have proved the premise $\psi(n)$ for each numeral $n\in\mathbb N$ . Infinite proof trees with the $\omega$ -rule will be called $\omega$ -proofs. Observe that logic alone yields

$\varphi(0)\land\forall_{y\in\mathbb N}(\varphi(y)\to\varphi(y+1))\to\varphi(n)$

for each $n\in\mathbb N$ . By the $\omega$ -rule, we can infer

$\forall_{x\in\mathbb N}(\varphi(0)\land\forall_{y\in\mathbb N}(\varphi(y)\to\varphi(y+1))\to\varphi(x)),$

which is logically equivalent to the usual formulation of induction (in which the universal quantifier is moved to the conclusion). Since they are provable, the induction axioms can be dropped in the context of $\omega$ -proofs.

Even though $\omega$ -proofs are infinite, cut elimination is still available, by essentially the same argument. Given that no complex axioms remain, no formula in a cut free proof has more quantifiers than the end formula. Hence a partial truth definition is sufficient to prove soundness by induction over $\omega$ -proofs.

What about formalization in $\mathbf{PA}$ ? Our argument does only require recursive $\omega$ -proofs. These can be represented by the Gödel numbers of the correponding programs (see the particularly elegant approach of Buchholz [1]). The only fact that $\mathbf{PA}$ cannot prove is that all relevant $\omega$ -proofs are well founded, which is needed for the induction.

It is known that cut elimination leads to a superexponential increase in the height of proofs. This remains true for infinite proof trees, but now with respect to the exponential function $\alpha\mapsto\omega^\alpha$ from ordinal arithmetic. In contrast to exponentiation on the natural numbers, this function has fixed points, the least of which is denoted by

$\varepsilon_0=\min\{\alpha\,|\,\omega^\alpha=\alpha\}.$

The order $\varepsilon_0$ can be represented in $\mathbf{PA}$ , by a system of terms that correspond to Cantor normal forms. Since $\varepsilon_0$ is a fixed point of ordinal exponentiation, cut elimination does not lead beyond. For this reason, Peano arithmetic shows that all proofs in our argument are well founded if the same holds for the order $\varepsilon_0$ . This leads to the following result of our ordinal analysis:

Theorem 1 (Gentzen [2]). Primitive recursive arithmetic (which is weaker than $\mathbf{PA}$ ) shows that $\mathbf{PA}$ is consistent if $\varepsilon_0$ is well founded (in the sense that no primitive recursive sequence descends forever).

In view of Gödel’s theorem, it follows that $\mathbf{PA}$ cannot prove the well foundedness of $\varepsilon_0$ . One can extract much more information from the ordinal analysis, in particular about the algorithms that $\mathbf{PA}$ proves to be total. Also, it is relatively straightforward to deduce mathematical independence results, such as Kirby and Paris’s result that Goodstein’s theorem is unprovable in $\mathbf{PA}$ (see [3]).

Connecting to reverse mathematics

Before we explain our application of ordinal analysis, we recall some basic facts about reverse mathematics (see [4] for a comprehensive introduction). Formulas of second order arithmetic express statements about natural numbers (which can be used to code finite objects, such as graphs) and subsets of $\mathbb N$ (which represent countable collections of such objects). An $\omega$ -model is given by a collection $\mathcal S=\{S_i\subseteq\mathbb N\,|\,i\in I\}$ of sets: to evaluate a formula, one assumes that the number variables range over the standard structure $\mathbb N$ , while the set variables range over $\mathcal S$ . For a second order statement $\varphi$ , we can view the following question (2) as a more formal version of the informal question (1):

(1) To which infinite sets do we commit when we accept $\varphi$ ?
(2) What are the closure properties that an arbitrary $\omega$ -model of $\varphi$ must satisfy?

In (2) one will usually restrict attention to $\omega$ -models $\mathcal S$ that satisfy a certain base theory $\mathbf{RCA_0}$ (recursive comprehension axiom), which ensures that $\mathcal S$ is closed under Turing reductions. To state a typical result of reverse mathematics, we recall that a formula is arithmetical if it does not quantify over subsets (but possibly over elements) of $\mathbb N$ . Arithmetical comprehension is the principle that $\{n\in\mathbb N\,|\,\varphi(n)\}$ exists whenever $\varphi$ is an arithmetical formula. The extension of $\mathbf{RCA_0}$ by arithmetical comprehension is denoted by $\mathbf{ACA_0}$ . To view the principle of arithmetical comprehension as a closure property, we point out that $\varphi$ may involve further parameters. Hence the given instance of arithmetical comprehension is satisfied in an $\omega$ -model $\mathcal S$ if we have

$X_0,\dots,X_{n-1}\in\mathcal S\quad\Rightarrow\quad\{n\in\mathbb N\,|\,\varphi(n,X_0,\dots,X_{n-1})\}\in\mathcal S.$

A classical result of reverse mathematics states that an $\omega$ -model of $\mathbf{RCA_0}$ satisfies Kőnig’s lemma (for arbitrary finitely branching trees) if, and only if, it satisfies arithmetical comprehension. In fact, the equivalence holds for arbitrary models of $\mathbf{RCA_0}$ , i.e., even when the first order part of the model is non-standard. We have focused on the weaker formulation in terms of $\omega$ -models as the latter are particularly intuitive.

Our application of ordinal analysis is concerned with iterations of arithmetical comprehension: given an arithmetical formula $\varphi$ , the principle of arithmetical recursion along $\mathbb N$ tells us that there is a sequence $\langle X_n\subseteq\mathbb N\,|\,n\in\mathbb N\rangle$ that satisfies the recursive clause

$X_n=\{m\in\mathbb N\,|\,\varphi(m,n,\langle X_k\,|\,k<n\rangle)\}.$

To make this precise, one should note that $\langle X_k\,|\,k\in I\rangle$ can be coded into the single set $\{(k,m)\,|\,k\in I\text{ and }m\in X_k\}\subseteq\mathbb N$ , where $(k,m)$ refers to the numerical code of the pair.

In the previous section, we have considered the first fixed point $\varepsilon_0$ of ordinal exponentiation. Let us now recall that ordinal exponentiation has a proper class of fixed points, which is enumerated by the function $\alpha\mapsto\varepsilon_\alpha$ . Each order $\varepsilon_\alpha$ can be represented by a system of terms, in which elements of $\alpha$ appear as constant symbols. We can now state the main result that we want to discuss in this post:

Theorem 2. Over $\mathbf{RCA_0}$ , the principle of arithmetical recursion along $\mathbb N$ is equivalent to the statement that $\varepsilon_\alpha$ is a well order whenever the same holds for $\alpha$ .

This result was first established by Marcone and Montalbán [5], who have used methods from computability theory. Afshari and Rathjen [6] have shown that the crucial direction (which deduces arithmetical recursion) can be seen as a relativized version of the ordinal analysis of Peano arithmetic. In the rest of the section, we explain how this relativization works. Let us mention that the literature contains many results that have the same form as Theorem 2. They characterize important principles from reverse mathematics, which range from arithmetical comprehension up to the existence of $\omega$ -models of $\Pi^1_1$ -comprehension (see [7] for a list of references). For several of these results, the only known proof uses ordinal analysis.

A countable coded $\omega$ -model is a collection $\{S_i\subseteq\mathbb N\,|\,i\in I\}$ with $I\subseteq\mathbb N$ , coded into a single subset of $\mathbb N$ . It is not hard to show that arithmetical recursion along $\mathbb N$ is equivalent to the statement that any subset of $\mathbb N$ is contained in a countable coded $\omega$ -model of $\mathbf{ACA_0}$ . To establish the crucial direction of the theorem above, it is thus enough to show that $\omega$ -models of $\mathbf{ACA_0}$ exist. How can ordinal analysis help with this? Well, the ordinal analysis from the previous section concludes that $\mathbf{PA}$ is consistent. The same is then true for $\mathbf{ACA_0}$ , which is a conservative extension of $\mathbf{PA}$ . Together with completeness, it follows that $\mathbf{ACA_0}$ has a model. There is, however, no reason why this should be an $\omega$ -model (i.e., why the first order part should be standard)

To obtain $\omega$ -models of $\mathbf{ACA_0}$ , we recall Shoenfield’s completeness theorem, which (essentially) shows that recursive $\omega$ -proofs are complete for $\omega$ -models. It only remains to show that $\mathbf{ACA_0}$ is consistent with respect to $\omega$ -proofs. This was essentially done in the previous section, but there is one difference: All $\omega$ -proofs in the ordinal analysis of $\mathbf{PA}$ arise from finite proofs, which entails that they have height below $\varepsilon_0$ and bounded cut rank. Both is no longer true in the present application, which explains why we need the entire function $\alpha\mapsto\varepsilon_\alpha$ , rather than just the single value $\varepsilon_0$ .

A wider perspective

Theorem 2 above concerns the reverse mathematics of the statement that $\alpha\mapsto\varepsilon_\alpha$ preserves well foundedness. The reader may object that this is not a statement from mathematical practice. To anticipate this objection, I would like to point out that the well foundedness of $\varepsilon_\alpha$ is closely related to a version of Kruskal’s theorem (for binary trees with leaf labels). This follows from work of Schmidt [8] and Friedman (see Simpson’s paper [9]), which I plan to discuss in a future post.

To conclude, let me mention that our considerations can be lifted to the next type level: instead of relativizing an ordinal analysis to an order $\alpha$ (so that $\varepsilon_0$ turns into $\varepsilon_\alpha$ ), one can also relativize it to an entire transformation $\alpha\mapsto D(\alpha)$ of orders. The author has shown [7] that $\Pi^1_1$ -comprehension is equivalent to the statement that a certain order $\vartheta D$ (which relativizes the Bachmann-Howard ordinal) is well founded whenever the transformation $D$ preserves well foundedness. This does, again, have implications for mathematical practice: it entails that $\Pi^1_1$ -comprehension is equivalent to a uniform version of Kruskal’s theorem, as shown by Rathjen, Weiermann and the present author [10]. This is significant because it means that the uniform Kruskal theorem exhausts the full power of Nash-Williams’s minimal bad sequence method [11], even though the usual Kruskal theorem does not.

References

[1]

W. Buchholz, “Notation systems for infinitary derivations,” Archive for Mathematical Logic, vol. 30, pp. 277-296, 1991.
[Bibtex]

@Article{buchholz-inf-deriv,
author = {Wilfried Buchholz},
title ={Notation systems for infinitary derivations},
journal = {Archive for Mathematical Logic},
volume = {30},
pages ={277-296},
year ={1991},
doi = {10.1007/BF01621472},
}

[2]

G. Gentzen, “Die Widerspruchsfreiheit der reinen Zahlentheorie,” Mathematische Annalen, vol. 112, pp. 493-565, 1936.
[Bibtex]

@Article{gentzen36,
author = {Gerhard Gentzen},
title = {Die {W}iderspruchsfreiheit der reinen {Z}ahlentheorie},
journal = {Mathematische Annalen},
volume = {112},
pages = {493-565},
year = {1936},
doi = {10.1007/BF01565428},
}

[3]

E. A. Cichon, “A short proof of two recently discovered independence results using recursion theoretic methods,” Proceedings of the American Mathematical Society, vol. 87, pp. 704-706, 1983.
[Bibtex]

@Article{cichon-independence,
author = {E. A. Cichon},
title = {A short proof of two recently discovered independence results using recursion theoretic methods},
journal = {Proceedings of the American Mathematical Society},
volume = {87},
pages = {704-706},
year = {1983},
doi = {10.1090/S0002-9939-1983-0687646-0},
}

[4]

S. Simpson, Subsystems of Second Order Arithmetic, Cambridge University Press, 2009.
[Bibtex]

@book{simpson09,
title={Subsystems of Second Order Arithmetic},
author={Stephen Simpson},
series={Perspectives in Logic},
year={2009},
publisher={Cambridge University Press},
doi = {10.1017/CBO9780511581007},
}

[5]

A. Marcone and A. Montalbán, “The Veblen functions for computability theorists,” Journal of Symbolic Logic, vol. 76, pp. 575-602, 2011.
[Bibtex]

@Article{marcone-montalban-veblen,
author = {Alberto Marcone and Antonio Montalb{\'a}n},
title ={The {V}eblen functions for computability theorists},
journal = {Journal of Symbolic Logic},
volume = {76},
pages ={575-602},
year ={2011},
doi = {10.2178/jsl/1305810765},
}

[6]

B. Afshari and M. Rathjen, “Reverse Mathematics and Well-Ordering Principles: A Pilot Study,” Annals of Pure and Applied Logic, vol. 160, pp. 231-237, 2009.
[Bibtex]

@Article{afshari-rathjen-pilot,
author = {Bahareh Afshari and Michael Rathjen},
title ={Reverse Mathematics and Well-Ordering Principles: {A} Pilot Study},
journal = {Annals of Pure and Applied Logic},
volume = {160},
pages ={231-237},
year ={2009},
doi = {10.1016/j.apal.2009.01.001},
}

[7]

A. Freund, “ ${\Pi}^1_1$ -Comprehension as a Well-Ordering Principle,” Advances in Mathematics, vol. 355, 106767, 2019.
[Bibtex]

@article{freund-equivalence,
author = {Anton Freund},
title = {-Comprehension as a Well-Ordering Principle},
journal = {Advances in Mathematics},
volume = {355, 106767},
year = {2019},
doi = {10.1016/j.aim.2019.106767},
}

[8]

D. Schmidt, “Well-Partial Orderings and their Maximal Order Types,” in Well-Quasi Orders in Computation, Logic, Language and Reasoning, P. Schuster, M. Seisenberger, and A. Weiermann, Eds., Springer, 2020, vol. 53, pp. 351-391.
[Bibtex]

@incollection{schmidt-habil,
author = {Diana Schmidt},
title = {Well-Partial Orderings and their Maximal Order Types},
booktitle = {Well-Quasi Orders in Computation, Logic, Language and Reasoning},
editor = {Peter Schuster and Monika Seisenberger and Andreas Weiermann},
series = {Trends in Logic},
volume = {53},
publisher = {Springer},
year = {2020},
pages = {351-391},
doi = {10.1007/978-3-030-30229-0_13},
}

[9]

S. Simpson, “Nonprovability of certain combinatorial properties of finite trees,” in Harvey Friedman’s Research on the Foundations of Mathematics, L. A. Harrington, M. D. Morley, A. Sčědrov, and S. G. Simpson, Eds., North-Holland, 1985, vol. 117, pp. 87-117.
[Bibtex]

@incollection{simpson85,
author = {Stephen Simpson},
title = {Nonprovability of certain combinatorial properties of finite trees},
booktitle = {Harvey Friedman's Research on the Foundations of Mathematics},
publisher = {North-Holland},
year = {1985},
pages = {87-117},
series = {Studies in Logic and the Foundations of Mathematics},
volume = {117},
editor = {L. A. Harrington and M. D. Morley and A. S\v{c}\v{e}drov and S. G. Simpson},
doi = {10.1016/S0049-237X(09)70156-9},
}

[10] A. Freund, M. Rathjen, and A. Weiermann, Minimal bad sequences are necessary for a uniform Kruskal theorem, 2020, arXiv:2001.06380.
[Bibtex]

@misc{frw-kruskal,
author = {Anton Freund and Michael Rathjen and Andreas Weiermann},
title = {Minimal bad sequences are necessary for a uniform {K}ruskal theorem},
year = {2020, arXiv:2001.06380},
}

[11]

C. Nash-Williams, “On well-quasi-ordering finite trees,” Proceedings of the Cambridge Philosophical Society, vol. 59, pp. 833-835, 1963.
[Bibtex]

@Article{nash-williams63,
author = {Crispin Nash-Williams},
title = {On well-quasi-ordering finite trees},
journal = {Proceedings of the Cambridge Philosophical Society},
volume = {59},
pages = {833-835},
year = {1963},
doi = {10.1007/978-0-8176-4842-8_24},
}

5 thoughts on “From cut elimination to reverse mathematics”

Sam Sanders says:

June 3, 2020 at 7:18 pm

While this veers into the “OK boomer” invitation territory, I believe I should point out that Reverse Mathematics started as a project strongly based on proof theory. Check the early papers and ye shall believe!

Perhaps recursion theory was ‘more receptive’, and that direction Reverse Mathematics went.

Anton Freund says:

June 4, 2020 at 2:21 pm

Thanks for pointing this out, Sam!

I should maybe clarify that I wanted to make a conceptual rather than a historical point: Reverse mathematics is often concerned with statements about set existence (e.g. complexity $\Pi^1_2$ ). These statements can fail in $\omega$ -models. Their unprovability can often be shown by methods from computability theory. Ordinal analysis is mostly concerned with statements that hold in all $\omega$ -models (typically complexity $\Pi^0_2$ or $\Pi^0_1$ , in any case below $\Pi^1_1$ ). In the post, I discuss the “surprising” phenomenon that methods from ordinal analysis can be used to prove (equivalences between) $\Pi^1_2$ -statements. If anyone knows further instances of this phenomenon, I would be very interested in references.

To illustrate my point, let me mention Friedman’s result that Kruskal’s theorem is unprovable in ATR_0 (see reference [9]). This is one of my favourite theorems, it is formulated in the framework of reverse mathematics, and–as far as I am aware–the only known proof uses ordinal analysis. However, it is not really an instance of the phenomenon that I discuss in the post: Kruskal’s theorem is a $\Pi^1_1$ -statement (and Friedman’s miniaturization of it is even a $\Pi^0_2$ -statement).

I guess this shows that the post is written from a rather specific viewpoint. One should certainly look beyond to see many more connections between reverse mathematics and ordinal analysis (and proof theory in general).

Pingback: What proof mining is about, Part I - The Proof Theory Blog
Anupam Das says:

June 13, 2020 at 4:11 pm

Hi Anton, thanks for the really interesting post! Framing Theorem 2 in terms of reverse mathematics of preservation of well-foundedness by ordinal operations is a nice perspective.

I have a possibly naive technical question: if for Theorem 2 you are relying on the Completeness Theorem, do you not need $\mathbf{WKL}_0$ in your base theory, on top of $\mathbf{RCA}_0$ ? Or is that not needed for Schoenfinkel’s result? (Or, alternatively, is it subsumed by each of the principles being proved equivalent?)

1. Anton Freund says:
  
  June 15, 2020 at 8:52 am
  
  Hi Anupam, that’s a very good question! Your suspicion is correct: In the crucial direction of Theorem 2, the assumption that $\alpha\mapsto\varepsilon_\alpha$ preserves well foundedness is known to imply arithmetical comprehension, which is stronger than weak König’s lemma (via a result of Girard, see [6] for a reference). I am not entirely sure whether weak König’s lemma is sufficient, or whether you really need arithmetical comprehension: the completeness result for $\omega$ -proofs relies on the fact that an $\omega$ -branching tree has a branch if the Kleene-Brouwer order is ill founded.

The ordinal analysis of Peano arithmetic

Connecting to reverse mathematics

A wider perspective

References

5 thoughts on “From cut elimination to reverse mathematics”

Leave a Reply Cancel reply