  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.

Logic