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

TL;DR

This paper introduces a cyclic proof system for an extension of propositional dynamic logic with backwards modal operators, analyzing its properties and limitations regarding cut-elimination.

Contribution

It presents a new sequent calculus and cyclic proof system for extended propositional dynamic logic, with proofs of soundness, completeness, and cut-elimination restrictions.

Findings

Soundness and completeness established for the systems

Cut-elimination fails in the general cyclic proof system

Cut-elimination holds under certain restrictions

Abstract

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.