Proof-theoretic dilator conjecture for 00^\sharp

Working over ZFC\mathsf{ZFC} with the existence of 00^\sharp, let TT be a Π31\Pi^1_3-sound extension of ACA0\mathsf{ACA}_0. View 00^\sharp as a dilator.

Proof-theoretic dilator conjecture. The proof-theoretic ordinals satisfy

TΠ31(0)=T+0Π11[0].|T|_{\Pi^1_3}(0^\sharp)=|T+\exists 0^\sharp|_{\Pi^1_1[0^\sharp]}.

This proposes a proof-theoretic interpretation of TΠ31(P)|T|_{\Pi^1_3}(P) for an (n1)(n-1)-ptyx with suitable definability, extending the paper’s main result beyond the Π21\Pi^1_2 setting. The source gives no evidence of a resolution.

Sources & referencesView supporting material

Primary source

Hanul Jeon, “Proof-theoretic dilator and intermediate pointclasses”, arXiv:2501.11220 (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.