Cyclic Arithmetic Is Equivalent to Peano Arithmetic
Cyclic Arithmetic Is Equivalent to Peano Arithmetic
复制标题
循环算术相当于皮亚诺算术
DOI：
10.1007/978-3-662-54458-7_17
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
A. Simpson
中科院分区：
文献类型：
--
作者：
A. Simpson
循环证明为具有感应和共同感应定义的逻辑提供了一种证明风格，其中证明是循环图，代表通过无限下降的一种参数形式。很容易表明，环状证明可以通过共同诱导来进行证明。因此，循环证明系统至少与具有显式共同诱导规则的相应证明系统一样强大。匡威包容是否存在是一个非平凡的问题。在本文中，我们在一个有趣的情况下解决了这个问题。我们表明，一阶算术的循环公式在Peano算术上等效。证明涉及在二阶算术子系统中正式化循环证明的元理论。
Cyclic proof provides a style of proof for logics with inductive and coinductive definitions, in which proofs are cyclic graphs representing a form of argument by infinite descent. It is easily shown that cyclic proof subsumes proof by coinduction. So cyclic proof systems are at least as powerful as the corresponding proof systems with explicit coinduction rules. Whether or not the converse inclusion holds is a non-trivial question. In this paper, we resolve this question in one interesting case. We show that a cyclic formulation of first-order arithmetic is equivalent in power to Peano Arithmetic. The proof involves formalising the meta-theory of cyclic proof in a subsystem of second-order arithmetic.