Towards Formalizing Cyclic Tableaux and Interpolation for PDL in Lean

ABSTRACT

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, all were criticised and one 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 I will discuss part of the main proof idea, the challenges of the formalization project, how we solved some of them already and what remains to be done. I 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 also was upstreamed 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