Definition and Syntax
The guarded fragment (GF) is a fragment of first-order logic over relational signatures, here with equality and without constant or function symbols. It contains atomic formulas, is closed under Boolean connectives, and permits guarded quantification:
\exists\bar y\,(\alpha\land\varphi), \qquad \forall\bar y\,(\alpha\to\varphi).
The guard \alpha is atomic and contains all free variables of \varphi as well as all quantified variables \bar y.
Semantics and Example
GF uses ordinary first-order semantics. A guard restricts quantification to tuples that occur together in an atomic relation.
\forall x\,(P(x)\to\exists y\,(R(x,y)\land Q(y)))
Every element satisfying P has an R-successor satisfying Q.
Properties and Complexity
GF has the finite model property. Satisfiability and finite satisfiability are 2EXPTIME-complete. When relation arities are bounded by a fixed constant of at least two, they are EXPTIME-complete [1]. The signature may vary within this arity bound.
The standard translation of basic modal logic K belongs to GF. Unlike FO², GF does not impose a fixed bound on the number of variable symbols.
References
- Erich Grädel (1999). On the Restraining Power of Guards. Journal of Symbolic Logic 64(4), 1719–1742. DOI.