# Interpolation for Converse PDL

## TL;DR

This paper proves that Converse PDL, an extension of propositional dynamic logic with converse programs, has the Craig Interpolation Property and Beth Definability, using a new cyclic sequent calculus.

## Contribution

It introduces a sound and complete cyclic sequent system for Converse PDL and establishes its interpolation and definability properties.

## Key findings

- Converse PDL enjoys the Craig Interpolation Property.
- The logic satisfies the Beth Definability Property.
- A new cyclic sequent calculus for Converse PDL is developed.

## Abstract

Converse PDL is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse PDL enjoys the (local) Craig Interpolation Property, with respect to both atomic programs and propositional variables. As a corollary we establish the Beth Definability Property for the logic. Our interpolation proof is based on an adaptation of Maehara's proof-theoretic method. For this purpose we introduce a sound and complete cyclic sequent system for this logic. This calculus features an analytic cut rule and uses a focus mechanism for recognising successful cycles.

---
Source: https://tomesphere.com/paper/2508.21485