Craig Interpolation for Decidable First-Order Fragments

We show that the guarded-negation fragment (GNFO) is, in a precise sense, the smallest extension of the guarded fragment (GFO) with Craig interpolation. In contrast, we show that the smallest extension of the two-variable fragment ( \(\textrm{FO}^2 \) ), and of the forward fragment (FF) with Craig interpolation, is full first-order logic. Similarly, we also show that all extensions of \(\textrm{FO}^2 \) and of the fluted fragment (FL) with Craig interpolation are undecidable.