PreprintarXiv licencearXiv
Dilator-based analysis of KP
Abstract
Proof theorists developed various frameworks to analyze impredicative systems like Π11−CA0 or KP; One is an operator-controlled derivation system, and the other is Girard's dilator-based β-logic. In this paper, we provide a functorial formulation of operator-controlled analysis of KP, thereby unifying the two approaches into a single framework. As an application, a new proof of Girard's boundedness theorem is also provided, which states that every Σ1-over-Lω1CK-definable function ω1CK→ ω1CK is bounded by a recursive dilator.
BibTeX
@misc{jeon2026dilatorbased,
title = {{Dilator-based analysis of KP}},
author = {Hanul Jeon},
howpublished = {arXiv},
year = {2026},
month = oct,
doi = {10.48550/arxiv.2608.29157},
eprint = {2608.29157},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2608.29157},
}
RIS
TY - UNPB
TI - Dilator-based analysis of KP
AU - Hanul Jeon
PY - 2026
DA - 2026/10/19
PB - arXiv
DO - 10.48550/arxiv.2608.29157
UR - https://arxiv.org/abs/2608.29157
AB - Proof theorists developed various frameworks to analyze impredicative systems like Π^1_1−CA_0 or KP; One is an operator-controlled derivation system, and the other is Girard's dilator-based β-logic. In this paper, we provide a functorial formulation of operator-controlled analysis of KP, thereby unifying the two approaches into a single framework. As an application, a new proof of Girard's boundedness theorem is also provided, which states that every Σ_1-over-L_ω_1^CK-definable function ω_1^CK→ ω_1^CK is bounded by a recursive dilator.
ER -