# On the Hierarchy of Natural Theories

James Walsh

###### Abstract.

It is a well-known empirical phenomenon that natural axiomatic theories are
pre-well-ordered by consistency strength. Without a precise mathematical
definition of “natural,” it is unclear how to study this phenomenon
mathematically. We will discuss the significance of this problem and survey
some strategies that have recently been developed for addressing it. These
strategies emphasize the role of reflection principles and ordinal analysis
and draw on analogies with research in recursion theory. We will conclude with
a discussion of open problems and directions for future research.

A version of this paper appeared in the author’s dissertation [34]. Thanks to
Antonio Montalbán for comments on a draft.

##  1\. The consistency strength hierarchy

The starting points of this story are Gödel’s incompleteness theorems. These
theorems establish fundamental restrictions on what can be proven on the basis
of any reasonable axiomatic theory. By a _reasonable_ axiomatic theory I mean
a consistent, recursively axiomatized theory that interprets a modicum of
arithmetic.

######  Theorem 1.1 (Gödel).

No reasonable axiomatic theory is complete.111This is technically Rosser’s
strengthening of Gödel’s Theorem, if we demand only that reasonable theories
are consistent. Gödel used the assumption of $\omega$-consistency in his
proof.

######  Theorem 1.2 (Gödel).

No reasonable axiomatic theory proves its own consistency.

The first incompleteness theorem shows that, no matter what principles we
endorse, there will be questions that are not resolvable on the basis of those
principles. This means that there is no universal axiom system within which
mathematics can be developed. Instead, we are left with a vast array of
axiomatic theories. The second incompleteness theorem yields the primary
method for mapping out this vast array of theories. For reasonable theories
$T$ and $U$, we say that $T\leq_{\mathsf{Con}}U$ if the consistency of $U$
implies the consistency of $T$ over a suitable base theory. As usual,
$T\equiv_{\mathsf{Con}}U$ if $T\leq_{\mathsf{Con}}U$ and
$U\leq_{\mathsf{Con}}T$. Also as usual, $T<_{\mathsf{Con}}U$ if
$T\leq_{\mathsf{Con}}U$ and $U\nleq_{\mathsf{Con}}T$. The notion of strength
that $<_{\mathsf{Con}}$ engenders is known as _consistency strength_.

The structure of _all_ reasonable theories ordered by consistency strength is
quite complicated. As far as I know, the following theorems are folklore:

######  Theorem 1.3 (Folklore).

The ordering $<_{\mathsf{Con}}$ is not _pre-linear_ , i.e., there are theories
$T$ and $U$ such that $T\not\equiv_{\mathsf{Con}}U$, $T\not<_{\mathsf{Con}}U$,
and $U\not<_{\mathsf{Con}}T$.

######  Theorem 1.4 (Folklore).

The ordering $<_{\mathsf{Con}}$ is _ill-founded_ , i.e., there is a sequence
$T_{0}>_{\mathsf{Con}}T_{1}>_{\mathsf{Con}}T_{2}>_{\mathsf{Con}}\dots$ where
each $T_{i}$ is consistent.

All known instances of non-linearity and ill-foundedness have been discovered
by defining theories in an ad-hoc manner using self-reference and other
logical tricks. When one restricts one’s attention to the _natural_ axiomatic
theories—those that arise in practice—ordered by $<_{\mathsf{Con}}$, the
resulting structure is a _pre-well-ordering_.222This is to say that the
induced ordering on the equivalence classes modulo equiconsistency is a well-
ordering. Here is a tiny snapshot of such theories:

$\mathsf{EA},\mathsf{EA}^{+},\mathsf{EA}^{+},I\Sigma_{n},\mathsf{PA},\mathsf{ATR}_{0},\Pi^{1}_{n}\mathsf{CA}_{0},\mathsf{PA}_{n},\mathsf{ZF},\mathsf{AD}^{L(\mathbb{R})}$

The well-ordering phenomenon persists, taking a very liberal view of what
constitutes a “natural” theory. Note that the theories just cited run the
gamut from weak fragments of arithmetic to subsystems of analysis and all the
way to strong extensions of set theory. These theories come from different
areas of mathematics (e.g., arithmetic, analysis, set theory) and often codify
different conceptions of mathematics. Indeed, many of the natural extensions
of set theory that have been investigated are jointly inconsistent, yet
comparable according to consistency strength.

Explaining the contrast between natural axiomatic theories and axiomatic
theories in general is widely regarded as a major outstanding conceptual
problem in mathematical logic. The following passage from a paper of S.
Friedman, Rathjen, and Weiermann is representative:

> The fact that “natural” theories, i.e. theories which have something like an
> “idea” to them, are almost always linearly ordered with regard to logical
> strength has been called one of the great mysteries of the foundations of
> mathematics.  (S. Friedman, Rathjen, Weiermann [10] p. 382)

If it is true that natural axiomatic theories are pre-well-ordered by
consistency strength, and not an illusion engendered by a paucity of examples,
then one would like to prove that it is true. However, the claim that natural
axiomatic theories are pre-well-ordered by consistency strength is not a
strictly mathematical claim. The problem is that we lack a definition of
“natural axiomatic theory.” Without a precise definition of “natural,” it is
not clear how to prove this claim, or even how to state it mathematically.

Here is my plan for the rest of the paper. In §2 I will discuss the relevance
of the pre-well-ordering phenomenon to the search for new axioms in set
theory. In §3–5 I will discuss two research programs that emerged from the
incompleteness theorems, namely, ordinal analysis and the study of iterated
reflection principles. Both programs will play an important role in the
approaches to the pre-well-ordering problem discussed in this paper. In §6 I
will discuss a phenomenon from recursion theory, namely, the well-ordering of
natural Turing degrees by Turing reducibility; this phenomenon is analogous in
many ways to the pre-well-ordering of natural theories by consistency
strength. In §7–10 I will discuss a few different approaches to the pre-well-
ordering problem that have emerged in recent work. Finally, in §11 I will
discuss remaining questions and directions for future research.

##  2\. The search for new axioms

I would like to consider how the well-ordering phenomenon plays out in
practice, namely, in set theory. Indeed, the well-ordering phenomenon has been
a focal point of interest in the search for new axioms extending the standard
$\mathsf{ZFC}$ axioms for set theory.

Set theory has been developed in an explicitly axiomatic fashion, at least
since Zermelo isolated the axioms that are the precursors to the standard
$\mathsf{ZFC}$ axioms. The early progenitors of set theory discovered that
various mathematical structures could be realized in set-theoretic terms and
that their properties could be established on the basis of set-theoretic
reasoning. Thus, set theory constitutes a highly general mathematical
framework. On the other hand, many of the central problems of set theory (such
as the Continuum Hypothesis, the Projective Measure problem, and Suslin’s
Hypothesis) _cannot_ be resolved on the basis of the $\mathsf{ZFC}$ axioms.
This has motivated the search for new axioms for set theory.

Set theorists have investigated many extensions of $\mathsf{ZFC}$, including
large cardinal axioms, determinacy axioms, forcing axioms, and more. Is it
possible to make rational judgments about these principles and their
consequences? Maddy has promoted the maxim “maximize interpretability
strength” as a guiding principle in the search for new axioms (see, e.g, [20,
21]). Let’s call this principle maddy’s maxim. For a large swathe of theories,
including extensions of set theory, maximizing interpretability strength
coincides with maximizing consistency strength. For a sentence $\varphi$ that
is independent of $\mathsf{ZFC}$, one can imagine the following four
possibilities:

  1. (1)

$\varphi$ increases interpretability strength but $\neg\varphi$ does not.

  2. (2)

$\neg\varphi$ increases interpretability strength but $\varphi$ does not.

  3. (3)

Neither $\varphi$ nor $\neg\varphi$ increases interpretability strength.

  4. (4)

Both $\varphi$ and $\neg\varphi$ increase interpretability strength.

It turns out that all four possibilities are realized; in the fourth case we
_cannot_ follow maddy’s maxim or we would land ourselves in inconsistency.
However, this is not typically taken as a refutation of maddy’s maxim. The key
point here is that when one restricts oneself to _natural_ theories, only the
first three possibilities are realized, since natural theories are linearly
ordered by consistency strength. See [15] for a discussion of this point.

Consider once more the variety of extensions of $\mathsf{ZFC}$ that are
investigated by set theorists: large cardinal axioms, axioms of definable
determinacy, forcing axioms, and more. These axiom systems, which have
different motivations and often codify different foundational conceptions of
mathematics, are pre-well-ordered by consistency strength. Indeed, they are
pre-well-ordered according to all the common notions of proof-theoretic
strength (such as 1-consistency strength, $\Pi^{1}_{1}$ reflection strength,
and so on). A consequence is that these axiom systems all converge on
arithmetic statements and even analytic statements. As Steel writes:

> Thus the well-ordering of natural consistency strengths corresponds to a
> well-ordering by inclusion of theories of the natural numbers. There is no
> divergence at the arithmetic level, if one climbs the consistency strength
> hierarchy in any natural way we know of…Natural ways of climbing the
> consistency strength hierarchy do not diverge in their consequences for the
> reals…Let $T,U$ be natural theories of consistency strength at least that of
> “there are infinitely many Woodin cardinals”; then either
> $(\Pi^{1}_{\omega})_{T}\subseteq(\Pi^{1}_{\omega})_{U}$ or
> $(\Pi^{1}_{\omega})_{U}\subseteq(\Pi^{1}_{\omega})_{T}$.  (Steel [31] p.
> 159)

That is, at the level of statements about $\mathbb{R}$, all natural theories
converge; maddy’s maxim and its variants suggest that we ought to endorse the
sentences on which they converge. Thus, the apparent pre-well-ordering of
theories by consistency strength and other notions of proof-theoretic strength
plays a central role in the search for new axioms in set theory.

##  3\. Ordinal analysis

At this point it will be helpful to discuss two research programs that deal
with questions of systematically reducing incompleteness. One is Gentzen’s
program of ordinal analysis and the other is Turing’s program of completeness
via iterated reflection principles. Both programs can be understood as
reactions to the incompleteness theorems. The practitioners of ordinal
analysis have attempted to reduce incompleteness by proving consistency
statements in a systematic way, namely, from ever stronger transfinite
induction principles. Turing’s program, on the other hand, uses the second
incompleteness theorem as the major engine for overcoming incompleteness; the
practitioners of Turing’s program try to systematically effect reductions in
incompleteness by successively adding consistency statements to theories as
new axioms. Both programs will play a major role in the approach to the “great
mystery” discussed here.

