Room 206
25 juin 2018 - 10h00
Martin-Lof's Inductive Definitions Are Not Equivalent to Cyclic Proofs
par Stefano Berardi de University of Torino
Abstract: Cyclic proofs (Brotherston, Simpson) are an alternative formalization of induction on data bases, suitable for proof search and for Separation Logic, it is interesting to know what tehy are able to prove. Brotherston-Simpson Conjecture (2011) says that cyclic proofs are equivalent to LKID, Martin-Lof's Theory of (finitary) Inductive Definitions. Brotherston-Simpson Conjecture is false (Fossacs 2017): the 2-Hydra statement has a cyclic proof but no proof in LKID. This result was later completed (Fossacs 2017 and LICS 2017, Simpson, Makoto and Berardi) as follows: cyclic proofs are more than Martin-Lof's inductive definitions, but the two become the same, provided we add on both sides the axioms of arithmetic.
