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.

Metatheory. Decidable: 2EXPTIME-complete. Finite model property. Tree model property. Interpolation. Preserved under guarded bisimulation.

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.

© 2026 Lingenic LLC