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 ∀y(P(y) → Q(y)) — NOT guarded (P doesn't contain x)

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	Atomic guard
∀ȳ	—	Guarded universal	Restricted ∀
∃ȳ	—	Guarded existential	Restricted ∃
→	U+2192	Implies	Guarded implication

Metatheory. Decidable: 2EXPTIME-complete. Finite model property. Tree model property. Craig interpolation fails (Hoogland and Marx 2002), despite the modal analogy — modal logic K has interpolation and GF does not. Preserved under guarded bisimulation; by the guarded Andréka–van Benthem–Németi theorem, GF is exactly the guarded-bisimulation-invariant fragment of first-order logic.

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

Limitations. Restricted expressiveness. Not all FOL expressible. Guard requirement constraining. Extensions can lose decidability.