系统T对话树的一个显式序数界
An Explicit Ordinal Bound for System T Dialogue Trees
浏览论文内容
中文总结 AI 辅助
本文给出系统T闭项的对话树序数高度低于ε₀的直接证明，通过类型层次计算显式塔式界，并在Agda中形式化验证。
中文摘要 AI 辅助
Escardó的对话解释将哥德尔系统T的每个闭项$t:(\iota\to\iota)\to\iota$（其中$\iota$为自然数类型）指派一棵良基的、可数分支的树$D(t)$。我们给出一个直接证明，表明其经典序数高度低于$\epsilon_0$。更精确地，我们从源项中出现的类型层次计算一个自然数$K(t)\ge2$，并证明$h(D(t))<\theta_{K(t)}$，其中$\theta_0=\omega$且$\theta_{n+1}=\omega^{\theta_n}$。我们的证明将递归子翻译为闭的无穷模板，并通过由普通类型层次索引的有限轮次消除$\beta$-可约式。翻译和每一轮都精确保持对话指称。一个辅助秩$\rho$满足加性替换界；每一轮将秩$\alpha$送至至多$2^\alpha$。将这些估计与可计算的初始界$\omega+m(t)$以及闭基范式$N$的对话高度界$2^{\rho(N)}$相结合，得出所陈述的塔式界。一个保持语义的翻译将结果转移到Escardó的原始组合子解释。我们在Agda中于经典序数上、在显式基础假设下形式化该证明。
英文摘要
Escardó's dialogue interpretation assigns to each closed term $t:(ι\toι)\toι$ of Gödel's System~T a well-founded, countably branching tree $D(t)$, where $ι$ is the natural-number type. We give a direct proof that its classical ordinal height is below $ε_0$. More precisely, we compute a natural number $K(t)\ge2$ from the type levels occurring in the source term and prove $h(D(t))<θ_{K(t)}$, where $θ_0=ω$ and $θ_{n+1}=ω^{θ_n}$. Our proof translates recursors into closed infinitary templates and eliminates $β$-redexes by a finite sequence of passes indexed by ordinary type level. The translation and every pass preserve the dialogue denotation exactly. An auxiliary rank $ρ$ satisfies an additive substitution bound; each pass sends rank $α$ to at most $2^α$. Combining these estimates with a computable initial bound $ω+m(t)$ and a dialogue-height bound $2^{ρ(N)}$ for closed ground normal forms $N$ yields the stated tower bound. A semantics-preserving translation transfers the result to Escardó's original combinatory interpretation. We formalise the proof in Agda over classical ordinals under explicit foundational assumptions.
发表机构
- Capital Normal University（首都师范大学）
- Kean University（基恩大学）
机构由 AI 辅助整理，请以论文原文为准。
