Equivalence of Inductive Definitions and Cyclic Proofs under Arithmetic
National Insitute of Informatics
COM2 Level 4
Executive Classroom, COM2-04-02
Abstract:
A cyclic proof system, called 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 CLKID-omega includes the provability of the classical system of Martin-Lof's inductive definitions, called LKID, and conjectured the equivalence. By this year the equivalence has been left an open question. In general, the conjecture was proved to be false in FoSSaCS 2017 paper by Berardi and Tatsuta. However, if we restrict both systems to only the natural number inductive predicate and add Peano arithmetic to both systems, the conjecture is proved to be true in FoSSaCS 2017 paper by Simpson. This talk shows that if we add arithmetic to both systems, they become equivalent, namely, the conjecture holds. The result of this talk includes that of the paper by Simpson as a special case. In order to construct a proof of LKID for a given cyclic proof, this talk shows every bud in the cyclic proof is provable in LKID, by cutting the cyclic proof into subproofs such that in each subproof the conclusion is a companion and the assumptions are buds. The global trace condition gives some induction principle, by using an extension of Podelski-Rybalchenko termination theorem from well-foundedness to induction schema. In order to show this extension, this talk also shows that infinite Ramsey theorem is formalizable in Peano arithmetic.
Biodata:
Bachelors in Law in 1983 and Science in 1985, Master's in Science in 1987, and PhD in 1993 all in University of Tokyo. An assistant professor and an associate professor at Tohoku University from 1989 to 1996. An associate professor at Kyoto University from 1996 to 2001. A professor at National Institute of Informatics since 2001. Interested in theoretical computer science and mathematical logic, in particular, separation logic, software verification, type theory, and constructive logic.