Reflection-principle classifications for labelled Kruskal's theorem

Let KT(ω)\text{KT}_{\ell}(\omega) denote the labelled Kruskal theorem for trees labelled by natural numbers, and let KT(n)\text{KT}_{\ell}(n) denote its restriction to labels below nn. Write Π21-ωRFN(Π21-BI0Π31)\Pi^1_2\text{-}\omega\operatorname{RFN}(\Pi^1_2\text{-}\operatorname{BI}_0\upharpoonright\Pi^1_3) for the relevant ω\omega-reflection principle, and Π21-RFN(Π21-BI0)\Pi^1_2\text{-}\operatorname{RFN}(\Pi^1_2\text{-}\operatorname{BI}_0) for the corresponding uniform reflection principle. Here RCA0\textsf{RCA}_0 is the base theory of recursive comprehension.

Pakhomov–Freund conjectures. The following two equivalences are conjectured:

RCA0KT(ω)Π21-ωRFN(Π21-BI0Π31),\textsf{RCA}_0\vdash \text{KT}_{\ell}(\omega)\leftrightarrow \Pi^1_2\text{-}\omega\operatorname{RFN}(\Pi^1_2\text{-}\operatorname{BI}_0\upharpoonright\Pi^1_3),

and

RCA0nKT(n)Π21-RFN(Π21-BI0).\textsf{RCA}_0\vdash \forall n\,\text{KT}_{\ell}(n)\leftrightarrow \Pi^1_2\text{-}\operatorname{RFN}(\Pi^1_2\text{-}\operatorname{BI}_0).

These proposed classifications aim to determine the proof-theoretic strength of labelled Kruskal's theorem and of its finite-label versions, extending the known classification of unlabelled Kruskal's theorem by Rathjen and Weiermann. The source attributes the first equivalence to F. Pakhomov and the second to A. Freund; no resolution is given here.

Sources & referencesView supporting material

Primary source

Gabriele Buriola and Andreas Weiermann, “Proof-Theoretic Relations between Higman's and Kruskal's theorem, and Independence Results for Tree-like Structures”, arXiv:2511.11297 (2026).

Progress summary

Never refreshed

Nothing recorded yet. Refresh searches the literature and the public web for attempts on this problem, and writes the first summary here.

Solutions 0

No solutions have been posted yet.