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 ():
(1) All axioms of
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
are true.
(4) Any contradictory statement is false. Hence (3) entails that
proves no contradiction.
In view of Gödel’s second incompleteness theorem, it cannot be possible to formalize this argument in . 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 does not prove
, 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 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 -rule, which allows us to infer
once we have proved the premise
for each numeral
. Infinite proof trees with the
-rule will be called
-proofs. Observe that logic alone yields
for each . By the
-rule, we can infer
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 -proofs.
Even though -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
-proofs.
What about formalization in ? Our argument does only require recursive
-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
cannot prove is that all relevant
-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 from ordinal arithmetic. In contrast to exponentiation on the natural numbers, this function has fixed points, the least of which is denoted by
The order can be represented in
, by a system of terms that correspond to Cantor normal forms. Since
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
. This leads to the following result of our ordinal analysis:
Theorem 1 (Gentzen [2]). Primitive recursive arithmetic (which is weaker than
) shows that
is consistent if
is well founded (in the sense that no primitive recursive sequence descends forever).
In view of Gödel’s theorem, it follows that cannot prove the well foundedness of
. One can extract much more information from the ordinal analysis, in particular about the algorithms that
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
(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 (which represent countable collections of such objects). An
-model is given by a collection
of sets: to evaluate a formula, one assumes that the number variables range over the standard structure
, while the set variables range over
. For a second order statement
, 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
?
(2) What are the closure properties that an arbitrary
-model of
must satisfy?
In (2) one will usually restrict attention to -models
that satisfy a certain base theory
(recursive comprehension axiom), which ensures that
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
. Arithmetical comprehension is the principle that
exists whenever
is an arithmetical formula. The extension of
by arithmetical comprehension is denoted by
. To view the principle of arithmetical comprehension as a closure property, we point out that
may involve further parameters. Hence the given instance of arithmetical comprehension is satisfied in an
-model
if we have
A classical result of reverse mathematics states that an -model of
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
, i.e., even when the first order part of the model is non-standard. We have focused on the weaker formulation in terms of
-models as the latter are particularly intuitive.
Our application of ordinal analysis is concerned with iterations of arithmetical comprehension: given an arithmetical formula , the principle of arithmetical recursion along
tells us that there is a sequence
that satisfies the recursive clause
To make this precise, one should note that can be coded into the single set
, where
refers to the numerical code of the pair.
In the previous section, we have considered the first fixed point of ordinal exponentiation. Let us now recall that ordinal exponentiation has a proper class of fixed points, which is enumerated by the function
. Each order
can be represented by a system of terms, in which elements of
appear as constant symbols. We can now state the main result that we want to discuss in this post:
Theorem 2. Over
, the principle of arithmetical recursion along
is equivalent to the statement that
is a well order whenever the same holds for
.
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 -models of
-comprehension (see [7] for a list of references). For several of these results, the only known proof uses ordinal analysis.
A countable coded -model is a collection
with
, coded into a single subset of
. It is not hard to show that arithmetical recursion along
is equivalent to the statement that any subset of
is contained in a countable coded
-model of
. To establish the crucial direction of the theorem above, it is thus enough to show that
-models of
exist. How can ordinal analysis help with this? Well, the ordinal analysis from the previous section concludes that
is consistent. The same is then true for
, which is a conservative extension of
. Together with completeness, it follows that
has a model. There is, however, no reason why this should be an
-model (i.e., why the first order part should be standard)
To obtain -models of
, we recall Shoenfield’s completeness theorem, which (essentially) shows that recursive
-proofs are complete for
-models. It only remains to show that
is consistent with respect to
-proofs. This was essentially done in the previous section, but there is one difference: All
-proofs in the ordinal analysis of
arise from finite proofs, which entails that they have height below
and bounded cut rank. Both is no longer true in the present application, which explains why we need the entire function
, rather than just the single value
.
A wider perspective
Theorem 2 above concerns the reverse mathematics of the statement that 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
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 (so that
turns into
), one can also relativize it to an entire transformation
of orders. The author has shown [7] that
-comprehension is equivalent to the statement that a certain order
(which relativizes the Bachmann-Howard ordinal) is well founded whenever the transformation
preserves well foundedness. This does, again, have implications for mathematical practice: it entails that
-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
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
@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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)

