Schwichtenberg杆递归闭包定理的直接证明

1979 年 Schwichtenberg 证明了系统 $\text{T}$ 可定义泛函在 Spector 最低类型级 $0$ 和 $1$ 的类规则版 bar recursion 下是封闭的。更确切地说，如果控制 Spector bar recursor 停止条件的泛函 $Y$ 是 $\text{T}$ 可定义的，那么相应的类型级 $0$ 和 $1$ 的 bar recursion 已经是 $\text{T}$ 可定义的。然而，Schwichtenberg 的原始证明依赖于一条通过 Tait 无穷项以及序数递归（$\alpha < \varepsilon_0$）与有限类型原初递归之间对应关系的绕路，这使得在给定具体系统 $\text{T}$ 输入时，难以计算出相应的系统 $\text{T}$ 输出会是什么样子。在本文中，我们提出了一种替代的（更直接的）证明，该证明基于一个显式构造，并通过适当定义的逻辑关系证明其正确性。我们通过一个例子展示这如何在 Schwichtenberg 定理的条件下，给出一个将 bar 递归定义转换为 $\text{T}$ 定义的直截了当的机制。最后，利用该显式构造我们还能轻易陈述一个更锐利的结果：如果 $Y$ 位于片段 $\text{T}_i$ 中，那么为此特定 $Y$ 由 $\text{BR}^{\mathbb{N}, \sigma}$ 构建的项可在片段 $\text{T}_{i + \max \{ 1, \text{level}{\sigma} \} + 2}$ 中定义。