Brotherston's Conjecture: Equivalence of Inductive Definitions and Cyclic Proofs

Makoto Tatsuta

An inductive definition is a way to define a predicate by an expression which may contain the predicate itself. The predicate is interpreted by the least fixed point of the defining equation. Inductive definitions are important in computer science, since they can define useful recursive data structures such as lists and trees. Inductive definitions are important also in mathematical logic, since they increase the proof theoretic strength. Martin-Lof’s system of inductive definitions given in 1971 is one of the most popular system of inductive definitions.

In 2006 Brotherston proposed an alternative formalization of inductive definitions, called a cyclic proof system. In general, for proof search, a cyclic proof system can find an induction formula in a more efficient way than Martin-Lof’s system, since a cyclic proof system does not have to choose fixed induction formulas in advance.

The equivalence of the provability of Martin-Lof’s system for inductive definitions and that of the cyclic proof system was conjectured in 2006. The speaker and Berardi solved it in 2017. This talk will explain this problem from basic background knowledge to the latest results.

---

Previous: Chiel Bruin | Frame VM: a virtual machine using scopes as frames
Next: Jurriaan Hage | Security Type Error Diagnosis for Functional Languages