[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
[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},
}
![[doi]](https://prooftheory.blog/wp-content/plugins/papercite/img/external.png)
[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},
}
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.
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
). These statements can fail in
-models. Their unprovability can often be shown by methods from computability theory. Ordinal analysis is mostly concerned with statements that hold in all
-models (typically complexity
or
, in any case below
). In the post, I discuss the “surprising” phenomenon that methods from ordinal analysis can be used to prove (equivalences between)
-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
-statement (and Friedman’s miniaturization of it is even a
-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).
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
in your base theory, on top of
? Or is that not needed for Schoenfinkel’s result? (Or, alternatively, is it subsumed by each of the principles being proved equivalent?)
Hi Anupam, that’s a very good question! Your suspicion is correct: In the crucial direction of Theorem 2, the assumption that
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
-proofs relies on the fact that an
-branching tree has a branch if the Kleene-Brouwer order is ill founded.
“Let us begin by considering the following argument for the consistency of Peano arithmetic (\mathbf{PA}): […] ”
Well, I recommend the paper: T. J. Stępień, Ł. T. Stępień, “On the Consistency of the Arithmetic System”, J. Math. Syst. Sci. 7, No.2, 43-55 (2017) ; arXiv:1803.11072, where a proof of consistency of Arithmetic System was published. This proof had been done within this Arithmetic System.
Dear Łukasz, If I understand you correctly: This is not possible in view of Gödel’s second incompleteness theorem. Best, Anton
Dear Anton
Thank you very much for your response. You have written “This is not possible in view of Gödel’s second incompleteness theorem”, yes but UNLESS Arithmetic System is inconsistent.
Let me remind that in March 2019, on FOM website, a discussion concerning Artemov’s paper “The Provability of Consistency” (arXiv:1902.07404v4) started. He wrote in abstract of this paper, among others “We consider consistency in its standard form “no sequence of formulas S is a derivation of a contradiction.” Using partial truth definitions, for each derivation S in PA we construct a finitary proof that S does not contain 0 = 1. This establishes consistency for PA by finitary means and vindicates, to some extent, Hilbert’s consistency program.” ALTHOUGH this fact, this paper was discussed on FOM website (among others, by you), and cited in some other papers.
When several weeks later I posted there my message “concerning provability of consistency”, about the paper T. J. Stępień, Ł. T. Stępień, “On the Consistency of the Arithmetic System”, J. Math. Syst. Sci. 7, No.2, 43-55 (2017) ; arXiv:1803.11072, then ONLY response was message from Alex Blum (everyone can read this on FOM website).
I informed by e-mail, some number of people, about the paper T. J. Stępień, Ł. T. Stępień, “On the Consistency of the Arithmetic System”, J. Math. Syst. Sci. 7, No.2, 43-55 (2017) ; arXiv:1803.11072. Very often reply was silence, some people were replying similarly to you (I would like to thank to you and to them for the responses), some people were trying to discuss about the issue proving of consistency of Arithmetic within Arithmetic, in this paper (and I would like to thank to them very much), but after giving some arguments by me, they gave up. Several people reacted positively (and I would like to thank to them very much, too). Certain professor mailed to me (I would like to thank to him very much, too), about 2 months ago, that he would find an error in this paper, but until today neither he nor anybody else reported any error or mistake in this paper.
I have posted my previous message here, becaues this is actually puzzling that citing the paper T. J. Stępień, Ł. T. Stępień, “On the Consistency of the Arithmetic System”, in another paper, talk, handbook or guide etc., is quite hard for the authors of these publications. Even if the author of such paper, talk, handbook or guide etc., does not want to say authoritatively that this paper T. J. Stępień, Ł. T. Stępień, “On the Consistency of the Arithmetic System”, is all right (i.e. the proof of consistency of Arithmetic System, was done there within this System), then he could write at least that FOR EXAMPLE “In the opinion of the authors of the paper T. J. Stępień, Ł. T. Stępień, “On the Consistency of the Arithmetic System”, J. Math. Syst. Sci. 7, No.2, 43-55 (2017) ; arXiv:1803.11072, their proof of consistency of Arithmetic System had been done within this System. The author leaves the conclusions to the readers.” .