I am looking for a characterization of the $Π_2$ statements provable in KP.
Here, KP (often denoted KPω) is the Kripke-Platek set theory, including infinity and full induction on ordinals. Here is my conjecture (which the answer(s) can tweak if appropriate).
Conjecture: A $Π_2$ statement is provable in KP iff it is provable in primitive recursive set theory plus (schema over $n$) $∀α∈\mathrm{Ord} \,\, Ω_{\text{BH},n}(α)∈\mathrm{Ord}$.
Here, $Ω_{\text{BH},n}(α)$ is the nth element of the standard fundamental sequence above $α$ for $Ω_\text{BH}(α)$ (without requiring for $Ω_\text{BH}(α)$ to be an ordinal), and $Ω_\text{BH}(α)$ is the analog of the Bachmann-Howard ordinal above $α$.
Primitive recursive set theory can be weakened to a weak base theory (extensionality, foundation (without full induction), infinity, closure under rudimentary functions) plus $∀x ∀y ∃z=L_{\mathrm{rank}(x)}(\mathrm{trcl}(y))$ where $\mathrm{trcl}$ is the transitive closure.
Related results
The Bachmann-Howard ordinal $Ω_\text{BH}$ is the $Π^1_1$ proof ordinal of KP. All $Π_2$ statements provable in KP hold in $L_{Ω_\text{BH}}$. (Note that $Π_2$ is very expressive in ZFC, but its expressiveness drops if all sets are countable, and especially if the universe is also not closed under hyperjumps.)
A somewhat related result is that all $Π_2^\mathcal{P}$ statements provable in $\text{KP}(\mathcal{P}) + AC$ hold in $V_{Ω_\text{BH}}$ (Relativized ordinal analysis: The case of Power Kripke-Platek set theory). This is despite $\text{KP}(\mathcal{P})$ including powerset and with collection expanded accordingly.
While proof ordinals are commonly used for $Π^1_1$ statements, their relevance is much broader. For example, not only is $Γ_0$ the proof ordinal of $\text{ATR}_0$, but over $\text{RCA}_0$, $\text{ATR}_0 ⇔ ∀X \, (\mathrm{WO}(X) ⇔ \mathrm{WO}(φ_X(0)))$ (in $\text{RCA}_0$, $\mathrm{WO}$ means lack of infinite descending sequences; $φ$ is Veblen fix-point function), and also $∀X \, (\mathrm{WO}(X) ⇔ \mathrm{WO}(Γ(X)))$ iff every $X$ is inside an $ω\text{-model}$ of $\text{ATR}_0$ (Omega-models and well-ordering principles).
An application
KP is inconsistent with $V = L_{Ω_\text{BH}}$ since (provably in KP) it is not an admissible set/class. However, we can correct this by using (essentially) the well-founded part. Below, $\mathrm{Ord}=\mathrm{wfp}(Ω_\text{BH}(α))$ means that every ordinal is isomorphic to an initial segment of $Ω_\text{BH}(α)$, with $Ω_\text{BH}(α)$ being the linear order for the standard notation system for the analog of Bachmann-Howard ordinal above $α$.
Consequences of the conjecture:
* KP + $∃α∈\mathrm{Ord} \,\, \mathrm{Ord}=\mathrm{wfp}(Ω_\text{BH}(α))$ is $Π_2$ conservative over KP.
* For every statement $φ$, KP + $∃S (φ^S ∧ \mathrm{Ord}=\mathrm{wfp}(Ω_\text{BH}(\mathrm{rank}(S)))$ is $Σ_1$ conservative over KP + $∃S \, φ^S$
The proof uses that adding the same $Σ_2$ statement to both sides preserves $Π_2$-conservativity, as well as an easy conservation result for the weak base theory.
The significance of the consequences is the following. A canonical ordinal analysis of some natural set theory is expected to include all ordinals that have a canonical definition in the theory, and not just the recursive ones. Which ordinals have a canonical definition is vague, but we can make it more precise by requiring that, consistently with the theory, all ordinals are included.
And a positive answer to the question will imply that for example, KP + $L_α ⊨ \text{ZFC}$ is relatively consistent with the Bachmann-Howard notation system capturing all ordinals above $α$ in terms of ordinals below $α$. Now, a limitation of KP is that it does not prove existence of admissible ordinals above $α$, so the next step may be $Π^1_1-\text{CA}_0$, as described in the question Ordinal analysis and nonrecursive ordinals.
