A robust proof-theoretic well-ordering

TL;DR

This paper investigates the ordering of axiomatic theories by their logical strength, especially under the influence of a $ ext{Σ}^1_1$ oracle, establishing genuine pre-well-orderings and unifying different notions of strength.

Contribution

It introduces a robust proof-theoretic framework that unifies various notions of logical strength in the presence of a $ ext{Σ}^1_1$ oracle, enabling genuine pre-well-orderings.

Findings

Different notions of logical strength coincide with a $ ext{Σ}^1_1$ oracle.

Established genuine pre-well-orderings of theories.

Dropped the need for non-mathematical quantification over theories.

Abstract

It is well-known that natural axiomatic theories are pre-well-ordered by logical strength, according to various characterizations of logical strength such as consistency strength and inclusion of $\Pi^0_1$ theorems. Though these notions of logical strength coincide for natural theories, they are not generally equivalent. We study analogues of these notions -- such as $\Pi^1_1$-reflection strength and inclusion of $\Pi^1_1$ theorems -- in the presence of an oracle for $\Sigma^1_1$ truths. In this context these notions coincide; moreover, we get genuine pre-well-orderings of axiomatic theories and may drop the non-mathematical quantification over "natural" theories.