Ordinal analysis was developed in the context of _Hilbert’s Program_ , an
early twentieth century research program pioneered by David Hilbert. To combat
skepticism about the cogency of infinitary mathematics, Hilbert proposed to
(i) axiomatize infinitary mathematics and (ii) prove the consistency of the
axioms by finitary means. In 1931, Hilbert’s program reached a major obstacle
in the form of Gödel’s [12] second incompleteness theorem. Indeed, it follows
from Gödel’s theorem that if the principles of finitistic mathematics are
codifiable in a reasonable axiomatic theory, then they do not prove their own
consistency, much less the consistency of stronger theories. Thus, it is
generally agreed that Hilbert’s program failed.

Gentzen was apparently undeterred, however. Not long after Gödel proved the
incompleteness theorems, Gentzen [11] produced a consistency proof of
arithmetic.

######  Theorem 3.1 (Gentzen).

If $\varepsilon_{0}$ is well-founded, then arithmetic is consistent.

The principles invoked in Gentzen’s proof are nearly universally regarded as
finitistically acceptable, except for the principle that the ordinal number
$\varepsilon_{0}$ is well-founded. Gentzen’s consistency proof marked the
beginning of _ordinal analysis_ , a research program whereby similar
consistency proofs have been discovered for a wide range of axiomatic
theories. Developing such a consistency proof for a theory $T$ involves, among
other things, determining the _proof-theoretic ordinal_ of $T$. Informally,
the proof-theoretic ordinal of $T$ is the least ordinal $\alpha$ such that
induction along $\alpha$ suffices to prove the consistency of $T$. Making this
informal definition precise is no easy task, as we shall see.

The methods of ordinal analysis have been used to analyze many theories of
interest, including subsystems of first-order arithmetic, second-order
arithmetic, and set theory. Ordinal analysis has not yet reached the level of
full second-order arithmetic. Nevertheless, it is reasonable to expect that
the existing results are part of a general connection between ordinals and
consistency. Do Gentzen-style methods suffice for proving the consistency of
any axiomatic theory? The following result [16] might _seem_ to suggest a
positive answer ($\mathsf{TI}^{\prec}_{\Pi_{1}}$ is a sentence expressing the
validity of induction for $\Pi_{1}$ predicates along $\prec$):

######  Theorem 3.2 (Kreisel–Shoenfield–Wang).

For any reasonable theory $T$, there is a presentation $\prec$ of a recursive
ordinal such that
$\mathsf{PA}+\mathsf{TI}^{\prec}_{\Pi_{1}}\vdash\mathsf{Con}(T)$.333Though I
state this result in terms of $\mathsf{PA}$, in the original paper it is
stated in terms of the system $Z^{\mu}$ from [14].

This theorem is proved by showing that, for any true $\Pi_{1}$ sentence
$\varphi$, one can encode the truth of $\varphi$ into an ordinal notation
system $\prec$ such that recognizing that $\prec$ has no $\Pi_{1}$ definable
descending sequences is equivalent to recognizing the truth of $\varphi$. One
would presumably not recognize the validity of $\Pi_{1}$ transfinite induction
along such a notation system without knowing the truth of $\varphi$, so one
could not use such a transfinite induction principle to prove $\varphi$. Thus,
the epistemic value of this theorem is limited.

As we will see, this is one version of a pervasive problem known as the
_canonicity problem_. The ordinal notations that are devised to prove Theorem
3.2 are not _natural_ notations. They form a notation system that one would
introduce only in an ad-hoc manner to solve a problem in proof theory. Does
the distinction between the pathological notation systems and the natural
notation systems reflect some intrinsic mathematical properties of the
notation systems? If one had a convincing definition of “natural,” one might
conjecture that, for any reasonable theory $T$, there is a _natural_
presentation $\prec$ of a recursive ordinal such that
$\mathsf{PA}+\mathsf{TI}^{\prec}_{\Pi_{1}}\vdash\mathsf{Con}(T)$. However, at
present there is no convincing evidence that it is possible to precisely
define the “natural” notation systems.

The canonicity problem also makes it difficult to define “proof-theoretic
ordinal,” as suggested earlier. One might try to define the proof-theoretic
ordinal of $T$ as the least ordinal $\alpha$ such that induction along
$\alpha$ (along with finitary methods) suffices to prove the consistency of
$T$. The problem with this definition is that, in formalized theories,
transfinite induction principles are stated in terms of _presentations_ of
ordinals, not the ordinals themselves. Kreisel has shown that it is always
possible to prove the consistency of a reasonable theory by induction along a
sufficiently pathological presentation of $\omega$. Conversely, Beklemishev
has shown that, for any reasonable theory $T$ and recursive ordinal $\alpha$,
there is a sufficiently pathological presentation of $\alpha$ such that
transfinite induction along that presentation (along with finitary methods)
will not suffice to prove the consistency of $T$. When one restricts one’s
attention to “natural” presentations of ordinals, the definition seems to
work, but the current state of affairs is vexing and unsatisfactory.

At present, many conflicting definitions of the “proof-theoretic ordinal” of a
theory have been proposed; these definitions often coincide in crucial cases.
Perhaps the most common definition is this: The proof-theoretic ordinal of a
theory $T$ is the supremum of the order-types of the primitive recursive well-
orderings whose well-foundedness is provable in $T$. This is sometimes called
the $\Pi^{1}_{1}$ ordinal of a theory. Of course, this notion is only useful
for measuring the proof-theoretic strength of theories in which well-
foundedness is expressible, so it does not apply, e.g., to fragments of first-
order arithmetic. Moreover, it is a somewhat coarse notion of strength, since
$\Pi^{1}_{1}$ ordinals are invariant under the addition of true
$\Sigma^{1}_{1}$ sentences to the object theory. Nevertheless, the
$\Pi^{1}_{1}$ ordinal of a theory is an _ordinal_ , not a presentation of an
ordinal, so this is a somewhat robust notion.

##  4\. Turing progressions

The second incompleteness theorem suggests a method for dealing with the first
incompleteness theorem. According to Turing [32], if we endorse the axioms of
a reasonable axiomatic theory $T$, then there is a principled way of extending
$T$, namely, by adopting $T$’s consistency statement as an axiom. Of course,
if one adopts the statement $\mathsf{Con}(T)$ as an axiom, the statement
$\mathsf{Con}(T+\mathsf{Con}(T))$ remains unprovable. However, there is a
principled way of resolving this problem, namely, by adopting
$\mathsf{Con}(T+\mathsf{Con}(T))$ as an axiom. Of course, this engenders a new
problem, but it just as easily engenders a new solution, whence this process
can iterated _ad infinitum_. Given presentations of recursive ordinals in the
language of arithmetic, one can even extend this process into the effective
transfinite.

Naively, we might try to define the iterations of consistency over a theory
$T$ as follows:

  * •

$T_{0}:=T$

  * •

$T_{\alpha+1}:=T_{\alpha}+\mathsf{Con}(T_{\alpha})$

  * •

$T_{\lambda}:=\bigcup_{\alpha<\lambda}T_{\alpha}$ for $\lambda$ a limit.

However, such a definition does not even pin down the theory $T_{\omega+1}$.
According to the definition, $T_{\omega+1}$ is just
$T_{\omega}+\mathsf{Con}(T_{\omega})$, but for $\mathsf{Con}(T_{\omega})$ to
be a statement of arithmetic we must have some effective presentation of
$T_{\omega}$, and there are many choices for the latter. Accordingly, when one
defines iterated consistency statements, one must first fix an ordinal
notation system $\prec$. One can then define the iterations of consistency
along $\prec$ within arithmetic via Gödel’s fixed point lemma. Let me briefly
indicate how this is done; thenceforth I will only give the intuitive
“definitions” by transfinite recursion, trusting the reader to fill in the
details.444For a discussion of this technique and comparisons with other
techniques see the proof of Theorem 3.8 in [5].

We fix a formula $\mathsf{ConFormula}(U,x)$ that formalizes the claim that $x$
is the formula expressing the consistency of $U$. We also fix a formula
$Ax(x,T)$ which formalizes that $x$ is an axiom of $T$. We now want to define
a formula $Ax(x,\alpha,T)$ that defines the axioms of the theory
$\mathsf{Con}^{\alpha}(T)$. We define the formula as the following fixed
point:

$\mathsf{PA}\vdash
Ax(x,\alpha,T)\leftrightarrow\big{(}Ax(x,T)\vee\exists\beta\prec\alpha\mathsf{ConFormula}(\mathsf{Con}^{\beta}(T),x)\big{)}$

Does iteratively endorsing consistency statements in this manner effect a
significant reduction in incompleteness? The following result suggests a
positive answer:

######  Theorem 4.1 (Turing).

For any true $\Pi_{1}$ sentence $\varphi$, there is a presentation $\prec$ of
$\omega+1$ such that $\mathsf{PA}_{\prec}\vdash\varphi$.

This result is known as _Turing’s Completeness Theorem_. At first glance it
may seem that this theorem is epistemically significant: we can come to know
the truth of any $\Pi_{1}$ statement $\varphi$ simply by iterating consistency
statements. How are the consistency statements used in the proof of $\varphi$
? The disappointing response is that they are not used at all. Instead, the
truth of $\varphi$ is encoded into a non-standard description of the base
theory $\mathsf{PA}$, which becomes available at iteration $\omega+1$. Given
this non-standard description of $\mathsf{PA}$, discerning what the theory
$\mathsf{PA}_{\prec}$ is committed to _requires_ knowing the truth-value of
$\varphi$. This is another appearance of the canonicity problem. As far as I
know, this was the initial appearance of the problem, and Turing was the first
to identify it.

Turing was careful not to overstate the epistemic significance of his theorem.
Indeed, he wrote:

> This completeness theorem as usual is of no value. Although it shows, for
> instance, that it is possible to prove Fermat’s last theorem…(if it is true)
> yet the truth of the theorem would really be assumed by taking a certain
> formula as an ordinal formula.  (Turing [32] p. 213)

Nevertheless, one might hope that iterating $\mathsf{Con}$ along _natural_
ordinal notations would also suffice to prove any true $\Pi_{1}$ statement.
Once again, if we had a precise definition of “natural” ordinal notation
systems, we would be able to formulate a precise conjecture; however, no such
characterization of “natural” ordinal notation systems is currently available.

Turing discussed the possibility of using iterated consistency progressions to
measure the strength of $\Pi_{1}$ statements. He wrote:

> We might also expect to obtain an interesting classification of number-
> theoretic theorems according to “depth”. A theorem which required an ordinal
> $\alpha$ to prove it would be deeper than one which could be proved by the
> use of an ordinal $\beta$ less than $\alpha$. However, this presupposes more
> than is justified.  (Turing [32] p. 200)

