Introducing myself: Malvin Gattinger / Modal Logic Tableaux

Stream: new members

[Malvin Gattinger]

Hi everyone :wave:
As a late introduction (and shameless advertisement, I hope this is allowed...) I would like to share my project: A proof that Basic Modal Logic has Craig Interpolation: https://github.com/m4lvin/tablean
The proof uses a tableau system and is relatively easy, though it took me quite some time to formalise while learning Lean as I went along. Big thanks go out to the many people here on zulip who helped me!
My motivation and long term goal is an open question, or a rather messy situation in the literature: Does Propositional Dynamic Logic (PDL, a much more complicated modal logic than Basic Modal Logic) have Craig Interpolation?
At least three proof( attempt)s for this have been (more or less) published, but none seems to be generally accepted. One of them (Borzechowski 1988) I translated from German to English, but am still really unsure whether it works. So a formalisation would be a great way to settle the confusion.
My next goal for now is to simplify and improve the proof/code (any suggestions are welcome!) before making it more complicated again by moving to more expressive modal logics. For now I am happy that I managed to finish this small first milestone.
Thanks again for making Lean, mathlib, the nice documentation, and for all the help!

[Malvin Gattinger]

I will give a short presentation about this at Advances in Modal Logic in a month, here is the five page paper that was accepted: https://malv.in/2022/AiML2022-basic-modal-interpolation-lean.pdf