Investigating uniform interpolation via global termination
Valentina Trucco Dalmas
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 better-understood Craig Interpolation Property. Interpolation properties are highly correlated with the expressive power of a logic and have been studied for many logics, including many non-classical logics.
In 1992, Andrew Pitts [1] established that Intuitionistic Propositional Logic has the UIP using a proof-theoretic 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 non-classical 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 proof-theoretic argument to non-classical —and in particular, substructural— logics.
This is joint work with Helle Hvid Hansen (Groningen) and Revantha Ramanayake (Groningen).
Bibliography
- Andrew M. Pitts,On an Interpretation of Second Order Quantification in First Order Intuitionistic Propositional LogicJournal of Symbolic Logic,vol. 57 (1992), no. 1, pp. 33–52.