Proof theoretic methodology for propositional dynamic logic

Abstract

We relate by syntactic techniques finitary and infinitary axiomatizations for the iterator-construct * of Propositional Dynamic Logic PDL. This is applied to derive the Interpolation Theorem for PDL, and to provide a new proof of the semantic completeness of Segerberg's axiomatic system for PDL.

Contrary to semantic techniques used to date, our proof of completeness is relatively insensitive to changes in the language and axioms used, provided some minimum syntactic closure properties hold. For instance, the presence of the test-operator adds no difficulty, and the proof also establishes the Interpolation Theorem and the closure under iteration of a constructive variant of PDL.