Propositional Dynamic Logic has Craig Interpolation, in Lean 4

Project Goal

We 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, Francisco Trucco Dalmas, Yde Venema: Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof. Preprint 2026, https://arxiv.org/abs/2503.13276v2

The article contains direct links to the corresponding parts of the formalization here. There is no separate blueprint.

Useful Links

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

• Open this repository in GitHub Codespaces

Overview

(This shows the status of the main branch at the last successful CI run.)

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).

• https://tools.malv.in/tapdleau - tableaux prover implemented in Haskell, useful to run examples.

• This project has been edited by Aristotle (Harmonic).