The behavior of higher proof theory I: Case $\Sigma^1_2$

TL;DR

This paper extends the understanding of proof-theoretic ordinals by establishing an equivalence between various comparison methods for $oldsymbol{ ext{Sigma}}^1_2$-consequences modulo true $oldsymbol{ ext{Pi}}^1_2$-sentences, generalizing previous results.

Contribution

It proves the equivalence between $oldsymbol{ ext{Sigma}}^1_2$-proof-theoretic ordinal, consequence, and reflection comparisons modulo true $oldsymbol{ ext{Pi}}^1_2$-sentences, advancing higher proof theory.

Findings

Established the equivalence between $oldsymbol{ ext{Sigma}}^1_2$-proof-theoretic ordinal and consequence comparison.

Connected $oldsymbol{ ext{Sigma}}^1_2$-proof-theoretic ordinal with the analogue of the reflection rank.

Extended prior results from $oldsymbol{ ext{Sigma}}^1_1$ to $oldsymbol{ ext{Sigma}}^1_2$-sentences.

Abstract

Walsh [MR4525964, Zbl 1569.03151] has shown that comparing proof-theoretic ordinals is equivalent to comparing $\Pi^1_1$-consequence comparison and $\Pi^1_1$-reflection comparison, all modulo true $\Sigma^1_1$-sentences. In this paper, we prove the analogous result for $\Sigma^1_2$-consequences modulo true $\Pi^1_2$-sentences, that is, the equivalence between $\Sigma^1_2$-proof-theoretic ordinal comparison, $\Sigma^1_2$-consequence comparison, and $\Sigma^1_2$-reflection comparison, all modulo true $\Pi^1_2$-sentences. We also examine the connection between $\Sigma^1_2$-proof-theoretic ordinal and $\Sigma^1_2$-analogue of the robust reflection rank in Pakhomov-Walsh [MR4362917, Zbl 1511.03018]