递归 $A$ 翻译中的递归表征极限

本文研究了在证明论和程序提取中递归表征的极限，以 refined $A$-translation 为中心例子。refined $A$-translation 由 Berger、Buchholz 和 Schwichtenberg 提出，基于最小算术 $\mathsf{MA}^\omega$ 中递归定义的公式类，特别是 definite 公式和 goal 公式的类。其基本属性之一是对于每个 definite 公式 $D$，都可推出 $D[\bot := F] \to D$。Schwichtenberg 和 Wainer 注意到，这一性质也适用于 definite 公式类之外的公式，并询问所有满足 $D[\bot := F] \to D$ 可派生的公式 $D$ 的有用表征。除了 definite 公式，refined $A$-translation 还涉及三个满足相关性质的公式类。我们展示，这四个性质中没有一个 admits 递归表征。除了这一负面结果外，我们还以两个方向扩展了 refined $A$-translation 的框架。首先，我们将联合词 $\wedge$ 加入 $\mathsf{MA}^\omega$ 的语言中，其原始形式仅包含逻辑联结词 $\forall$ 和 $\to$，并相应地调整公式类。其次，我们呈现相应的略微扩展后的 refined $A$-translation 定理，讨论这些类的可能递归扩展。最后，我们讨论了一个用 Rust 编写的证明器，其实现了理论 $\mathsf{MA}^\omega$ 和这四个公式类。该证明器不被用作结果的形式化验证，而是作为检验 Rust 作为证明助理编程语言的案例研究。我们概述了 Rust 在此设置下的一些优势和缺点，包括其类型系统、对部分构造的支持、所有权和借用模型、模块性以及测试基础设施。