Equivalence of Intuitionistic Inductive Definitions and Intuitionistic Cyclic Proofs under Arithmetic

TL;DR

This paper proves that under Heyting arithmetic, intuitionistic cyclic proofs and inductive definitions are equivalent in provability, extending prior classical results and clarifying the scope of their equivalence.

Contribution

It establishes the equivalence of intuitionistic cyclic proofs and inductive definitions under arithmetic, and proves related induction theorems within Heyting arithmetic.

Findings

Equivalence holds under Heyting arithmetic for intuitionistic logic.

HA proves Podelski-Rybalchenko and Kleene-Brouwer theorems for induction.

Countermodels show the conjecture is false in general without arithmetic.

Abstract

A cyclic proof system gives us another way of representing inductive definitions and efficient proof search. In 2011 Brotherston and Simpson conjectured the equivalence between the provability of the classical cyclic proof system and that of the classical system of Martin-Lof's inductive definitions. This paper studies the conjecture for intuitionistic logic. This paper first points out that the countermodel of FOSSACS 2017 paper by the same authors shows the conjecture for intuitionistic logic is false in general. Then this paper shows the conjecture for intuitionistic logic is true under arithmetic, namely, the provability of the intuitionistic cyclic proof system is the same as that of the intuitionistic system of Martin-Lof's inductive definitions when both systems contain Heyting arithmetic HA. For this purpose, this paper also shows that HA proves Podelski-Rybalchenko theorem for induction and Kleene-Brouwer theorem for induction. These results immediately give another proof to the conjecture under arithmetic for classical logic shown in LICS 2017 paper by the same authors.