Cut-Elimination for Cyclic Proof Systems with Inductively Defined Propositions (Theory and Applications of Proof and Computation)

Abstract

Cyclic proof systems are extensions of the sequent-calculus style proof systems for logics with inductively defined predicates. In cyclic proof systems, inductive reasoning is realized as cyclic structures in proof trees. It has been already known that the cut-elimination property does not hold for the cyclic proof systems of some logics such as the first-order predicate logic and the separation logic. In this paper, we consider the cyclic proof systems with inductively defined propositions (that is, nullary predicates), and prove that the cut-elimination holds for the propositional logic, and it does not hold for the bunched logic.