Title: Craig Interpolation for PDL, finally and formally

Speaker: Malvin Gattinger (University of Amsterdam)

Time: Sep. 29th (Tuesday) 15:10 - 18:00

Location: Teaching Building No.2 (二教) 411

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 was an open question for many years, with a somewhat chaotic situation in the literature: three proof attempts existed, all were criticised and one officially revoked.

We recently published a tableau-based proof that PDL does indeed have Craig Interpolation [1], based on ideas from Borzechowski (1988). In parallel we also formalized this proof in Lean, and since 2 September 2026 that Lean proof is sorry-free [2].

In this talk I will discuss the history of the problem, the main proof ideas, the formalization, and lastly a new result about test-free PDL.

This continues my talk at PKU on 6 December 2016, but I will not assume that the audience remembers everything from then.

Main 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. Accepted / to appear in LMCS.

https://arxiv.org/abs/2503.13276

[2] Malvin Gattinger, Amos Nicodemus, Djanira dos Santos Gomes, Noam Cohen, Madeleine Gignoux, Wietse Bosman, Dionysis Yusofy, Haitian Wang, Eshel Yaron, Xiaoshuang Yang, Jeremy Sorkin: Tableaux for Propositional Dynamic Logic in Lean 4.

https://github.com/m4lvin/lean4-pdl