Naively, one approach would be to assign to each true $\Pi_{1}$ sentence
$\varphi$ the least ordinal $\alpha$ such that
$\mathsf{PA}_{\alpha}\vdash\varphi$ as its measure of complexity. One could
then extend this measure of complexity to theories: the complexity of $T$ is
the least ordinal such that $\mathsf{PA}_{\alpha}\vdash\varphi$ for each
$\Pi_{1}$ theorem $\varphi$ of $T$. Clearly, Turing’s completeness theorem
shows that iterations of consistency depend on presentations of ordinals and
not just on ordinals themselves. The possibility remains, however, that one
could prove informative results of this sort for large swathes of interesting
theories by antecedently fixing some natural notation system; Beklemishev has
recently pursued this possibility, as we will discuss in §5.

Turing’s work was later pursued and greatly extended by Feferman [5]. Feferman
shifted the focus from iterated consistency to iterated reflection principles
of other sorts. Recall that $\mathsf{RFN}(T)$ is the uniform reflection schema
for $T$, that is,

$\mathsf{RFN}(T):=\\{\forall\vec{x}\big{(}\mathsf{Pr}_{T}(\varphi(\vec{x}))\rightarrow\varphi(\vec{x}))\big{)}:\varphi(\vec{x})\in\mathcal{L}_{A}\\}.$

After fixing a presentation $\prec$ of a recursive ordinal, we can then define
iterations of reflection over a theory $T$ so as to satisfy the following
conditions:

  * •

$T^{\mathsf{RFN}}_{0}:=T$

  * •

$T^{\mathsf{RFN}}_{\alpha+1}:=T^{\mathsf{RFN}}_{\alpha}+\mathsf{RFN}(T^{\mathsf{RFN}}_{\alpha})$

  * •

$T^{\mathsf{RFN}}_{\lambda}:=\bigcup_{\alpha<\lambda}T^{\mathsf{RFN}}_{\alpha}$
for $\lambda$ a limit.

Feferman proved that, merely by iterating the uniform reflection schema along
presentations of recursive ordinals, one can accrue resources sufficient, not
only for proving any true $\Pi_{1}$ statement, but for proving _any_ true
arithmetical statement.

######  Theorem 4.2 (Feferman).

For any true arithmetical sentence $\varphi$, there is a presentation $\prec$
of an ordinal $\alpha<\omega^{\omega^{\omega}+1}$ such that
$\mathsf{PA}^{\mathsf{RFN}}_{\prec}\vdash\varphi$.

This result is known as _Feferman’s Completeness Theorem_. In the proof of
this theorem, Feferman used Turing’s technique of encoding the truth of
statements into presentations of recursive ordinals, among other things.
Feferman also proved that there are paths $P$ through Kleene’s $\mathcal{O}$
such that iterating uniform reflection along $P$ is arithmetically complete
[5]. However, no such path is even $\Sigma^{1}_{1}$ definable [6]. That is,
identifying such a path is _more difficult_ than identifying the set of
arithmetical truths. Thus, the epistemic significance of these results—as
Feferman emphasized—is limited.

##  5\. Ordinal analysis via iterated reflection

In recent years there has been interest in the interface between ordinal
analysis and Turing progressions. This research has been motivated by a number
of the drawbacks of the research discussed in the previous two sections.

As discussed in §3, the standard notion of the $\Pi^{1}_{1}$ ordinal of a
theory is (i) only applicable to theories in which “well-foundedness” is
expressible and (ii) insensitive to the true $\Sigma^{1}_{1}$ consequences of
a theory. Building on earlier work of Schmerl [26], Beklemishev [2] introduced
the notion of the $\Pi_{1}$ ordinal of a theory; this notion of “ordinal
analysis” is both (i) suitable for subsystems of first-order arithmetic and
(ii) sensitive to the $\Pi_{1}$ consequences of theories. Iterations of
consistency in the style of Turing play a central role in the definition of
$\Pi_{1}$ ordinals.

First we fix a base theory: Beklemishev uses $\mathsf{EA}^{+}$, a weak
subsystem of arithmetic. The theory $\mathsf{EA}$ is a subsystem of arithmetic
that proves the totality of exponentiation but not superexponentiation;
$\mathsf{EA}$ is just strong enough to carry out arithmetization of syntax in
the standard way. $\mathsf{EA}^{+}$ extends $\mathsf{EA}$ with an axiom
stating the totality of superexponentiation; unlike $\mathsf{EA}$ it can prove
the cut-elimination theorem and its standard corollaries, e.g., Herbrand’s
Theorem. We then fix some natural ordinal notation system and define the
iterations of $\mathsf{EA}^{+}$ so as to satisfy the following conditions:

  1. (1)

$\mathsf{EA}^{+}_{0}:=\mathsf{EA}^{+}$

  2. (2)

$\mathsf{EA}^{+}_{\alpha+1}:=\mathsf{EA}^{+}_{\alpha}+\mathsf{Con}(\mathsf{EA}^{+}_{\alpha})$

  3. (3)

$\mathsf{EA}^{+}_{\lambda}:=\bigcup_{\alpha<\lambda}\mathsf{EA}^{+}_{\alpha}$
for $\lambda$ a limit.

Given a target theory $T$, the $\Pi_{1}$ ordinal of $T$ (relative to the base
theory $\mathsf{EA}^{+}$ and notation system $\prec$) is defined as follows:

$|T|_{\Pi_{1}}:=\mathsf{sup}\\{\alpha:\mathsf{EA}^{+}_{\alpha}\subseteq T\\}$

This definition yields interesting information only if $T$ is conservatively
approximated by iterations of consistency over $\mathsf{EA}^{+}$; that is,
only if $T\equiv_{\Pi_{1}}\mathsf{EA}^{+}_{\alpha}$ where
$\alpha=|T|_{\Pi_{1}}$. Knowing that $T$ is so approximated is useful, because
there are elegant equations, first discovered by Schmerl [26], spelling out
conservation relations between iterated reflection principles. In what follows
$\mathsf{RFN}_{\Pi_{n}}$ is the restriction of the uniform reflection
principle to $\Pi_{n}$ formulas:555This theorem is stated for all ordinal
notations systems. For an appropriate treatment of ordinal notations that
makes sense of this statement see [23].

######  Theorem 5.1 (Schmerl).

For any $n,m\in\mathbb{N}$,

$\mathsf{RFN}_{\Pi_{n+1}}^{\alpha}(\mathsf{EA}^{+})\text{ is
$\Pi_{n}$-conservative over
}\mathsf{RFN}_{\Pi_{n}}^{\omega_{m}(\alpha)}(\mathsf{EA}^{+}).$

One can use these equations to calculate the $\Pi_{1}$ proof-theoretic
ordinals of theories that are conservatively approximated by iterated
consistency statements in a uniform manner.

Clearly, $\Pi_{1}$ ordinals are well-defined for theories of first-order
arithmetic in which well-foundedness is not directly expressible. The
definition is also sensitive to $\Pi_{1}$ sentences. For instance, whereas the
$\Pi_{1}$ ordinal of $\mathsf{PA}$ is $\varepsilon_{0}$, the $\Pi_{1}$ ordinal
of $\mathsf{PA}+\mathsf{Con}(\mathsf{PA})$ is $\varepsilon_{0}\times 2$.

Note that the definition of $\Pi_{1}$ ordinals achieves Turing’s goal of
providing a metric of strength for theories in terms of the number of
iterations of consistency required to capture their $\Pi_{1}$ theorems. It
turns out that this metric of strength is the same one provided by ordinal
analysis (that is, the definition of $\Pi_{1}$ ordinals coincides with other
standard definitions of proof-theoretic ordinal in standard cases). To provide
such a metric of strength, we must fix (in advance) a natural ordinal notation
system. Moreover, the definition only works for theories whose $\Pi_{1}$
fragments can be conservatively approximated by iterated consistency
statements. This is apparently a feature of “natural theories” but not of all
theories. This approach to ordinal analysis was a major inspiration for the
approach to the main topic of this paper discussed in §8.3.

Beklemishev [3, 4] has also advocated for an approach to the canonicity
problem for ordinal notation systems that makes use of reflection principles.
I will briefly describe Beklemishev’s notation system for $\mathsf{PA}$ and
its fragments. The terms are generated by the constant symbol $\top$ and the
function symbols $\mathsf{Con}_{\mathsf{EA}}(\cdot)$,
$1\mathsf{Con}_{\mathsf{EA}}(\cdot)$, $2\mathsf{Con}_{\mathsf{EA}}(\cdot)$,
etc. The ordering on the terms is given, roughly, by consistency strength over
$\mathsf{EA}$.666In fact, Beklemishev uses the ordering $\prec$ defined as
follows: $\alpha\prec\beta$ if
$\mathsf{GLP}\vdash\beta\rightarrow\diamondsuit_{0}\alpha$, where
$\mathsf{GLP}$ is a certain polymodal logic corresponding to provability over
$\mathsf{EA}$. This notation system is well-suited to ordinal analysis via
iterated reflection, since $\mathsf{PA}$ can be conservatively approximated
over $\mathsf{EA}$ by the terms of the notation system, regarded as first-
order theories.

The connection with the canonicity problem is this: If these reflection
principles may be regarded as a _canonical means_ of specifying the theory
$\mathsf{PA}$, then the ordinal notation system (not just the ordinal) has
been extracted from a canonical presentation of $\mathsf{PA}$. Various results
discussed in this paper will lend support to the notion that reflection
principles _are_ canonical, and to the notion that natural theories can be
approximated by iterating reflection principles. However, the results
discussed in this paper seem too coarse grained to isolate Beklemishev’s
notation system as canonical in a way that certain notation systems that give
“wrong” answers for ordinal analysis are not.

##  6\. Turing degree theory

The pre-well-ordering of natural theories is paralleled by a phenomenon in
Turing degree theory. The Turing degrees are not linearly ordered by $<_{T}$.
That is, there are distinct degrees $a$ and $b$ such that $a\nleq_{T}b$ and
$b\nleq_{T}a$. The Turing degrees are also ill-founded. That is, there are
infinite sequences $(a_{n})_{n<\omega}$ such that $a_{k}>_{T}a_{k+1}$ for all
$k$. These two results mean that is neither possible to compare nor to rank
Turing degrees in general.

The degrees that exhibit these pathological properties have been constructed
using ad-hoc recursion-theoretic techniques, like the priority method. When
one restricts one’s attention to _natural_ Turing degrees, the resulting
structure is a well-ordering.

$0,0^{\prime},0^{\prime\prime},\dots,0^{\omega},\dots,\mathcal{O},\dots,0^{\sharp},\dots$

