Krivine经典实现的塔尔斯基理论

本文提出了关于Krivine经典实现解释的形式化理论，以一阶皮亚诺算术($\mathsf{PA})$为例。为了将该理论表述为$\mathsf{PA}$的扩展，我们首先将Krivine的原始定义修改为类似于Kleene直觉主义实现（用于Heyting算术）的数值实现。通过添加额外谓词符号对实现进行公理化，我们获得了一个可以形式化实现$\mathsf{PA}$每个定理的第一阶理论$\mathsf{CR}$。虽然$\mathsf{CR}$本身是$\mathsf{PA}$的保守扩展，但加入一种大致表述为“实现蕴含真理”的反射原理后，$\mathsf{CR}$即可基本等价于塔尔斯基理论$\mathsf{CT}$（类型化组合真理），而$\mathsf{CT}$已知比$\mathsf{PA}$在证明论上更强。因此，$\mathsf{CT}$可被视为经典实现的形式化理论。我们还证明，一种较弱的反射原理（保持实现与真理之间的区别）对$\mathsf{CR}$同样具有$\mathsf{CT}$的相同强度。此外，我们对$\mathsf{CR}$及其变体的超限迭代进行了形式化，然后确定了它们的证明论强度。