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

TL;DR

The paper develops a non-labelled cyclic proof system for TPDL (TPDL with backwards modalities) and its corresponding sequent calculus, proving soundness and completeness for both. It demonstrates that cut-elimination fails in CGTPDL and GTPDL, while a fragment CGPDL (a backward-operator-free PDL) does admit cut-elimination via cut-free completeness proven through finite, game-based proof-search methods. The authors introduce Fischer–Ladner closures and canonical counter-models to establish completeness and the finite model property, and they connect the TPDL framework to Hoare-style reasoning and related logics. The work thus advances cyclic proof theory in dynamic logics and provides a precise boundary for cut-elimination within this setting, with implications for verification and reasoning about programs that involve backward transitions.

Abstract

Dynamic logic is a 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.

Figures (14)

• Figure 1: Rules of $\mathtt{GTPDL}$
• Figure 2: A $\mathtt{GTPDL}$ proof of ${}\Rightarrow{p\to\mleft[ \alpha \mright]^{-1}\mleft\langle \alpha \mright\rangle p}$
• Figure 4: proof of \ref{['prop:inner-cut-sequent']}
• Figure 5: A proof of $\mleft[ \pi_{0};\pi_{1} \mright]^{-1}\varphi \Rightarrow \mleft[ \pi_{1} \mright]^{-1}\mleft[ \pi_{0} \mright]^{-1}\mleft\langle \pi_{0};\pi_{1} \mright\rangle\mleft[ \pi_{0};\pi_{1} \mright]^{-1}\varphi$
• Figure 7: A proof of $\mleft[ \pi_{0}\cup \pi_{1} \mright]^{-1}\varphi \Rightarrow \mleft[ \pi_{i} \mright]^{-1}\mleft\langle \pi_{0}\cup \pi_{1} \mright\rangle\mleft[ \pi_{0}\cup \pi_{1} \mright]^{-1}\varphi$ with $i=0, 1$

Theorems & Definitions (135)

• Definition 2.1: Length of well-formed expression
• Definition 2.2: Model for $\mathtt{TPDL}$
• Definition 3.1: $\mathtt{GTPDL}$ proof
• Theorem 3.2: Soundness of $\mathtt{GTPDL}$
• proof
• Theorem 3.3: Completeness of $\mathtt{GTPDL}$
• Theorem 3.4: Finite model property
• Proposition 4.1
• proof
• Proposition 4.2