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

2025/12/17 by Oda, Yukihiro
Computer Science · #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Formal Methods in Verification

paper · doi:10.48550/arxiv.2512.15075

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.

Related

• Cut elimination for Cyclic Proofs: A Case Study in Temporal Logic
• A study for recovering the cut-elimination property in cyclic proof systems by restricting the arity of inductive predicates
• A Non-wellfounded, Labelled Proof System for Propositional Dynamic Logic
• Cut elimination for propositional cyclic proof systems with fixed-point operators
• Cyclic Proofs, Hypersequents, and Transitive Closure Logic