Stefano Berardi ; Makoto Tatsuta - 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 - https://doi.org/10.23638/LMCS-15(3:10)2019
Classical System of Martin-Lof's Inductive Definitions is not Equivalent to Cyclic Proofs

Authors: Stefano Berardi ; Makoto Tatsuta

    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.


    Volume: Volume 15, Issue 3
    Published on: August 1, 2019
    Accepted on: August 1, 2019
    Submitted on: December 29, 2017
    Keywords: Computer Science - Logic in Computer Science

    1 Document citing this article

    Share

    Consultation statistics

    This page has been seen 454 times.
    This article's PDF has been downloaded 283 times.