Propositional Dynamic Logic in Lean 4

Project Goal

The aim is to prove that Propositional Dynamic Logic (PDL) has the Craig Interpolation property. The main reference is the following.

• 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 2025, https://arxiv.org/abs/2503.13276

The article contains direct links to the corresponding parts of the formalization here. A checkmark in the article means that the Lean statement is sorry-free, including all its dependencies. There is no separate blueprint.

Useful Links

• Documentation: https://m4lvin.github.io/lean4-pdl/docs/ (generated by doc-gen4)

• Tableaux prover: https://w4eg.de/malvin/illc/tapdleau (implemented here in Haskell, useful to run examples)

• Open this repository in Gitpod or GitHub Codespaces

Module dependency overview

(Run make dependencies.svg to update this.)

Other References

• https://github.com/m4lvin/tablean - previous project for Basic Modal Logic, in Lean 3. Code from there has been ported to Lean 4 and is included here in the Bml folder.
• https://malv.in/2020/borzechowski-pdl - the German original proof by Borzechowski (1988) and the English translation (2020)