Characterizations of ordinal analysis

TL;DR

This paper provides an abstract characterization of ordinal analysis, linking it to equivalence relations and orderings on theories based on proof-theoretic ordinals, and explores its relation to notions of theory strength.

Contribution

It offers novel abstract characterizations of ordinal analysis as a partition and an ordering of theories, connecting it to proof-theoretic ordinals and strength measures.

Findings

Ordinal analysis characterized as a partition of theories with same proof-theoretic ordinal.

No finer equivalence relation than the ordinal analysis partition under certain conditions.

Ordinal analysis corresponds to an ordering based on proof-theoretic ordinals, aligning with strength measures.

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.