$Π_2$ strength of KP

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.

• There is a paper "Classifying the provably total set functions of $\mathsf{KP}$ and $\mathsf{KP}(\mathcal{P})$" by J. Cook and M. Rathjen (see arxiv.org/pdf/1610.02194.pdf ). Their Theorem 6.2 isn't exactly what you need but fairly close. I think that with some additional efforts their technique should give the result that you want. Feb 29, 2020 at 12:48
• Also there is an unpublished result of mine about an analogue of Schmerl's formula for $\mathsf{KP}$ from which it is fairly easy to derive your conjectured result. See slides mathnet.ru:8080/PresentFiles/22127/kpomega_via_reflection.pdf . Also there are recordings of my talks (in Russian) on the subject mathnet.ru/php/… , mathnet.ru/php/… Feb 29, 2020 at 12:51
• @FedorPakhomov Theorem 6.2 appears to work. If $\text{KP}⊢∀x∃y \, φ(x,y)$ (with $Δ_0$ $φ$), we can consider $f$ with $f(x)$ being the least $L_α(x)⊨∃y \, φ(x,y)$, so it suffices to consider functions. Also, the paper notes that for each individual proof, the result of Theorem 6.2 is provable in KP; and the theory in the conjecture should also work as it can set up enough of the notation system. (Also, your analysis of iterated reflection in subsystems of KP is interesting.) Would you like to expand all the comments into an answer? Mar 1, 2020 at 2:11