Finite model property of guarded fragments

Ian Hodkinson


The guarded fragment of first-order logic, GF, was introduced in [H. Andreka, J. van Benthem, and I. Nemeti, Modal languages and bounded fragments of predicate logic, Journal of Philosophical Logic, 27(3):217-274, 1998].  The link is to the Kluwer journal page where you may (if it lets you in) be able to retrieve a .pdf file of the article.

The idea came from algebraic logic, and the motivation was to find a `modal-style' fragment of first-order logic that shared the nice properties of modal logic (such as decidability with reasonable complexity, and the finite model property), for similar reasons.  The rough idea of the guarded fragment is that quantification must always be relativised to an atomic formula. Other more expressive fragments along the same lines were introduced later:
The lectures will discuss these fragments and their background, but will mainly concern recent proofs of the finite model property for them.  These proofs use combinatorial results on extending partial isomorphisms of a finite structure to full automorphisms of a larger but still finite structure, developed in model theory by Hrushovski, Herwig, and Lascar.  The first application of these results to guarded fragments was in [E. Grädel, On the restraining power of guards, Journal of Symbolic Logic, vol. 64, pp. 1719-1742, 1999], where it is shown among other things (such as complexity results) that the guarded fragment has the finite model property.  LGF, PF, and CGF were shown to have the finite model property as well in I. Hodkinson, Loosely guarded fragment of first-order logic has the finite model property, Studia Logica 70 (2002) 205-240.  A simpler and nicer proof is in I. Hodkinson and M. Otto, Finite Conformal Hypergraph Covers, with Two Applications, Bull. Symbolic Logic 9 (2003) 387-405, available from the Bulletin here.

Extending partial isomorphisms

  1. Hrushovski's original proof that any finite graph A embeds in a finite graph B such that any partial isomorphism of A extends to an automorphism of B is in  E. Hrushovski, Extending partial isomorphisms of graphs, Combinatorica 12 (1992), 411-416.
  2. John Truss proved earlier in [J.K.Truss, Generic automorphisms of homogeneous structures, Proceedings of the London Mathematical Society 64, 121-141, 1992] that given a finite graph A and a single partial isomorphism p, there is a finite graph B extending A in which p is induced by an automorphism.
  3. Hrushovski's result was used to prove the small index property for the random graph in W. A. Hodges, I. M. Hodkinson, D. Lascar and S. Shelah, The small index property for $\omega$-stable $\omega$-categorical structures and for the random graph, J. London Math. Soc. (2) 48 (1993), 204 218.
  4. The first Herwig paper [B. Herwig, Extending partial isomorphisms on finite structures, Combinatorica 15 (1995) 365--371]  extended Hrusovski's result to arbitrary relational structures.  Here is a possibly early version of this paper, called Many $\omega$-categorical structures have the small index property.
  5. The second Herwig paper [B. Herwig, Extending partial isomorphisms for the small index property of many $\omega$-categorical structures, Israel J. Math. 107 (1998) 93-124] extended this to structures omitting certain homomorphic images (eg if A is a graph with no complete subgraph of size n, then B can be found with the same property).
  6. The Herwig-Lascar paper[B. Herwig and D. Lascar, Extending partial isomorphisms and the profinite topology on the free groups, Trans. Amer. Math. Soc. 352 (2000) 1985-2021] generalised this approach much further.  These two papers are both on Herwig's home page.
  7. The Herwig-Lascar paper has references to related work in free groups by Almeida and Delgado (and Marshall Hall).

Related work

The proof technique was used by Grohe in finite model theory - e.g., in [Martin Grohe, Equivalence in Finite-Variable Logics is Complete for Polynomial Time, Proc. IEEE Symposium on Foundations of Computer Science (LICS) 1996, pp. 264-273] and [Martin Grohe, Arity Hierarchies, Annals of Pure and Applied Logic 82 (1996) 103-163].

For other work see, e.g., [K. Auinger and B. Steinberg, On The Extension Problem For Partial Permutations, preprint I think].

A Google search will produce more.  It seems quite a big area now.