Berardi, Stefano and Tatsuta, Makoto - Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs

lmcs:4173 - Logical Methods in Computer Science, August 1, 2019, Volume 15, Issue 3
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs

Authors: Berardi, Stefano and Tatsuta, Makoto

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öf'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.


Source : oai:arXiv.org:1712.09603
Volume: Volume 15, Issue 3
Published on: August 1, 2019
Submitted on: December 29, 2017
Keywords: Computer Science - Logic in Computer Science


Share