1st Semester 2023/24: Towards PDL Interpolation in Lean 4

Instructors

Malvin Gattinger, Valentina Trucco Dalmas

ECTS

6

Description

It is considered an open question whether Propositional Dynamic Logic (PDL) has Craig Interpolation, even though three proofs have been written so far: by Leivant in 1981, by Borzechowski in 1988 and by Kowalski in 2004. The newest one is officially retracted, the oldest one has problems that so far nobody managed to repair, and the middle one by Borzechowski seems to never have been understood by the community. For more history, see the slides by Malvin from LoLaCo this year, available on Canvas or upon request by email.
In 2020 Malvin translated the proof by Borzechowski (a German diploma thesis at FU Berlin) to English and since 2021 we are slowly understanding it, rewriting it to modern notation, and adding more explanations. In parallel we have started formalizing the proof in the proof assistant Lean 4. For this formalization we are now looking for help.

Organisation

We will work as a team, fully online/remote, with weekly meetings and otherwise mostly asynchronous/chat communication.
You will be given access to the current draft of our rewrite of the Borzechowski proof, and your main task will be to write Lean code. Depending on the status of the project by beginning of January, this will mostly be writing proofs, but it probably will also happen that we have to "go back to the drawing board" and rewrite some definitions and statements of theorems.
We can accommodate at most five students.

Prerequisites

You must have experience with Lean 4. You should also know Modal Logic, including PDL, and Modal Tableaux systems.

Assessment

Grading will be pass/fail as usual, based on whether you made a contribution to the team effort.

References

- Borzechowski (1988) and translation: https://malv.in/2020/borzechowski-pdl (also has text and slides from a short presentation at AiML 2020)

- Current Lean 4 code: https://github.com/m4lvin/lean4-pdl

- Interpolation for Basic Modal Logic in Lean 3: https://github.com/m4lvin/tablean