Malvin Gattinger
(ILLC)
PDL probably has Craig Interpolation since 1981. Or: If Rumsfeld would have been a logician.
March 28th at 18:00, in ILLC Seminar room
If A implies B, then there is a C which only uses the common vocabulary of A and B such that A implies C and C implies B. This property called Craig Interpolation has been shown for many logics, including first-order logic, basic and multi modal logic and the mu-calculus. For Propositional Dynamic Logic (PDL) the question is still open, according to textbooks and current papers. But at least three proofs have been written, two of them published and only one officially revoked. To put it bluntly: The situation is a mess. In this talk we first introduce PDL, make the supposedly open question precise and tell some (hi)stories. We then discuss the proof by Daniel Leivant from 1981 which seems to have been put aside after it was criticized by Marcus Kracht. After defending the proof against this criticism we argue that a revised version of the proof should work. The talk will be accessible for everyone who is not afraid of Kripke frames, typewriters, proof theory and stars.