算术归纳定义的循环证明
摘要：通过对Peano算术的推理扩展（有限迭代）的归纳定义的研究，我们调查了循环证明理论。这些理论对于对某些“不可捉摸”的理论进行推理分析是至关重要的；此外，我们的循环系统自然地包含了辛普森的循环算术。 我们的主要结果是，算术归纳定义的循环和归纳系统具有相同的能力。我们进行了一种元数学论证，通过闭包序数上形式归纳的方式在二阶算术中对循环证明的正确性进行了形式化，接着依靠保守性结果进行了证明。这种方法受到了辛普森和达斯对循环算术的方法的启发，然而我们还必须进一步解决一个困难：我们归纳定义的闭包序数（围绕Church-Kleene）远超过适当元理论的证明论序数（围绕Bachmann-Howard），所以无法直接对它们的记号进行归纳。因此，我们更倾向于在二阶算术中对（递归）序数的理论进行形式化。
作者：Anupam Das and Lukas Melgaard
论文ID：2306.08535
分类：Logic
分类简称：math.LO
提交时间：2023-06-16