Technical Summary: Propositional Dynamic Logic Has Craig Interpolation

1. The Problem

The paper addresses the long-standing open question of whether Propositional Dynamic Logic (PDL) possesses the Craig Interpolation Property (CIP). CIP states that for any valid implication $\phi \to \psi$, there exists an interpolant $\theta$ such that $\phi \to \theta$ and $\theta \to \psi$ are valid, and $\theta$ contains only propositional letters and atomic programs common to both $\phi$ and $\psi$.

Despite PDL being a well-studied modal logic with established decidability and completeness results, its interpolation status has remained unclear for decades. The literature contains three previous attempts to prove interpolation:

1. Leivant (1981): Claimed a proof, later refuted by Kracht (1999) for incorrect reasons, though a genuine gap in Leivant's proof remains.
2. Borzechowski (1988): A master's thesis (Diplomarbeit) claiming a proof, which received little attention and was dismissed by some as unverifiable.
3. Kowalski (2002): Claimed a proof, which was refuted and officially withdrawn in 2004.

The difficulty arises because PDL is a modal fixpoint logic (due to the iteration operator $*$). While interpolation has been established for the full modal $\mu$-calculus and its alternation-free fragment using cyclic proof systems, the specific constraints of PDL make it challenging to ensure that the solutions to the fixpoint equations characterizing interpolants can be expressed within PDL itself, rather than requiring the full expressive power of the $\mu$-calculus.

2. Methodology

The authors provide a constructive proof based on a cyclic tableau system and an adaptation of Maehara's proof-theoretic method.

2.1. A Cyclic Tableau System for PDL

The authors define a new tableau system for PDL that operates on split sequents (pairs of formula sets). Key features include:

• Local vs. Modal Reasoning: The system distinguishes between local rules (propositional reasoning and unfolding of programs within a single state) and modal rules (moving between states in a Kripke model).
• Unfolding Mechanism: Instead of standard reduction rules for each program constructor, the system uses a "loading" mechanism. Formulas of the form $[\alpha]\psi$ (where $\alpha$ is non-atomic) are unfolded into a finite set of sequents based on "test profiles." This set, denoted $\text{unfold}_\square(\alpha, \psi)$, represents the disjunction of all possible execution paths of $\alpha$ where specific tests succeed or fail.
• Handling Iteration: To prevent infinite local unfolding of formulas like $[\alpha^*]\psi$, the system eliminates regenerated occurrences of the formula during the unfolding process. This relies on the observation that $[\alpha^*]\psi$ is a greatest fixpoint.
• Cyclic Proofs: The system allows for "repeats" (nodes with identical labels to an ancestor).
  • Loaded-path repeats: A repeat where the path from the ancestor (companion) to the current node consists entirely of loaded nodes. These are treated as "successful" leaves (indicating a loop that satisfies the formula).
  • Free repeats: A repeat where the path contains unloaded nodes. These are treated as "unsuccessful" leaves, indicating a potential counter-model.
• Termination: The system ensures finiteness by enforcing that all free repeats and loaded-path repeats are leaves, and by utilizing the Fischer-Ladner closure to bound the set of formulas.

2.2. Interpolation via Quasi-Tableaux and Fixpoint Equations

To construct the interpolant, the authors adapt Maehara's method to the cyclic setting:

• Clusters: The tableau is viewed as a graph with back edges from repeats to companions. The strongly connected components (SCCs) of this graph are called "clusters."
• Quasi-Tableaux: For a proper cluster (a non-singleton SCC), the authors define a "quasi-tableau." This structure is used to set up a system of equations characterizing the interpolant.
• Pre-interpolants: The method defines "pre-interpolants" for nodes in the quasi-tableau via a leaf-to-root induction.
  • At exit nodes (leaves not part of the cluster), the pre-interpolant is the interpolant of the exit node (assumed to exist by induction).
  • At repeat leaves, the pre-interpolant is an internal propositional variable $q_x$.
  • At companion nodes, the pre-interpolant is defined as the solution to a fixpoint equation. Specifically, if a companion $x$ has a child $y$ with pre-interpolant $\iota_y \equiv \bigwedge_i [\alpha_i]q_x \wedge \bigwedge_j [\beta_j]q_{z_j} \wedge \psi$, the pre-interpolant for $x$ is defined as $\iota_x := [(\bigcup_i \alpha_i)^*](\bigwedge_j [\beta_j]q_{z_j} \wedge \psi)$.
• Solving in PDL: The crucial insight is that this specific construction ensures the solutions to the fixpoint equations remain within the language of PDL. The use of the iteration operator $*$ in the definition of $\iota_x$ effectively solves the equation $\iota_x \equiv \iota_y\langle q_x \mapsto \iota_x \rangle$ within PDL.
• Final Interpolant: The interpolant for the root of the cluster is obtained by substituting the internal variables in the root's pre-interpolant with the corresponding region formulas (disjunctions of left-hand sides of the split sequents).

3. Key Contributions and Results

• Proof of CIP for PDL: The paper establishes that PDL has the Craig Interpolation Property.
• Beth Definability: As a corollary, the paper proves that PDL has the Beth Definability Property (since CIP implies Beth definability in the presence of a deduction theorem).
• Constructive Algorithm: The proof is constructive. The authors provide a clear algorithm for computing interpolants from a closed tableau.
• Formal Verification: The authors have partially formalized the proof in the interactive theorem prover Lean 4. As of the paper's writing, the Soundness and Completeness theorems, along with several supporting lemmas, have been verified.
• Implementation: A Haskell implementation of the tableau system and interpolant construction is provided, available via a web interface.

4. Significance and Claims

The paper claims to resolve a puzzle in the literature regarding PDL's interpolation status, providing the first verified proof that overcomes the gaps in previous attempts.

• Resolution of Historical Issues: The authors explicitly address the history of failed attempts, noting that their approach builds on the core ideas of Borzechowski (1988) but rigorously formalizes the handling of cyclic proofs and the construction of interpolants within the language of PDL.
• Methodological Novelty: The paper highlights that while Maehara's method is standard for non-cyclic proofs, applying it to cyclic proofs (fixpoint logics) requires solving fixpoint equations. The authors demonstrate that for PDL, these solutions can be expressed using the logic's own iteration operator, a non-trivial result that distinguishes PDL from other fragments where such solutions might require the full $\mu$-calculus.
• Open Questions: The authors modestly note that their method relies on the presence of test programs ($\tau?$). Consequently, it remains an open question whether the test-free fragment of PDL has interpolation, as their construction generally yields interpolants containing tests even when the input is test-free. They also leave open the extension of their method to other PDL variants (e.g., with converse or intersection) and the implications for Kleene Algebra with Tests (KAT).

In summary, the paper provides a definitive, constructive proof of Craig Interpolation for PDL using a novel cyclic tableau system and a specialized fixpoint-solving technique for interpolants, supported by both a Haskell implementation and partial formal verification in Lean.