The Guarded Fragment (GF) of first-order logic is known to have many attractive computational and model theoretic properties. However, it fails to have interpolation. By moving to an extension of GF called the Guarded Negation Fragment (GNF), we gain interpolation while retaining many of the nice properties of GF.
In this talk, I will describe an interpolation procedure for GNF of optimal doubly exponential complexity. The interpolation result is strong enough to derive some effective preservation theorems for GNF and GF. I will also mention some preliminary work considering interpolation for the fixpoint extensions of these guarded logics.
Joint work with Michael Benedikt and Balder ten Cate.