Living without Beth and Craig: Explicit Definitions and Interpolants in the Guarded Fragment

The guarded fragment of FO fails to have the Craig Interpolation Property (CIP) and the Projective Beth Definability Property (PBDP). Thus, not every valid implication between guarded formulas has a guarded interpolant, and not every implicitly definable relation has an explicit guarded definition. In this article, we show that nevertheless the existence of guarded interpolants and explicit definitions is decidable. Moreover, it is 3ExpTime-complete in general, and 2ExpTime-complete if the arity of relation symbols is bounded by a constant. Deciding the existence of guarded interpolants and explicit definitions is thus by one exponential harder than validity in the guarded fragment.