UC Berkeley

It is a well-known empirical phenomenon that natural axiomatic theories are pre-well-ordered by proof-theoretic strength. However, without a precise definition of ``natural,'' it is not clear how to explain this observation in a strictly mathematical way. One expression of the pre-well-ordering phenomenon comes from ordinal analysis, a research program wherein ordinals are assigned to natural theories; these ordinals are commonly understood as measuring the ``strength'' of the theories to which they are assigned. Our goal in this dissertation is to formulate and prove statements that provide insight into the pre-well-ordering phenomenon.

Part I contains an investigation of the pre-well-ordering phenomenon in the setting of first-order arithmetic. One method for determining the proof-theoretic ordinal of a theory $T$ involves showing that $T$ can be conservatively approximated by iterating consistency statements over a weak base theory. This technique yields informative results only for natural theories. Why can natural theories be conservatively approximated by iterating consistency statements? Our explanation is that the consistency operator and its iterates into the effective transfinite are canonical as functions on theories. To this end, we prove that any recursive monotone function on finitely axiomatized theories that is everywhere bounded by an iterate of the consistency operator must coincide somewhere with some iterate of the consistency operator. We also prove that any recursive monotone function on finitely axiomatized theories must be either as weak as the identity operator in the limit or as strong as the consistency operator in the limit.

Part II contains an investigation of the pre-well-ordering phenomenon in the setting of second-order arithmetic. In second-order arithmetic it is possible to formalize $\Pi^1_1$ reflection, which provides a more robust measurement of proof-theoretic strength than consistency strength. We prove that the behavior exhibited by natural theories with respect to consistency strength is exhibited in general with respect to $\Pi^1_1$ strength in the following sense: there is no sequence $(T_n)_{n<\omega}$ 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}$. This means that it is possible to rank the $\Pi^1_1$ sound extensions of $\mathsf{ACA}_0$ by proof-theoretic strength. We prove that for every $\Pi^1_1$ sound extension $T$ of $\mathsf{ACA}_0^+$ the rank of $T$ is exactly the proof-theoretic ordinal of $T$; this vindicates the common wisdom that ordinal analysis measures the proof-theoretic strength of natural theories. Along the way we prove two far-reaching conservation theorems. First, $\alpha$ iterated $\Pi^1_1$ reflection of $\mathsf{ACA}_0$ is $\Pi^1_1(\Pi^0_3)$ conservative over $\varepsilon_\alpha$ iterated $\Pi^1_1(\Pi^0_3)$ reflection of $\mathsf{RCA}_0$. Second, for any $\Pi^1_2$ axiomatizable $T$, every set is contained in an $\omega$ model if and only if, for every well order $\alpha$, $\alpha$ iterated $\Pi^1_1$ reflection for $T$ is $\Pi^1_1$ sound. Finally, we use the techniques introduced to prove these results to provide a purely proof-theoretic demonstration of a classical theorem of recursion theory: there is no sequence $(A_n)_{n<\omega}$ such that, for each $n$, $ \mathcal{O}^{A_{n+1}} \leq_H A_n $. This engenders a well-founded ranking of the real numbers; we prove for almost all reals $A$, the rank of $A$ is $\omega_1^A$. These results strengthen the analogy between the pre-well-ordering of natural theories by proof-theoretic strength in proof theory and the pre-well-ordering of reals under descriptive complexity.

Part III contains reflections on foundational issues. The main foundational applications of ordinal analysis to date are in Hilbert's program and modifications thereof. Instead, I emphasize the \emph{explanatory} value of ordinal-theoretic consistency proofs over their \emph{justificatory} value. Whether, for instance, Gentzen's consistency proof convinces us \emph{that} arithmetic is consistent, it explains \emph{why} arithmetic is consistent. On this basis, I argue against certain restrictive norms on mathematical practice. For instance, I argue against the norm that consistency proofs ought to be carried out using only constructive methods. Though this restriction is reasonable if one is attempting to convince a constructivist skeptic, it loses force when one instead seeks a combinatorial explanation of a theory's consistency.