一句话：证明含 Martin-Löf 归纳定义的经典系统 LKID 与循环证明系统 CLKID-omega 并不等价。
Brotherston 在 2005 年证明循环证明系统 CLKID-omega 的可证性包含经典一阶归纳定义系统 LKID 的可证性，并猜想二者等价；该问题自 2011 年以来一直未决。本文否定该猜想：在一阶语言中引入常数 0、后继、自然数谓词以及用于表达 2-Hydra 的二元谓词，构造 2-Hydra 语句，并证明该语句在 CLKID-omega 中可证，但在 LKID 中不可证。关键方法是构造一个使 2-Hydra 为假的 Henkin 模型，从而给出 LKID 不可证性。该结果确立了循环证明与经典归纳定义在证明能力上的严格分离。
A cyclic proof system, called CLKID-omega, gives us another way of representing inductive definitions and efficient proof search. The 2005 paper by Brotherston showed that the provability of CLKID-omega includes the provability of LKID, first order classical logic with inductive definitions in Martin-L\"of's style, and conjectured the equivalence. The equivalence has been left an open question since 2011. This paper shows that CLKID-omega and LKID are indeed not equivalent. This paper considers a statement called 2-Hydra in these two systems with the first-order language formed by 0, the successor, the natural number predicate, and a binary predicate symbol used to express 2-Hydra. This paper shows that the 2-Hydra statement is provable in CLKID-omega, but the statement is not provable in LKID, by constructing some Henkin model where the statement is false.
@article{paperbot775,
title = {Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs},
author = {Stefano Berardi and Makoto Tatsuta},
journal = {Logical Methods in Computer Science},
volume = {Volume 15, Issue 3},
year = {2019},
doi = {10.23638/lmcs-15(3:10)2019}
}