Speaker
Valentina Trucco Dalmas
Bernoulliborg, Nijenborgh 9, 9747 AG Groningen, University of Groningen, The Netherlands
Talks at this conference:
Thursday, 18:10, J222 
Investigating uniform interpolation via global termination 
A logic \(L\) has the Uniform Interpolation Property (UIP) if for every formula \(\phi\), and every propositional variable \(p\), there exists a formula \(E p. \phi\) built from variables in \(\phi\) different from \(p\), that satisfies \(\phi \to E p. \phi \in L\) and that whenever \(\phi \to \psi \in L\), we have \(E p. \phi \to \psi \in L\) for all \(\psi\) not containing \(p\). UIP can be interpreted as saying that the propositional quantifier \(\exists p\) is definable. In addition, UIP is a stronger version of the relatively betterunderstood Craig Interpolation Property. Interpolation properties are highly correlated with the expressive power of a logic and have been studied for many logics, including many nonclassical logics. In 1992, Andrew Pitts [1] established that Intuitionistic Propositional Logic has the UIP using a prooftheoretic approach. Pitts’ method crucially relies on a locally terminating proof calculus, i.e., a calculus where every rule’s premise is smaller than the conclusion w.r.t. some measure. While Pitts’ argument has been adapted to many nonclassical logics, all of these arguments use a locally terminating proof calculus or rely on the ability of the logic to express fixpoints, such as in the case of the modal \(\mu\)calculus. In this investigation, we aim to isolate the global termination conditions under which a modified Pitts’ method would remain applicable, to widen the scope of the prooftheoretic argument to nonclassical —and in particular, substructural— logics. This is joint work with Helle Hvid Hansen (Groningen) and Revantha Ramanayake (Groningen). Bibliography
