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.

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.