Interpolation in Guarded Fragments
Eva Hoogland, Maarten Marx

Abstract:
The guarded fragment (GF) was introduced by Andreka, van Benthem and
Nemeti as a fine-structure of first order logic which combines a great
expressive power with nice modal behavior. It consists of relational
first order formulas whose quantifiers are relativized by atoms in a
certain way.  Slightly generalizing the admissible relativizations
yields the packed fragment (PF). In this paper we chart the behavior
of these fragments with regard to interpolation. While GF and PF have
been established as particularly well-behaved fragments of first order
logic in many respects, it will be shown that the interpolation
property of first order logic fails in restriction to GF and
PF. However, each of these fragments turns out to have an alternative
interpolation property that closely resembles the interpolation
property usually studied in modal logic. These results are strong
enough to entail the Beth definability theorem for GF and PF. Even
better, every n-variable guarded or packed fragment with up to n-ary
relations has the Beth property. Finally it will be demonstrated that
any n-variable guarded fragment which contains at most k-ary relations
has interpolation if and only if k<3 or n<3. In particular, the
2-variable guarded fragment has interpolation. The packed fragments
have interpolation if and only if n<3 or k<2.

Keyword(s): Guarded fragment, packed fragment, interpolation property,
Beth definability property.

Note: The part of this paper concerning Beth's definability property
for the guarded fragment has appeared as: E. Hoogland, M. Marx, and
M. Otto. Beth Definability for the Guarded Fragment. In: H. Ganzinger,
D. McAllester, and A. Voronkov editors, Logic for Programming and
Automated Reasoning, 6th International Conference LPAR99, Tbilisi,
Georgia, volume 1705 of LNAI, pages 273--285. Springer, 1999.