This state of affairs is remarkably similar to the state of affairs on the
proof-theoretic side. Once again, it is not entirely clear how to address this
problem. It is not a wholly mathematical problem since there is no precise
mathematical definition of “natural” Turing degrees.

One oft-noted feature of natural Turing degrees is that their definitions
_relativize_. Relativizing the definition of a Turing degree yields a degree-
invariant function on the reals, where a function $f$ is degree-invariant if
for all reals $A$ and $B$, $A\equiv_{T}B$ implies $f(A)\equiv_{T}f(B)$. For
instance, relativizing the definition of $0^{\prime}$ yields the Turing jump
$\lambda X.X^{\prime}$, relativizing the definition of Kleene’s $\mathcal{O}$
yields the hyperjump $\lambda X.\mathcal{O}^{X}$, relativizing the definition
of $0^{\sharp}$ yields the sharp function $\lambda X.X^{\sharp}$, and so on.

Martin proposed a classification of the degree-invariant functions in terms of
their behavior _almost everywhere_ in the sense of Martin Measure. Recall that
a _cone_ in the Turing degrees is any set of the form $\\{a:a\geq_{T}b\\}$.
Assuming $\mathsf{AD}$, Martin proved that every degree-invariant set of reals
either contains a cone or is disjoint from a cone. Moreover the intersection
of countably many cones contains a cone. Thus, assuming $\mathsf{AD}$, the
function

$\mu(A)=\begin{cases}1&\textrm{ if $A$ contains a cone}\\\ 0&\textrm{ if $A$
is disjoint from a cone}\end{cases}$

is a countably additive measure on the $\sigma$ algebra of degree-invariant
sets. This measure is called _Martin Measure_. In the statement of Martin’s
Conjecture, _almost everywhere_ means almost everywhere with respect to Martin
Measure.

######  Conjecture 6.1 (Martin).

Assume $\mathsf{ZF}+\mathsf{DC}+\mathsf{AD}$. Then

  1. I.

If $f:2^{\omega}\rightarrow 2^{\omega}$ is degree-invariant, and $f$ is not
increasing a.e. then $f$ is constant a.e.

  2. II.

$\leq_{m}$ pre-well-orders the set of degree-invariant functions that are
increasing a.e. If $f$ has $\leq_{m}$ rank $\alpha$, then $f^{\prime}$ has
$\leq_{m}$ rank $\alpha+1$, where $f^{\prime}(x)=f(x)^{\prime}$ for all $x$.

One can view Martin’s Conjecture as a conjecture about the functions in
$L(\mathbb{R})$, since, assuming appropriate large cardinal axioms,
$L(\mathbb{R})$ satisfies $\mathsf{AD}$. Thus, Martin’s Conjecture roughly
states that the only definable degree-invariant functions (up to almost
everywhere equivalence) are constant functions, the identify function, and
iterates of the Turing Jump.

Though Martin’s Conjecture is presently open, many informative partial results
and special cases are known (see [30, 27]). We remind the reader that a
function $f$ is _uniformly degree-invariant_ if there is a recursive $\phi$
such that if $A\leq_{T}B$ via $e$ then $f(A)\leq_{T}f(B)$ via $\phi(e)$. A
function $f$ is _order-preserving_ if $A\leq_{T}B$ implies $f(A)\leq_{T}f(B)$.
Finally, a function $f$ is increasing if, for all $A$, $A\leq_{T}f(A)$.

######  Theorem 6.2 (Slaman–Steel).

Part I of Martin’s Conjecture holds for all uniformly degree-invariant
functions.

######  Theorem 6.3 (Steel).

Part II of Martin’s Conjecture holds for all uniformly degree-invariant
functions.

######  Theorem 6.4 (Slaman–Steel).

If $f$ is a Borel order-preserving function that is increasing a.e., then
there exists an $\alpha<\omega_{1}$ such that $f(x)\equiv_{T}x^{(\alpha)}$
a.e.

######  Theorem 6.5 (Lutz-Siskind).

Part I of Martin’s Conjecture holds for all order-preserving functions.

There are other results that speak to this phenomenon. For instance, Steel
[29] has shown that there cannot be any “simple” descending sequences in the
Turing jump hierarchy, in the following sense:

######  Theorem 6.6 (Steel).

Let $P\subset\mathbb{R}^{2}$ be arithmetic. Then there is no sequence
$(x_{n})_{n<\omega}$ such that for every $n$,

  * (i)

$x_{n}\geq_{T}x^{\prime}_{n+1}$ and

  * (ii)

$x_{n+1}$ is the unique $y$ such that $P(x_{n},y)$.

We will explore the analogy between the recursion-theoretic and proof-
theoretic well-ordering phenomena throughout this paper. On the one hand, we
will describe proof-theoretic theorems from [22, 23, 24, 33] whose statements
and proofs were inspired by this recursion-theoretic research. On the other
hand, we will also describe purely recursion-theoretic results from [19] that
were inspired by the aforementioned proof-theoretic theorems.

##  7\. Interlude

My goal is to bring precision to the question of the pre-well-orderedness of
natural theories and to offer (at least partial) solutions. Before summarizing
this research, I would like to mention three themes that will be interwoven.

The first theme is that many natural theories can be axiomatized by reflection
principles over natural base theories. Indeed, the fragments of natural
theories corresponding to different syntactic complexity classes can often be
conservatively approximated by iterated reflection principles of the
appropriate complexity class.

The second theme is that ordinal analysis is an expression of the well-
ordering phenomenon. For different notions of “proof-theoretic strength,”
there are corresponding notions of “proof-theoretic ordinals.” Insofar as the
proof-theoretic ordinal afforded by some definition of “proof-theoretic
ordinal” measures the proof-theoretic strength of theories, the attendant
method of ordinal analysis well-orders the theories within its ken according
to that notion of strength. The heuristic that we will try to vindicate in
this paper is the following: to calculate the proof-theoretic ordinal of a
theory $T$ is to determine $T$’s rank in the hierarchy of natural theories
ordered by proof-theoretic strength.

The third theme is that reflection principles play a role proof theory
analogous to the role jumps play in recursion theory. Just as natural Turing
degrees are apparently equivalent to ordinal iterates of the Turing jump,
natural theories are apparently equivalent to ordinal iterates (along natural
presentations of well-orderings) of reflection principles. Just as natural
Turing degrees can be obliquely studied in terms of jumps, natural axiomatic
theories can be obliquely studied in terms of reflection principles.

##  8\. Analogues of Martin’s Conjecture

The well-ordering phenomenon is evident in ordinal analysis. Recall that
Beklemishev’s method (see §5) for calculating the proof-theoretic ordinal of a
theory $T$ involves demonstrating that $T$ can be approximated over a weak
base theory by a class of formulas that are well understood. In particular,
the $\Pi_{1}$ fragments of natural theories are often proof-theoretically
equivalent to iterated consistency statements over a weak base theory, whence
these theories are amenable to ordinal analysis. Why are the $\Pi_{1}$
fragments of natural theories proof-theoretically equivalent to iterated
consistency statements?

Our approach to this problem is inspired by Martin’s Conjecture. In
particular, we shift our focus from theories to well-behaved functions on
theories. Specifically, we fix an appropriate base theory $T$ and focus on
functions on finite extensions of $T$ (that is, on sentences). The goal of
this approach is to show that the consistency operator and its iterates are
canonical according to well-motivated but formally precise criteria.

Since Martin’s Conjecture focuses on degree-invariant functions, one might be
tempted to focus on functions that are _extensional_ :

######  Definition 8.1.

A function $\mathfrak{g}$ is _extensional_ over a theory $T$ if for all
$\varphi$ and $\psi$

$\text{if }T\vdash\varphi\leftrightarrow\psi\text{ then
}T\vdash\mathfrak{g}(\varphi)\leftrightarrow\mathfrak{g}(\psi).$

The identity function and constant functions are all extensional; so is the
consistency operator $\varphi\mapsto\mathsf{Con}_{T}(\varphi)$.

By analogy with Martin’s Conjecture, one might conjecture that the consistency
operator and its iterates are canonical among recursive extensional functions.
For instance, one might conjecture that the consistency operator is the
weakest extensional operator that is stronger than the identity operator. In
§8.1–8.2, we will describing some results that are “negative” insofar as they
demonstrate that the consistency operator is not canonical in this sense.

In §8.3, we will describe “positive” results that demonstrate that the
consistency operator is canonical among _monotone_ functions.

######  Definition 8.2.

A function $\mathfrak{g}$ is _monotone_ over a theory $T$ if for all $\varphi$
and $\psi$

$\text{if }T\vdash\varphi\to\psi\text{ then
}T\vdash\mathfrak{g}(\varphi)\to\mathfrak{g}(\psi).$

Note that all monotone functions are extensional but not vice-versa. Extending
the analogy with Martin’s Conjecture, monotone functions are analogous to
order-preserving functions. In §8.3 we will describe some of the major results
demonstrating the canonicity of the consistency operator and its iterates
among recursive monotone functions. We also mention some open problems.

Before describing these results, let’s fix some notation. When I write that
$\varphi$ implies $\psi$ over a theory $T$, I mean that $T+\varphi\vdash\psi$.
When I write that $\varphi$ strictly implies $\psi$, I mean that $\varphi$
implies $\psi$ and $\psi$ does not imply $\varphi$. We write $[\varphi]_{T}$
to denote the equivalence class of $\varphi$ modulo $T$ provable equivalence,
i.e., $[\varphi]_{T}=\\{\psi:T\vdash\varphi\leftrightarrow\psi\\}$. In what
follows by “true” I mean “true according to the standard interpretation
$\mathbb{N}$ of first-order arithmetic.”

###  8.1. Slow Consistency

One can use Rosser-style self-reference to exhibit theories whose deductive
strength is strictly between that of $\mathsf{PA}$ and
$\mathsf{PA}+\mathsf{Con}(\mathsf{PA})$. Indeed, by the second incompleteness
theorem $\mathsf{PA}+\neg\mathsf{Con}(\mathsf{PA})$ is consistent, so by
Rosser’s Theorem there is some sentence $\varphi$ independent from
$\mathsf{PA}+\neg\mathsf{Con}(\mathsf{PA})$. An elementary argument then shows
that $\mathsf{PA}+\big{(}\mathsf{Con}(\mathsf{PA})\vee\varphi\big{)}$ has
deductive strength strictly between $\mathsf{PA}$ and
$\mathsf{PA}+\mathsf{Con}(\mathsf{PA})$.

