Speaker: Guillermo Menéndez Turata
Date and Time: Thursday, June 3rd 2021, 16:30-18:00, Amsterdam time.
Venue: online.
Title: Uniform interpolation from cyclic proofs: the case of modal mu-calculus.
Abstract. Uniform interpolation was first established for the modal mu-calculus by D’Agostino and Hollenberg via a combination of semantic and syntactic methods. A natural question is whether a purely syntactical proof of this result, in the style of Pitt’s seminal work on uniform interpolation for intuitionistic logic, can be produced. One possible reason Pitt’s method has not been applied to the modal mu-calculus is that it requires a setting where uniform interpolation can be proved by induction on cut-free derivations in a finitary system. While it is feasible to design cut-free calculi for fixpoint modal logics, they are often infinitary, i.e., derivations may have infinite branches. In this talk we apply Pitt’s technique to the modal mu-calculus and show how to construct uniform interpolants from cyclic derivations in an annotated goal-oriented proof system introduced by Jungteerapanich and Stirling.