Taming proof systems towards uniform interpolation

Iris van der Giessen
University of Amsterdam

Uniform interpolants reflect a balanced flow of information within a logical system. Intuitively, given a statement $A$ that involves specific terminology, its uniform inter-polant $A^′$ serves as a simplified reflection of $A$: it employs fewer terms but retains precisely those consequences of $A$ that can be expressed in this reduced terminology. We say that a logic has the uniform interpolation property if for all formulas $A$ there exists a uniform interpolant.

In this talk, I will explain how proof systems can be used to construct uniform interpolants, and explain why it is important to tame your proof system towards the right shape. Through a series of examples, I will illustrate how I have tamed sequent calculi to prove the uniform interpolation property for some modal logics. I would like to highlight ongoing research together with Borja Sierra Miranda and Guillermo Menéndez Turatain which we show that intuitionistic Gödel-Löb logic $\mathsf{iGL}$ enjoys the uniform interpolation property for which a cyclic proof system was necessary.

Download the abstract.

 Overview  Program