Equivalence of inductive definitions and cyclic proofs under arithmetic
Equivalence of inductive definitions and cyclic proofs under arithmetic
复制标题
算术下归纳定义与循环证明的等价
DOI：
10.1109/lics.2017.8005114
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
M. Tatsuta
中科院分区：
文献类型：
--
作者：
S. Berardi;M. Tatsuta
循环证明系统，称为CLKID-omega，为我们提供了另一种表示归纳定义和有效证明搜索的方法。Brotherston和Simpson在2011年的论文中指出，CLKID-omega的可证明性包括了马丁-洛夫归纳定义的经典系统（称为LKID）的可证明性，并证明了等价性。到今年为止，这种等价性已经成为一个悬而未决的问题。一般来说，Berardi和Tatsuta在FoSSaCS 2017论文中证明了该猜想是错误的。然而，如果我们将两个系统限制为仅自然数归纳谓词，并将Peano算法添加到两个系统中，则Simpson在FoSSaCS 2017论文中证明了该猜想是正确的。本文证明，如果我们添加算术到两个系统，他们成为等价的，即猜想成立。本文的结果包含了Simpson的结果作为特例。为了构造一个循环证明的LKID证明，通过将循环证明切割成子证明，使得在每个子证明中结论是伴随的，假设是芽，证明了循环证明中的每个芽在LKID中都是可证的.利用Podelski-Rybalchenko终止定理从适基性到归纳模式的推广，给出了整体迹条件的归纳原理。为了证明这一扩展，本文还证明了无限拉姆齐定理在皮亚诺算术中是可形式化的。
A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2011 paper by Brotherston and Simpson showed that the provability of CLKID-omega includes the provability of the classical system of Martin-Lof's inductive definitions, called LKID, and conjectured the equivalence. By this year the equivalence has been left an open question. In general, the conjecture was proved to be false in FoSSaCS 2017 paper by Berardi and Tatsuta. However, if we restrict both systems to only the natural number inductive predicate and add Peano arithmetic to both systems, the conjecture was proved to be true in FoSSaCS 2017 paper by Simpson. This paper shows that if we add arithmetic to both systems, they become equivalent, namely, the conjecture holds. The result of this paper includes that of the paper by Simpson as a special case. In order to construct a proof of LKID for a given cyclic proof, this paper shows every bud in the cyclic proof is provable in LKID, by cutting the cyclic proof into subproofs such that in each subproof the conclusion is a companion and the assumptions are buds. The global trace condition gives some induction principle, by using an extension of Podelski-Rybalchenko termination theorem from well-foundedness to induction schema. In order to prove this extension, this paper also shows that infinite Ramsey theorem is formalizable in Peano arithmetic.