发表机构
Vienna University of Technology（维也纳工业大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文将算子控制推导系统与 Girard 基于 dilator 的 $\beta$-逻辑两种框架统一，为 KP 的算子控制分析提供函子形式，并给出 Girard 有界性定理的新证明。
AI 中文摘要
证明理论家开发了多种框架来分析如 $\boldsymbol{\beta}$-逻辑等不可谓词系统，其中一种是算子控制的推导系统，另一种是 Girard 的基于 dilator 的 $\beta$-逻辑。本文为 KP 的算子控制分析提供了函子形式，从而将两种方法统一为单一框架。作为应用，还给出了 Girard 有界性定理的新证明，该定理指出每个在 $L_{\boldsymbol{\beta}}$-上 $\boldsymbol{\beta}$-可定义的函数 $\boldsymbol{\beta} \to \boldsymbol{\beta}$ 都被一个递归 dilator 有界。
英文摘要
Proof theorists developed various frameworks to analyze impredicative systems like $Π^1_1\text{-}\mathsf{CA}_0$ or $\mathsf{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 $\mathsf{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^{\mathsf{CK}}}$-definable function $ω_1^\mathsf{CK}\to ω_1^\mathsf{CK}$ is bounded by a recursive dilator.
Comments33 pages