However, such theories are usually regarded as unnatural. In [10], S.
Friedman, Rathjen, and Weiermann present what they claim is a natural theory
of strictly intermediate strength between $\mathsf{PA}$ and
$\mathsf{PA}+\mathsf{Con}(\mathsf{PA})$. The key notion that they introduce is
a variant of consistency called _slow consistency_ , defined as follows:

$\mathsf{SlowCon}(\mathsf{PA}):=\forall
x\big{(}F_{\varepsilon_{0}}(x)\downarrow\to\mathsf{Con}(I\Sigma_{x})\big{)}$

######  Theorem 8.3 (S. Friedman–Rathjen–Weiermann).

$\mathsf{SlowCon}(\mathsf{PA})$ has strictly intermediate deductive strength
between $\mathsf{PA}$ and $\mathsf{PA}+\mathsf{Con}(\mathsf{PA})$, i.e.:

  1. (1)

$\mathsf{PA}+\mathsf{Con}(\mathsf{PA})$ strictly implies
$\mathsf{SlowCon}(\mathsf{PA})$;

  2. (2)

$\mathsf{PA}$ does not prove $\mathsf{SlowCon}(\mathsf{PA})$, i.e.,
$\mathsf{SlowCon}(\mathsf{PA})$ strictly implies $\top$.

S. Friedman, Rathjen, and Weiermann claim that this is an example of a
“natural” theory with strength strictly between $\mathsf{PA}$ and
$\mathsf{PA}+\mathsf{Con}(\mathsf{PA})$. I am not convinced that this is so;
nevertheless, there are some points that can be made in favor of their claim.
In particular, note that $\mathsf{SlowCon}$ does not involve Rosser orderings
or self-reference in any obvious way; it does not seem to be a statement about
its own code or the lengths of its shortest proofs.777Though “explicit” self-
reference is missing, the definition of $\mathsf{SlowCon}$ still makes use of
the fixed point theorem, covertly, in the presentation of
$F_{\varepsilon_{0}}$. We define $F_{\varepsilon_{0}}$ using effective
transfinite recursion, which we arithmetize after the fact. Effective
transfinite recursion relies on a fixed point argument in the form of the
fixed point theorem. This is evident in the _extensionality_ of
$\mathsf{SlowCon}$. Indeed, relativizing the construction of the slow
consistency statement yields an extensional function. Indeed, for any sentence
$\varphi$, define the slow consistency statement for $\varphi$ as follows:

$\mathsf{SlowCon}(\varphi):=\forall
x\big{(}F_{\varepsilon_{0}}(x)\downarrow\to\mathsf{Con}(I\Sigma_{x}+\varphi)\big{)}$

This function is extensional; for any $\varphi$ and $\psi$,

$\text{if }\mathsf{PA}\vdash\varphi\leftrightarrow\psi\text{ then
}\mathsf{PA}\vdash\mathsf{SlowCon}(\varphi)\leftrightarrow\mathsf{SlowCon}(\psi).$

For more work on slow consistency and its variants, see [7, 8, 9, 13, 25].

###  8.2. Uniform Density

Shavrukov and Visser provided another blow to the canonical status of the
consistency operator. S. Friedman asked them, in conversation, whether “the
consistency operator is, in some sense, the least way to strengthen theories.”
Against this hypothesis, Shavrukov and Visser exhibited an extensional density
function on the Lindenbaum algebra of $\mathsf{PA}$. Let me explain.

For any reasonable theory $T$, there is a recursive density function on the
Lindenbaum algebra of $T$ that is bequeathed to us by Rosser’s version of
Gödel’s first incompleteness theorem. One can use Rosser-style self-reference
to produce, for any sentences $\varphi$ and $\psi$ such that $\varphi$
strictly implies $\psi$, a sentence $\theta$ of strictly intermediate
deductive strength. Since $\psi$ does not imply $\varphi$, this means that
$\psi\wedge\neg\varphi$ is consistent. Hence, one can use Rosser-style self-
reference to find a sentence $\theta$ independent from $\psi\wedge\neg\varphi$
and then takes

$\mathfrak{R}(\varphi,\psi):=\big{(}\varphi\vee(\psi\wedge\theta)\big{)}$

as one’s intermediate sentence.

However, even if $\varphi$ and $\psi$ are natural, it does not seem that
$\mathfrak{R}(\varphi,\psi)$ is natural. In particular, the definition of
$\mathfrak{R}(\varphi,\psi)$ involves self-reference in the choice of
$\theta$. One consequence of this self-reference is that $\mathfrak{R}$ is not
_extensional_. That is, $\mathfrak{R}$ is sensitive to more than the mere
deductive strength of its input over $\mathsf{PA}$. Indeed, $\mathfrak{R}$ is
sensitive to syntactic details like the Gödel codes of its input sentences.

Shavrukov and Visser introduced an alternative recursive density function on
the Lindenbaum algebra of $\mathsf{PA}$ that _is_ extensional. First, they
introduced the following formula:

$\mathsf{SV}(\varphi):=\varphi\wedge\forall
x\big{(}\mathsf{Con}(I\Sigma_{x}+\varphi)\to\mathsf{Con}^{2}(I\Sigma_{x}+\varphi)\big{)}$

The function $\varphi\mapsto\mathsf{SV}(\varphi)$ is extensional in the sense
that whenever $\mathsf{PA}\vdash\varphi\leftrightarrow\psi$ then also
$\mathsf{PA}\vdash\mathsf{SV}^{(}\varphi)\leftrightarrow\mathsf{SV}^{(}\psi)$.
This formula engenders a recursive extensional _density_ function on the
Lindenbaum algebra of $\mathsf{PA}$. Indeed, we may define:

$\mathsf{SV}^{\star}(\varphi,\psi):=\varphi\vee\big{(}\mathsf{SV}(\neg\varphi\wedge\psi)\wedge\psi\big{)}.$

This is a recursive extensional density function on the Lindenbaum algebra of
$\mathsf{PA}$:

######  Theorem 8.4 (Shavrukov–Visser).

For any $\varphi$ and $\psi$ such that $\varphi$ strictly implies $\psi$:

  1. (1)

$\varphi$ strictly implies $\mathsf{SV}^{\star}(\varphi,\psi)$

  2. (2)

$\mathsf{SV}^{\star}(\varphi,\psi)$ strictly implies $\psi$.

In particular, by Theorem 8.4, for any $\varphi$ such that
$\varphi\wedge\mathsf{Con}_{\mathsf{PA}}(\varphi)$ strictly implies $\varphi$,
we have the following:

  1. (1)

$\varphi\wedge\mathsf{Con}_{\mathsf{PA}}(\varphi)$ strictly implies
$\mathsf{SV}^{\star}(\varphi\wedge\mathsf{Con}_{\mathsf{PA}}(\varphi),\varphi)$;

  2. (2)

$\mathsf{SV}^{\star}(\varphi\wedge\mathsf{Con}_{\mathsf{PA}}(\varphi),\varphi)$
strictly implies $\varphi$.

That is,
$\varphi\mapsto\mathsf{SV}^{\star}\big{(}\varphi\wedge\mathsf{Con}_{\mathsf{PA}}(\varphi),\varphi)$
is an extensional function that is strictly stronger than the identity
operator but strictly weaker than the consistency operator. Shavrukov and
Visser wrote that this suggests a negative answer to S. Friedman’s question
whether the consistency operator is “the least way to strengthen theories.”

It is worth mentioning before continuing that the Shvarukov–Visser results do
not apply _only_ to $\mathsf{PA}$. Indeed, these results generalize to _all_
recursively enumerable consistent theories that interpret $\mathsf{R}$ since
the Lindenbaum algebras of such theories are all effectively isomorphic by a
result of Kripke and Pour-El [17].

###  8.3. Monotone operators

Shavrukov and Visser provided a recursive extensional density function on the
Lindenbaum algebra of $\mathsf{PA}$. They asked whether their result could be
improved by providing such a function that is not only extensional but also
_monotone_. The answer to their question is that there is no such function.
Indeed, the consistency operator enjoys canonical status among recursive
monotone operators. In a sense to be made precise, it is the weakest recursive
monotone operator that is stronger than the identity.

Before stating the relevant theorems, let’s fix some notation. Let $T$ be a
sound (i.e., true in the standard model), recursively axiomatized extension of
elementary arithmetic. We write $[\varphi]_{T}$ to denote the equivalence
class of $\varphi$ modulo $T$ provable equivalence, i.e.,
$[\varphi]_{T}=\\{\psi:T\vdash\varphi\leftrightarrow\psi\\}$. Finally, by
“true” we mean “true according to the standard interpretatin $\mathbb{N}$ of
first-order arithmetic.”

######  Theorem 8.5 (Montalbán–W).

Let $\mathfrak{g}$ be recursive and monotone. Suppose that for all consistent
$\varphi$,

  1. (1)

$\varphi\wedge\mathsf{Con}_{T}(\varphi)$ implies $\mathfrak{g}(\varphi)$ and

  2. (2)

$\mathfrak{g}(\varphi)$ strictly implies $\varphi$.

Then for every true $\varphi$, there is a true $\psi$ such that $\psi$ implies
$\varphi$ and
$[\mathfrak{g}(\psi)]_{T}=[\psi\wedge\mathsf{Con}_{T}(\psi)]_{T}.$

This is to say that any recursive monotone function that is strictly stronger
than the identity but weaker than the consistency operator must coincide
“cofinally often” with the consistency operator on true sentences. More
precisely, the functions induced by the consistency operator and
$\mathfrak{g}$ on the Lindenbaum algebra of $T$ coincide cofinally in the
ultrafilter of true sentences. As a corollary we infer the following:

######  Corollary 8.5.1.

There is no monotone function $\mathfrak{g}$ such that for all consistent
$\varphi$,

  1. (1)

$\varphi\wedge\mathsf{Con}_{T}(\varphi)$ strictly implies
$\mathfrak{g}(\varphi)$;

  2. (2)

$\mathfrak{g}(\varphi)$ strictly implies $\varphi$.

Why is the slow consistency operator not a counter-example to this result? The
reason is that if $\mathsf{PA}+\varphi\vdash F_{\varepsilon_{0}}\downarrow$,
then

$\mathsf{PA}+\varphi\vdash\mathsf{SlowCon}(\varphi)\leftrightarrow\mathsf{Con}(\varphi).$

Accordingly, the slow consistency operator and the consistency operator agree
with each other on all inputs that imply the totality of
$F_{\varepsilon_{0}}$, whence they agree cofinally in the ultrafilter of true
sentences.

