The Interpolation Theorem for IL and ILP
Carlos Areces, Dick de Jongh, Eva Hoogland

Abstract:
In this article we establish interpolation for the minimal system of 
interpretability logic IL. We prove that arrow interpolation holds for 
IL and that turnstile interpolation and interpolation for the \Lambda­
modality easily follow from this. Furthermore, these properties are 
extended to the system ILP. The related issue of Beth Definability is 
also addressed. As usual, the arrow interpolation property implies the 
Beth property. From the latter it follows via an argumentation which is 
standard in provability logic, that IL has the fixed point property. 
Finally we observe that a general result of Maksimova [11] for 
provability logics can be extended to interpretability logics, implying 
that all extensions of IL have the Beth property.