Propositional Dynamic Logic (PDL) is a well-known modal logic where modalities are programs using sequencing, choice, iteration and tests. PDL can embed many other modal logics, it can capture common programming constructs such as if-then-else and while loops, and it is related to Kleene Algebra with Tests (KAT). A logic has Craig Interpolation if for every validity φ→ψ there is a formula θ such that φ→θ and θ→ψ are also valid, and θ only uses the vocabulary occurring in both φ and ψ. Whether PDL has his property has been an open question for many years, with a somewhat chaotic situation in the literature: three proof attempts exist, which all were criticised and in one case also officially revoked.

A new tableau-based proof, based on the ideas from Borzechowski (1988), was recently made available [1]. In parallel to its development we have started to formalize this proof in the interactive proof assistant Lean [2].

In this talk we will discuss the challenges of the formalization project, how we solved some of them already and what remains to be done. We plan to cover (i) Mutual recursion and induction (because PDL formulas contain programs and vice versa), (ii) the Dershowitz-Manna Ordering to prove tableaux termination that we contributed to mathlib [3], and (iii) the issue of encoding well-formed cyclic proof trees into dependent inductive types.

References:

[1] Manfred Borzechowski, Malvin Gattinger, Helle Hvid Hansen, Revantha Ramanayake, Valentina Trucco Dalmas, Yde Venema: Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof. Preprint submitted to LMCS, March 2025. https://arxiv.org/abs/2503.13276

[2] Malvin Gattinger, Amos Nicodemus, Djanira dos Santos Gomes, Noam Cohen, Wietse Bosman, Madeleine Gignoux, Haitian Wang, Eshel Yaron, Xiaoshuang Yang, Jeremy Sorkin: Tableaux for Propositional Dynamic Logic in Lean 4. Work in progress since October 2023. https://github.com/m4lvin/lean4-pdl

[3] Haitian Wang: Pull request 14411 for mathlib: add Dershowitz-Manna Ordering and Theorem. Merged into mathlib in January 2025. https://github.com/leanprover-community/mathlib4/pull/14411