Theorem 8.5 shows that sufficiently constrained recursive monotone functions
must coincide with the consistency operator _cofinally_ in the ultrafilter of
true sentences. In fact, more can be said. Indeed, in [33] it is shown that
sufficiently constrained recursive monotone functions must coincide with the
consistency operator _in the limit_ within the ultrafilter of true sentences.
Note that “in the limit” plays a role analogous to that which “a.e. in the
sense of Martin measure” does in Martin’s Conjecture.

######  Theorem 8.6 (W).

Let $\mathfrak{g}$ be recursive and monotone such that, for all $\varphi$,
$\mathfrak{g}(\varphi)$ is $\Pi_{1}$. Then one of the following holds:

  1. (1)

There is a true $\psi$ such that, for all $\varphi$ for which $\varphi$
implies $\psi$,

$\varphi\text{ implies }\mathfrak{g}(\varphi).$

  2. (2)

There is a true $\psi$ such that, for all $\varphi$ for which $\varphi$
implies $\psi$,

$\varphi+\mathfrak{g}(\varphi)\text{ implies }\mathsf{Con}_{T}(\varphi).$

This is roughly to say that any recursive monotone operator that must either
be as weak as the identity operator in the limit or as strong as the
consistency operator in the limit.

Theorem 8.5 generalizes into the effective transfinite. For the rest of this
section we will be interested in theories of iterated consistency that are
finitely axiomatized over $T$ (that is, equivalent to $T+\varphi$ for some
sentence $\varphi$). Accordingly, in this section we will work with a
definition of iterated consistency sequences that guarantees this property. To
this end, we fix an effective presentation $\prec$ of a recursive ordinal.
Using Gödel’s fixed point lemma, we define the predicate
$\mathsf{Con}^{\star}$ as follows:

$\mathsf{PA}\vdash\mathsf{Con}^{\star}(\alpha,T)\leftrightarrow\forall\beta\prec\alpha\mathsf{Con}\big{(}T+\ulcorner\mathsf{Con}^{\star}(\beta,T)\urcorner\big{)}$

We use the notation $\mathsf{Con}^{\alpha}(T)$ for
$\mathsf{Con}^{\star}(\alpha,T)$ and we write $T_{\alpha}$ for
$T+\mathsf{Con}^{\alpha}(T)$.

In [22] it is shown that for any recursive monotone $\mathfrak{g}$, for
_arbitrarily strong_ true inputs, $\mathfrak{g}$ must be either as strong as
$\mathsf{Con}_{T}^{\alpha}$ or as weak as $\mathsf{Con}_{T}^{\beta}$ for some
$\beta\prec\alpha$.

######  Theorem 8.7.

Let $\mathfrak{g}$ be monotone. Suppose that for all $\varphi$,

  1. (1)

$\varphi\wedge\mathsf{Con}^{\alpha}_{T}(\varphi)$ implies
$\mathfrak{g}(\varphi)$

  2. (2)

If $[\mathfrak{g}(\varphi)]=[\bot]$, then $\mathfrak{g}(\varphi)$ strictly
implies $\varphi\wedge\mathsf{Con}^{\beta}_{T}(\varphi)$ for all
$\beta\prec\alpha$.

Then for every true $\varphi$, there is a true $\psi$ such that $\psi$ implies
$\varphi$ and
$[\mathfrak{g}(\psi)]_{T}=[\psi\wedge\mathsf{Con}^{\alpha}_{T}(\psi)]_{T}.$

######  Corollary 8.7.1.

There is no monotone function $\mathfrak{g}$ such that for all $\varphi$, if

$[\varphi\wedge\mathsf{Con}_{T}^{\alpha}(\varphi)]_{T}\neq[\bot]_{T},$

  1. (1)

$\varphi\wedge\mathsf{Con}_{T}(\varphi)$ strictly implies
$\mathfrak{g}(\varphi)$ and

  2. (2)

$\mathfrak{g}(\varphi)$ strictly implies $\varphi$.

Ideally, one would be able to generalize Theorem 8.6 to iterates of the
consistency operator in an analogous manner. However, it is not clear at
present how to generalize this result even beyond the first step. This leads
to the following question:

######  Question 8.8.

Let $\mathfrak{g}$ be recursive and monotone such that, for all $\varphi$,
$\mathfrak{g}(\varphi)$ is $\Pi_{1}$. Must it be that one of the following
holds?

  1. (1)

There is a true $\psi$ such that, for all $\varphi$ for which $\varphi$
implies $\psi$,

$\varphi\wedge\mathsf{Con}_{T}(\varphi)\text{ implies }\mathfrak{g}(\varphi).$

  2. (2)

There is a true $\psi$ such that, for all $\varphi$ for which $\varphi$
implies $\psi$,

$\varphi\wedge\mathfrak{g}(\varphi)\text{ implies
}\mathsf{Con}^{2}_{T}(\varphi).$

