Classical System of Martin Lof's Inductive Definitions Is Not Equivalent to Cyclic Proof System
A cyclic proof system, called \mathtt{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 \mathtt{CLKID}\omega includes the provability of Martin Lof's system of inductive definitions, called \mathtt{LKID} and conjectured the equivalence. Since then, the equivalence has been left an open question. This paper shows that \mathtt{CLKID}\omega and \mathtt{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 \mathtt{CLKID}\omega but the statement is not provable in \mathtt{LKID} by constructing some Henkin model where the statement is false.
FoSSaCS