Conjectured reflection classifications for labelled Kruskal's theorem

Let KT(ω)\operatorname{KT}_{\ell}(\omega) denote labelled Kruskal's theorem with labels drawn from ω\omega, and let KT(n)\operatorname{KT}_{\ell}(n) denote its restriction to labels below nn. Let Π21-ωRFN(Π21-BI0Π31)\Pi^1_2\text{-}\omega\operatorname{RFN}(\Pi^1_2\text{-}\operatorname{BI}_0\upharpoonright\Pi^1_3) and Π21-RFN(Π21-BI0)\Pi^1_2\text{-}\operatorname{RFN}(\Pi^1_2\text{-}\operatorname{BI}_0) be the corresponding uniform reflection principles over the indicated base theories. Pakhomov–Freund conjectures. The following classifications hold:

RCA0KT(ω)Π21-ωRFN(Π21-BI0Π31),\textsf{RCA}_0\vdash\operatorname{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\,\operatorname{KT}_{\ell}(n)\leftrightarrow \Pi^1_2\text{-}\operatorname{RFN}(\Pi^1_2\text{-}\operatorname{BI}_0).

These conjectures seek proof-theoretic classifications of labelled Kruskal's theorem and its finite-label versions in terms of reflection principles, extending the known classification of unlabelled Kruskal's theorem. The first proposed classification is attributed to F. Pakhomov and the second to A. Freund; their status is not established in the supplied source.

Sources & referencesView supporting material

Primary source

Gabriele Buriola and Andreas Weiermann, “Ordinal Analysis of Well-Ordering Principles, Well Quasi-Orders Closure Properties, and Σ_n-Collection Schema”, arXiv:2511.11196 (2025).

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.