Theorem 8.7 says that if the range of a monotonic function $\mathfrak{g}$ is
sufficiently constrained, then for some $\varphi$ and some $\alpha$,
$[\mathfrak{g}(\varphi)]_{T}=[\varphi\wedge\mathsf{Con}^{\alpha}_{T}(\varphi)\neq[\bot]_{T}$.
This property still holds even when these constraints on the range of
$\mathfrak{g}$ are relaxed considerably. Indeed, the main theorem of [22]
states that if the strength of any sufficiently nice function $\mathfrak{g}$
is “bounded” by some iterate of the consistency operator, then $\mathfrak{g}$
must somewhere coincide with an iterate of the consistency operator.

######  Theorem 8.9 (Montalbán–W).

Let $\mathfrak{g}$ be recursive and monotone such that, for all $\varphi$,
$\mathfrak{g}(\varphi)$ is $\Pi_{1}$. Then one of the following holds:

  1. (1)

For some $\varphi$, $\varphi\wedge\mathsf{Con}_{T}^{\alpha}(\varphi)$ does not
imply $\mathfrak{g}(\varphi)$;

  2. (2)

For some $\beta\preceq\alpha$ and some $\varphi$,
$[\varphi\wedge\mathfrak{g}(\varphi)]_{T}=[\varphi+\mathsf{Con}_{T}^{\beta}(\varphi)]_{T}\neq[\bot]_{T}$.

In [33] some limitative results on the scope of this approach are established.
In particular, it is shown that the assumption that $\mathfrak{g}$ is
recursive is necessary in the statement of Theorem 8.6. We do this by
exhibiting a function $\mathfrak{g}$ that is limit-recursive but not recursive
which meets the other hypotheses of Theorem 8.6 but does not satisfy the
conclusion. In particular, $\mathfrak{g}$ vacillates between behaving like the
identity operator and the consistency operator, without converging on either.

######  Theorem 8.10 (W).

There is a limit-recursive monotone function $\mathfrak{g}$ such that, for
every $\varphi$, $\mathfrak{g}(\varphi)$ is $\Pi_{1}$, yet for arbitrarily
strong true sentences

$[\varphi\wedge\mathfrak{g}(\varphi)]_{T}=[\varphi+\mathsf{Con}_{T}(\varphi)]_{T}$

and for arbitrarily strong true sentences

$[\varphi\wedge\mathfrak{g}(\varphi)]_{T}=[\varphi]_{T}.$

##  9\. Reflection ranks and ordinal analysis

To understand the apparent _well-foundedness_ of natural theories by proof-
theoretic strength, we now turn our attention to descending sequences of
theories in proof-theoretic hierarchies. In particular, we turn to results,
inspired by Steel’s Theorem 6.6, to the effect that such descending sequence
cannot be simple. Indeed, these results show that descending sequences in
proof-theoretic hierarchies are descriptively complex or contain elements that
are unsound.

###  9.1. Descending sequences

A few theorems concerning descending sequences in proof-theoretic hierarchies
appear in [23]. The first such theorem concerns, not the ordering
$\prec_{\mathsf{Con}}$ on axiomatic theories, but a closely related structure.
We say that a theory is $\Sigma_{2}$-sound if all its $\Sigma_{2}$
consequences are true. It is proved that there are no “simple” descending
sequences in the $\Sigma_{2}$-soundness hierarchy in the following sense:

######  Theorem 9.1 (Pakhomov–W).

There is no recursively enumerable sequence $(T_{n})_{n\in\mathbb{N}}$ of
$\Sigma_{2}$-sound extensions of $B\Sigma_{1}$ such that, for each $n$,
$T_{n}$ proves the $\Sigma_{2}$-soundness of $T_{n+1}$.888In [23] this is
stated as a result about $\mathsf{EA}$ rather than $B\Sigma_{1}$. This is
because we formalize our results in terms of “smooth provability” instead of
using the ordinary provability predicate. Our proof works for smooth
provability, but not ordinary provability, over $\mathsf{EA}$, whereas it
works for both over $B\Sigma_{1}$. Rather than explicate the notion of smooth
provability here we state our result about extensions of $B\Sigma_{1}$.

Theorem 9.1 was inspired by an alternative proof, discovered by H. Friedman,
of Steel’s Theorem 6.6. The adaptability of this proof arguably strengthens
the analogy between the proof-theoretic and recursion-theoretic well-
foundedness phenomena; we revisit this idea in §10.

Theorem 9.1 shows that descending sequences in a certain proof-theoretic
hierarchy cannot be simple in the sense that they cannot be recursively
enumerable. However, the following question remains:

######  Question 9.2.

Is there a limit-recursive sequence $(T_{n})_{n\in\mathbb{N}}$ of
$\Sigma_{2}$-sound extensions of $B\Sigma_{1}$ such that, for each $n$,
$T_{n}$ proves the $\Sigma_{2}$-soundness of $T_{n+1}$?

In fact, Theorem 9.1 is very similar to an earlier theorem of H. Friedman,
Smorynski, and Solovay (see [18, 28]). Gaifman asked whether there is a
recursive sequence $\langle T_{0},T_{1},\dots\rangle$ of consistent r.e.
extensions of $\mathsf{PA}$ such that for all $n$,
$T_{n}\vdash\mathsf{Con}(T_{n_{1}})$. The answer is positive; however, there
are none that are $\mathsf{PA}$-_provably_ descending.

######  Theorem 9.3 (H. Friedman, Smorynski, Solovay).

There is no recursively enumerable sequence $(T_{n})_{n<\omega}$ of consistent
r.e. extensions of $\mathsf{PA}$ such $\mathsf{PA}\vdash\forall
x\mathsf{Pr}_{T_{x}}\big{(}\mathsf{Con}(T_{x+1})\big{)}$.

An alternative proof of Theorem 9.3, similar in style to the proof of Theorem
9.1, is presented in [23].

Theorem 9.1 is the best possible theorem with respect to the syntactic
complexity classes it concerns. To state this precisely, we recall that a
theory is $\Sigma_{1}$-sound if all its $\Sigma_{1}$ consequences are true.
The following theorem demonstrates that Theorem 9.1 is the best possible.

######  Theorem 9.4 (Pakhomov–W).

There exists a recursive sequence $(T_{n})_{n\in\mathbb{N}}$ of
$\Sigma_{1}$-sound extensions of elementary arithmetic such that, for each
$n$, $T_{n}$ proves the $\Sigma_{1}$-soundness of $T_{n+1}$.

The method introduced to prove Theorem 9.1 easily adapts to rule out _all_
descending sequences in another hierarchy of proof-theoretic strength, namely,
the one given by $\Pi^{1}_{1}$-soundness. Recall that a theory is
$\Pi^{1}_{1}$-sound if all its $\Pi^{1}_{1}$ consequences are true.

######  Theorem 9.5 (Pakhomov–W).

There is no sequence $(T_{n})_{n\in\mathbb{N}}$ of $\Pi^{1}_{1}$-sound
extensions of $\mathsf{ACA}_{0}$ such that, for each $n$, $T_{n}$ proves the
$\Pi^{1}_{1}$-soundness of $T_{n+1}$.

Theorem 9.5 rules out descending sequences of theories according to a certain
metric of logical strength. This makes it possible to rank theories according
to this metric of strength. We call the rank of a theory in this hierarchy its
_reflection rank_.

It is worth pausing to note that when one proves that $U$ proves the
consistency of $T$, one often also establishes the stronger fact that $U$
proves the $\Pi^{1}_{1}$-soundness of $T$. Moreover, of course, many natural
theories are $\Pi^{1}_{1}$-sound extensions of $\mathsf{ACA}_{0}$.
Accordingly, Theorem 9.5 delivers some insight into the phenomenon that the
natural axiomatic theories are pre-well-ordered by consistency strength.

###  9.2. Ordinal analysis

Recall that in ordinal analysis, values called _proof-theoretic ordinals_ are
systematically assigned to theories and that, according to conventional
wisdom, proof-theoretic ordinals measure the proof-theoretic strength of
theories. We vindicate this conventional wisdom by proving that for most
theories $T$, the reflection rank of $T$ equals the proof-theoretic ordinal of
$T$. We make the notion of “most theories” precise in the following way
($\mathsf{ACA}_{0}^{+}$ is an axiomatic theory extending $\mathsf{ACA}_{0}$
with the axiom “every set is contained in an $\omega$-model of
$\mathsf{ACA}_{0}$”).

######  Theorem 9.6 (Pakhomov–W).

For any $\Pi^{1}_{1}$-sound extension $T$ of $\mathsf{ACA}_{0}^{+}$, the
reflection rank of $T$ equals the $\Pi^{1}_{1}$ proof-theoretic ordinal of
$T$.

Theorem 9.6 is derived from a variant of Schmerl’s conservation theorem (see
Theorem 5.1) in the context of second-order arithmetic. To precisely state
this variant of Schmerl’s theorem, we introduce some terminology. Let
$\Pi^{1}_{1}(\Pi^{0}_{3})$ be the syntactic complexity class consisting of
formulas of the form $\forall X\varphi(X)$ where $\varphi(X)$ is
$\Pi^{0}_{3}$. Though all $\Pi^{1}_{1}$ formulas are provably equivalent to
such formulas in $\mathsf{ACA}_{0}$, this is not the case in
$\mathsf{RCA}_{0}$. We define $R^{\alpha}_{\Gamma}(T)$ as the result of
iterating $\Gamma$ reflection $\alpha$ many times over $T$. Roughly, the
iterates of reflection are defined as the solutions of the following equation:

$R^{\alpha}_{\Gamma}(T):=\mathsf{RFN}_{\Gamma}\big{(}T+\\{R^{\beta}_{\Gamma}(T):\beta\prec\alpha\\}\big{)}$

We are now ready to state the variant of Schmerl’s formula for second-order
arithmetic:

######  Theorem 9.7 (Pakhomov–W).

For any ordinal notation $\alpha$,

$R^{\alpha}_{\Pi^{1}_{1}}(\mathsf{ACA}_{0})\text{ is
}\Pi^{1}_{1}(\Pi^{0}_{3})\text{ conservative over
}R^{\varepsilon_{\alpha}}_{\Pi^{1}_{1}(\Pi^{0}_{3})}(\mathsf{RCA}_{0}).$

###  9.3. Measuring $\omega$-model reflection via dilators

The results described in §9.1 demonstrate that sufficiently sound theories can
be ranked according to their $\Pi^{1}_{1}$ consequences. More robust claims
are made about theories’ consequences from higher complexity classes, e.g.,
$\Pi^{1}_{2}$, in [24]. The main tool for explicating these claims is a
conservation theorem that reduces $\omega$-model reflection to iterated
$\Pi^{1}_{1}$ reflection. Theorem 9.6 yields thorough proof-theoretic
understanding of the latter in terms of ordinal analysis. Accordingly, these
reductions yield proof-theoretic analyses of $\omega$-model reflection
principles.

The results in this subsection are formalized in $\mathsf{ACA}_{0}$ and
concern the language $\mathbf{L}_{2}$ that extends the standard language of
second-order arithmetic with set-constants $C_{X}$ for all sets $X$.
$\mathbf{L}_{2}$ formulas can be encoded as sets and reasoned about in
$\mathsf{ACA}_{0}$. Boldface notation is used to define the standard syntactic
complexity classes for $\mathbf{L}_{2}.$

The main syntactic reflection principle we consider,
$\boldsymbol{\Pi}^{1}_{1}$-$\mathsf{RFN}(T)$, informally says “all
$\boldsymbol{\Pi}^{1}_{1}$ theorems of $T$ are true.” We will also be
interested in the theories $\boldsymbol{\Pi}^{1}_{1}$-$\mathbf{R}^{\alpha}(T)$
that result from iterating this principle along well-orderings. Informally,
one can think of them as defined inductively, according to the following
equation:

$\boldsymbol{\Pi}^{1}_{1}\text{-}\mathbf{R}^{\alpha}(T):=T+\\{\boldsymbol{\Pi}^{1}_{1}\text{-}\mathsf{RFN}\big{(}T+\boldsymbol{\Pi}^{1}_{1}\text{-}\mathbf{R}^{\beta}(T)\big{)}:\beta<\alpha\\}$

The main semantic principle we consider is an $\omega$ -model reflection
principle. An $\omega$-model is an $L_{2}$ structure whose first-order part is
$\mathbb{N}$ and whose second-order part is some subset of
$\mathcal{P}(\mathbb{N})$. The semantic reflection principle we work with is
“every set is contained in an $\omega$-model of $T$.” The reduction principle
is the following:

######  Theorem 9.8 (Pakhomov–W).

$\mathsf{ACA}_{0}$ proves that for any
$\boldsymbol{\Pi}^{1}_{2}$-axiomatizable $T$, the following are equivalent:

  1. (1)

Every set is contained in an $\omega$-model of $T$.

  2. (2)

$\forall\alpha\big{(}\mathsf{WO}(\alpha)\rightarrow\boldsymbol{\Pi}^{1}_{1}\textrm{-}\mathsf{RFN}(\boldsymbol{\Pi}^{1}_{1}\textrm{-}\mathbf{R}^{\alpha}(T))\big{)}.$

To systematically measure proof-theoretic strength as a function of iterated
$\omega$-model reflection, we must turn to a notion more robust than that of a
proof-theoretic ordinal. The key notion here is that of the _dilator of a
theory_ , which is roughly a function encapsulating the closure conditions
that a theory imposes on the ordinals. More formally, we use the following
definition:

######  Definition 9.9.

The _proof-theoretic dilator_ of a theory $T$ is the following function
$\omega_{1}\cup\\{\infty\\}\to\omega_{1}\cup\\{\infty\\}$:

$|\alpha|\longmapsto|T+\mathsf{WO}(\dot{\alpha})|_{\boldsymbol{\Pi}^{1}_{1}}$

where $\alpha$ ranges over countable linear orders. We write
$|T|_{\boldsymbol{\Pi}^{1}_{2}}$ to denote the proof-theoretic dilator of $T$.

One can pin down how theories’ dilators climb the Veblen hierarchy as a
function of the amount of $\omega$-model reflection postulated. First we
recall the basics of the Veblen hierarchy. A _fixed point_ of a function $f$
on the ordinals is any ordinal $\alpha$ such that $f(\alpha)=\alpha$. We then
define the Veblen functions as follows:

  * •

$\phi_{0}(\gamma)=\omega^{\gamma}$.

  * •

$\phi_{\alpha+1}$ enumerates the fixed points of $\phi_{\alpha}$.

  * •

$\phi_{\lambda}$ enumerates the simultaneous fixed points for
$\delta<\lambda$, i.e., the ordinals that are fixed points of $\phi_{\delta}$
for each $\delta<\lambda$, for a limit $\lambda$.

Now we introduce some notation. For linear orders $\alpha,\beta,\gamma$ we
write $\phi_{\alpha}^{+}(\beta)$ to denote the standard notation system for
the least ordinal strictly above $\beta$ that is a value of $\phi_{\alpha}$
function. And we write $\phi_{\alpha}^{+\gamma}(\beta)$ to denote the standard
notation system for the $\gamma^{th}$ ordinal above $\beta$ that is a value of
$\phi_{\alpha}$-function. We write $\omega\mathbf{R}^{\alpha}(T)$ for the
result of iterating the principle “every set is contained in an $\omega$-model
of…” along $\alpha$ starting with $T$. The strength of iterated $\omega$-model
reflection is characterized via dilators as follows:

######  Theorem 9.10 (Pakhomov–W.).

$\mathsf{ACA}_{0}$ proves that for any linear order $\alpha$

$|\omega\mathbf{R}^{\alpha}(\mathsf{ACA}_{0})|_{\boldsymbol{\Pi}^{1}_{2}}=|\phi_{1+\alpha}^{+}|.$

##  10\. Hyperdegrees

Theorem 9.5 demonstrates that the restriction of the $\Pi^{1}_{1}$-reflection
ordering to $\Pi^{1}_{1}$-sound extensions of $\mathsf{ACA}_{0}$ is _actually_
well-founded, not just well-founded for natural theories. In fact, a similar
phenomenon happens on the recursion-theoretic side when we shift our attention
from the Turing degrees to the _hyperdegrees_. For reals $A$ and $B$, we say
that $A\leq_{H}B$ if $A$ is hyperarithmetical in $B$. For any real $A$, there
is a canonical real $\mathcal{O}^{A}$, known as the _hyperjump_ of $A$, such
that $A<_{H}\mathcal{O}^{A}$. In [19], the technique introduced to prove
Theorem 9.5 is refined to provide a novel proof of the following classic
recursion-theoretic result:

######  Theorem 10.1 (Spector).

There is no sequence $(A_{n})_{n\in\mathbb{N}}$ of reals such that, for each
$n$, $\mathcal{O}^{A_{n+1}}\leq_{H}A_{n}$.

Whereas Spector’s proof relies on the theory of admissible ordinals, the [19]
proof uses Gödel’s second incompleteness theorem.

The analogy between Theorem 9.5 and Theorem 10.1 raises the question: What is
the analogue of ordinal analysis in the hyperdegrees? Indeed, Theorem 10.1
states that the relation $A\prec B$ defined by $\mathcal{O}^{A}\leq_{H}B$ is a
well founded partial order. We call the $\prec$ rank of a real its _Spector
rank_. There is a recursion-theoretically natural characterization of the
Spector ranks of reals:

######  Theorem 10.2 (Lutz–W.).

For any real $A$, the Spector rank of $A$ is $\alpha$ just in case
$\omega_{1}^{A}$ is the $(1+\alpha)^{\text{th}}$ admissible ordinal.

######  Corollary 10.2.1.

Assuming suitable large cardinal hypotheses, for all $X$ on a cone, the
Spector rank of $X$ is $\omega_{1}^{X}$. In particular, for all
$X\geq_{H}0^{\sharp}$, the Spector rank of $X$ is $\omega_{1}^{X}$.

These new proofs and results strengthen the analogy between the proof-
theoretic and recursion-theoretic well-ordering phenomena. According to this
analogy, calculating the least ordinal not recursive in a real is analogous to
calculating the proof-theoretic ordinal of a theory.

##  11\. Conclusions

Why are the natural axiomatic theories pre-well-ordered by proof-theoretic
strength? We have described a few results that point towards an answer,
interweaving the three themes discussed in §7. The emerging picture is that
natural theories are proof-theoretically equivalent to iterated reflection
principles. Moreover, ordinal analysis is a means of calculating the ranks of
natural theories in these hierarchies. I write “hierarchies” since there will
be different hierarchies attending different notions of proof-theoretic
strength, depending, e.g., on the reflection principle they are based on. One
may have to adapt the notion of ordinal analysis to investigate these
different notions of proof-theoretic strength. The claim that ordinal analysis
is a means of calculating the ranks of natural theories should be refined by
further developing the systematic connections between iterated reflection and
proof-theoretic ordinals.

Nevertheless, many questions remain. I have already discussed two of these in
§8.3 and §9.1. I hope that both questions will be answered in such a way that
leads to broad classification theorem. Let me say a bit more about these
questions.

First, Question 8.8: Must any recursive monotone operator that is stronger
than the consistency operator coincide with an iterate of the consistency
operator in the limit? I hope that a positive answer to Question 8.8 leads to
the following classification:

######  Conjecture 11.1.

Let $T$ be a sound r.e. extension of $\mathsf{EA}$. Let $\mathfrak{g}$ be a
non-constant, recursive, monotone function such that, for all $\varphi$,
$\mathfrak{g}(\varphi)$ is $\Pi_{1}$. Let $\prec$ be a nice999For a definition
see [1] §2.3 Definition 1. presentation of a well-ordering. Suppose that for
every $\varphi$,
$T+\varphi+\mathsf{Con}_{T}^{\alpha}(\varphi)\vdash\mathfrak{g}(\varphi)$.
Then for some $\beta\preceq\alpha$ and some true $\varphi$, for all $\psi$
such that $T+\psi\vdash\varphi$,

$[\psi+\mathfrak{g}(\psi)]_{T}=[\psi+\mathsf{Con}_{T}^{\beta}(\psi)]_{T}.$

Second, Question 9.2: How much must we assume to rule out descending sequences
in certain reflection hierarchies? In particular, is there a limit-recursive
sequence of $\Sigma_{2}$-sound theories each of which proves the
$\Sigma_{2}$-soundness of the next? I hope that a positive answer to Question
9.2 leads to the following classification:

######  Conjecture 11.2.

For every $n\in\mathbb{N}$, both of the following hold:

  1. (1)

There exists a $0^{(n)}$-recursive sequence $(T_{n})_{n<\omega}$ of
$\Sigma_{n+1}$-sound r.e. extensions of $B\Sigma_{1}$ such that, for each $n$,
$T_{n}$ proves the $\Sigma_{n+1}$-soundness of $T_{n+1}$.

  2. (2)

There is no $0^{(n)}$-recursive sequence $T(T_{n})_{n<\omega}$ of
$\Sigma_{n+1}$-sound r.e. extensions of $B\Sigma_{1}$ such that, for each $n$,
$T_{n}$ proves the $\Sigma_{n+1}$-soundness of $T_{n+1}$.

Questions 8.8 and 9.2 are precise, but broad, thematic questions also remain.
The canonicity problem—that is, the problem of precisely formulating the
distinction between natural and unnatural ordinal notation systems—remains.
For the reasons indicated in §3–5, progress on this canonicity problem would
almost certainly yield insights into the pre-well-ordering problem. However,
at present, it is not even clear what sorts of progress on the canonicity
problem are possible.

Finally, there are many open problems—such as Martin’s Conjecture and its
kin—on the recursion-theoretic side of the analogy between the two well-
ordering phenomena. I suspect that answers to these recursion-theoretic
questions will shed light on the proof-theoretic questions as well.

## References

  * [1] Lev Beklemishev.  Iterated local reflection versus iterated consistency.  Annals of Pure and Applied Logic, 75(1-2):25–48, 1995.
  * [2] Lev Beklemishev.  Proof-theoretic analysis by iterated reflection.  Archive for Mathematical Logic, 42(6):515–552, 2003.
  * [3] Lev Beklemishev.  Provability algebras and proof-theoretic ordinals, I.  Annals of Pure and Applied Logic, 128(1-3):103–123, 2004.
  * [4] Lev Beklemishev.  Reflection principles and provability algebras in formal arithmetic.  Russian Mathematical Surveys, 60(2):197, 2005.
  * [5] Solomon Feferman.  Transfinite recursive progressions of axiomatic theories.  The Journal of symbolic logic, 27(3):259–316, 1962.
  * [6] Solomon Feferman and Clifford Spector.  Incompleteness along paths in progressions of theories.  The Journal of Symbolic Logic, 27(4):383–390, 1962.
  * [7] Anton Freund.  Proof lengths for instances of the Paris–Harrington principle.  Annals of Pure and Applied Logic, 168(7):1361–1382, 2017.
  * [8] Anton Freund.  Slow reflection.  Annals of Pure and Applied Logic, 168(12):2103–2128, 2017.
  * [9] Anton Freund and Fedor Pakhomov.  Short proofs for slow consistency.  Notre Dame Journal of Formal Logic, 61(1):31–49, 2020.
  * [10] Sy-David Friedman, Michael Rathjen, and Andreas Weiermann.  Slow consistency.  Annals of Pure and Applied Logic, 164(3):382–393, 2013.
  * [11] Gerhard Gentzen.  Die gegenwärtige Lage in der mathematischen Grundlagenforschung. Neue Fassung des Widerspruchsfreiheitsbeweises für die reine Zahlentheorie.  Bull. Amer. Math. Soc. 45 (1939), 812-813, pages 0002–9904, 1939\.
  * [12] Kurt Gödel.  Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.  Monatshefte für mathematik und physik, 38(1):173–198, 1931\.
  * [13] Paula Henk and Fedor Pakhomov.  Slow and ordinary provability for peano arithmetic.  arXiv preprint arXiv:1602.01822, 2016.
  * [14] D. Hilbert and P. Bernays.  Grundlagen der Mathematik, volume 2.  1938\.
  * [15] Peter Koellner.  Independence and large cardinals.  Stanford Encyclopedia of Philosophy, 2010.
  * [16] Georg Kreisel, J Shoenfield, and Hao Wang.  Number theoretic concepts and recursive well-orderings.  Archiv für mathematische Logik und Grundlagenforschung, 5(1-2):42–64, 1960.
  * [17] S. Kripke and M. B. Pour-El.  Deduction-preserving “recursive isomorphisms” between theories.  Fundamenta Mathematicae, Fundamenta Mathematicae.
  * [18] Per Lindström.  Aspects of Incompleteness, volume 10.  Cambridge University Press, 2017.
  * [19] Patrick Lutz and James Walsh.  Incompleteness and jump hierarchies.  Proceedings of the American Mathematical Society, 148(11):4997–5006, 2020.
  * [20] Penelope Maddy.  Believing the axioms I.  The Journal of Symbolic Logic, 53(2):481–511, 1988.
  * [21] Penelope Maddy.  Believing the axioms II.  The Journal of Symbolic Logic, 53(3):736–764, 1988.
  * [22] Antonio Montalbán and James Walsh.  On the inevitability of the consistency operator.  The Journal of Symbolic Logic, 84(1):205–225, 2019.
  * [23] Fedor Pakhomov and James Walsh.  Reflection ranks and ordinal analysis.  The Journal of Symbolic Logic, 2020.
  * [24] Fedor Pakhomov and James Walsh.  Reducing $\omega$-model reflection to iterated syntactic reflection.  arXiv preprint arXiv:2103.12147, 2021.
  * [25] Michael Rathjen.  Long sequences of descending theories and other miscellanea on slow consistency.  IfCoLog Journal of Logics and their Applications, page 1411, 2017\.
  * [26] Ulf R. Schmerl.  A fine structure generated by reflection formulas over primitive recursive arithmetic.  Studies in Logic and the Foundations of Mathematics, 97:335–350, 1979.
  * [27] Theodore A Slaman and John R Steel.  Definable functions on degrees.  In Cabal Seminar 81–85, pages 37–55. Springer, 1988.
  * [28] Craig Smorynski.  Self-Reference and Modal Logic.  Springer Science, 2012.
  * [29] John Steel.  Descending sequences of degrees.  The Journal of Symbolic Logic, 40(1):59–61, 1975.
  * [30] John R Steel.  A classification of jump operators.  The Journal of Symbolic Logic, 47(2):347–358, 1982.
  * [31] John R Steel.  Gödel’s program.  Interpreting Gödel: Critical Essays, pages 153–79, 2014.
  * [32] Alan Mathison Turing.  Systems of logic based on ordinals.  Proceedings of the London mathematical society, 2(1):161–228, 1939\.
  * [33] James Walsh.  A note on the consistency operator.  Proceedings of the American Mathematical Society, 148(6):2645–2654, 2020.
  * [34] James Walsh.  Reflection principles and ordinal analysis.  PhD thesis, UC Berkeley, 2020.