Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs
Abstract
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.
Keywords
Cite
@article{arxiv.1712.09603,
title = {Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs},
author = {Stefano Berardi and Makoto Tatsuta},
journal= {arXiv preprint arXiv:1712.09603},
year = {2023}
}