A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics
Logic in Computer Science
2026-03-03 v2 Logic
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.
Keywords
Cite
@article{arxiv.2512.15075,
title = {A study of cut-elimination for a non-labelled cyclic proof system for propositional dynamic logics},
author = {Yukihiro Oda},
journal= {arXiv preprint arXiv:2512.15075},
year = {2026}
}