Finite model property of guarded fragments
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 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
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)
from the Bulletin here.
- The loosely guarded fragment
was introduced in Johan
van Benthem, Dynamic Bits And Pieces, ILLC technical report no.
- The packed fragment was
introduced in M
Marx, Tolerance Logic, Journal of Logic,
Language and Information 10 (3): 353-374, 2001.
- The similar clique-guarded
fragment was introduced in
E. Grädel, Decision procedures for guarded logics, in Automated Deduction
- CADE16. Proceedings of 16th International Conference on Automated
Trento, 1999, vol. 1632 of LNCS, Springer-Verlag, 1999.
Extending partial isomorphisms
- Hrushovski's original proof that any finite graph A embeds in a
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.
- John Truss proved earlier in [J.K.Truss, Generic automorphisms of homogeneous
structures, Proceedings of the London Mathematical Society 64,
1992] that given a finite graph A and a single partial isomorphism p,
is a finite graph B extending A in which p is induced by an
- Hrushovski's result was used to prove the small index property
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.
- The first Herwig paper [B. Herwig,
Extending partial isomorphisms on finite structures,
Combinatorica 15 (1995) 365--371] extended Hrusovski's result to
structures. Here is a possibly early version of this paper,
$\omega$-categorical structures have the small index property.
- 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).
- 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
These two papers are both on Herwig's home
- The Herwig-Lascar paper has references to related work in free
and Delgado (and Marshall Hall).
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
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