A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics

Dynamic logic is a modal logic for reasoning about programs. A cyclic proof system is a proof system that allows proofs containing cycles and is an alternative to a proof system containing (co-)induction. This paper introduces a sequent calculus and a non-labelled cyclic proof system for an extension of propositional dynamic logic obtained by adding backwards modal operators. We prove the soundness and completeness of these systems and show that cut-elimination fails in both. Moreover, we show the cut-elimination property of the cyclic proof system for propositional dynamic logic obtained by restricting ours.