Guarded Fragment

Origin. Andréka, van Benthem, Németi (1998). Decidable fragment of first-order logic. Variables must be "guarded" by atoms. Generalizes modal logic to first-order. Foundation for description logic decidability.

Models. Quantifiers restricted: ∀ȳ(G(x̄,ȳ) → φ). Guard G must contain all free variables. Modal logic embeds into GF. Tree-model property.

Formalism.

Guarded quantification: ∀ȳ(G(x̄,ȳ) → φ(x̄,ȳ)) ∃ȳ(G(x̄,ȳ) ∧ φ(x̄,ȳ)) G: guard atom containing all free variables of φ.

Guard condition: All free variables of φ must occur in guard G. G is an atomic formula (including equality).

Examples: ∀y(R(x,y) → P(y)) — guarded by R(x,y). ∀y(P(y) → Q(y)) — guarded by P(y): free(Q(y)) = {y} ⊆ vars(P(y)). ∀x∀y∀z(R(x,y) ∧ R(y,z) → R(x,z)) — NOT guarded. No single atom covers x, y and z; transitivity is loosely guarded, not guarded.

Modal translation: □φ becomes ∀y(Rxy → φ(y)) ◇φ becomes ∃y(Rxy ∧ φ(y)) GF generalizes modal logic.

Loosely guarded: Guard can be conjunction of atoms. ∀ȳ(G₁ ∧ G₂ → φ) where G₁ ∧ G₂ covers variables.

Clique guarded: Guards form cliques in Gaifman graph.

Tree model property: Satisfiable GF formulas have tree-like models. Key to decidability.

Symbols.

Symbol	Unicode	Name	Meaning
G	—	Guard	The atomic formula licensing a quantification
∀	U+2200	Universal quantifier	Occurs only in the pattern ∀ȳ(G → φ)
∃	U+2203	Existential quantifier	Occurs only in the pattern ∃ȳ(G ∧ φ)
→	U+2192	Rightwards arrow / Conditional	Joins guard to matrix in the universal pattern
∧	U+2227	Conjunction	Joins guard to matrix in the existential pattern; also compounds loose guards
x̄, ȳ	—	Variable tuples	Free and bound blocks of variables
=	U+003D	Identity	Equality atoms are admissible guards
□	U+25A1	Box / Necessity	Modal operator; translates to a guarded ∀
◇	U+25C7	Diamond / Possibility	Modal operator; translates to a guarded ∃
GF	—	Guarded fragment	The fragment as a whole
φ, ψ	—	Schematic formulas	Matrices of guarded quantifications

Metatheory. Decidability rests on a generalized tree model property: every satisfiable guarded sentence has a model of tree width bounded by the sentence's width, so satisfiability reduces to an emptiness test for alternating automata on trees. Grädel (1999) obtained 2EXPTIME-completeness from this, dropping to EXPTIME-complete when the signature has bounded arity, and proved the finite model property, so finite satisfiability and satisfiability coincide; Hodkinson (2002) settled the same question for the loosely guarded fragment. GF is invariant under guarded bisimulation, and the converse holds — every first-order formula so invariant is equivalent to a guarded one, the guarded analogue of van Benthem's characterization theorem, established by Andréka, van Benthem, and Németi (1998) and extended to finite structures by Otto (2012). That is what makes GF the fragment rather than one decidable fragment among many: it is not a syntactic restriction that happens to work but the exact first-order counterpart of a semantic invariance. GF and the two-variable fragment are incomparable, neither containing the other.

Applies to. Description logics. Modal logic generalization. Database queries. Ontology reasoning. Decidable fragments.

Limitations. Transitivity is the standing obstacle. It is not guarded — no single atom covers the three variables — and it cannot simply be imposed on the models either: the guarded fragment with transitive relations is undecidable, so orders, temporal structures and transitive ontology roles all fall outside. The repairs are partial. Szwast and Tendera (2001) recovered decidability by requiring transitive relations to appear only as guards, never in the matrix, and Grädel and Walukiewicz (1999) showed the extension μGF with least and greatest fixed points remains decidable, which supplies reachability while leaving first-order logic. Craig interpolation fails (Hoogland and Marx 2002), so the modal analogy that motivates the fragment breaks at exactly the point where one would expect it to hold; the Beth definability property nonetheless survives (Hoogland, Marx, and Otto 1999), so the two come apart here as they do not in first-order logic, and the repair for interpolation is to change fragment rather than patch this one — the guarded negation fragment of Bárány, ten Cate, and Segoufin (2011) is strictly larger, still 2EXPTIME-complete, and does interpolate. Guarded bisimulation invariance, which characterizes the fragment, also bounds it: nothing the guarded fragment says can distinguish a structure from its guarded unravelling. The unravelling preserves every atom within a guarded tuple, so what lies inside a single guard survives it — ∃x∃y∃z (R(x,y,z) ∧ E(x,y) ∧ E(y,z) ∧ E(z,x)) is guarded and detects a triangle. What is lost is the global view: the unravelling has tree width bounded by the largest guard rather than being acyclic, so connectivity, reachability, acyclicity of E as a relation, and counting across a structure are all inexpressible. The cost is driven by arity — satisfiability is 2EXPTIME-complete in general and EXPTIME-complete once relation arity is bounded (Grädel 1999) — so there is no tractable case to retreat to, and the second exponential comes from unbounded guards rather than from guarding as such.