A characterization of ordinal analysis

TL;DR

This paper characterizes ordinal analysis as the finest possible partition of certain logical theories based on proof-theoretic ordinals, showing that no coarser equivalence relation can distinguish theories beyond this partition.

Contribution

It proves that the ordinal analysis partition is maximal among equivalence relations satisfying natural conditions related to $ ext{Pi}^1_1$ sentences and adding true $ ext{Sigma}^1_1$ sentences.

Findings

No equivalence relation finer than ordinal analysis partition under given conditions.

Ordinal analysis captures all distinctions made by such equivalence relations.

The results establish the maximality of ordinal analysis in classifying theories.

Abstract

Ordinal analysis induces a partition of $\Sigma^1_1$-definable and $\Pi^1_1$-sound theories 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.