Characterizations of ordinal analysis

Abstract

Ordinal analysis is a research program wherein recursive ordinals are assigned to axiomatic theories. According to conventional wisdom, ordinal analysis measures the strength of theories. Yet what is the attendant notion of strength? In this paper we present abstract characterizations of ordinal analysis that address this question. First, we characterize ordinal analysis as a partition of $\Sigma^1_1$-definable and $\Pi^1_1$-sound theories, namely, the partition whereby two theories are equivalent if they have the same proof-theoretic ordinal. We show that no equivalence relation $\equiv$ is finer than the ordinal analysis partition if both: (1) $T\equiv U$ whenever $T$ and $U$ prove the same $\Pi^1_1$ sentences; (2) $T\equiv T+U$ for every set $U$ of true $\Sigma^1_1$ sentences. In fact, no such equivalence relation makes a single distinction that the ordinal analysis partition does not make. Second, we characterize ordinal analysis as an ordering on arithmetically-definable and $\Pi^1_1$-sound theories, namely, the ordering wherein $T< U$ if the proof-theoretic ordinal of $T$ is less than the proof-theoretic ordinal of $U$. The standard ways of measuring the strength of theories are consistency strength and inclusion of $\Pi^0_1$ theorems. We introduce analogues of these notions -- $\Pi^1_1$-reflection strength and inclusion of $\Pi^1_1$ theorems -- in the presence of an oracle for $\Sigma^1_1$ truths, and prove that they coincide with the ordering induced by ordinal analysis.