Title: 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 effcient proof search. The 2011 paper by
Brotherston and Simpson showed that the provability of CLKID-omega includes the
provability of Martin-Lof's system of inductive definitions, called LKID, and
conjectured the equivalence. Since then, the equivalence has been left an open
question. 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.