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 loosely guarded fragment
was introduced in Johan
van Benthem, Dynamic Bits And Pieces, ILLC technical report no.
LP-1997-01, 1997.
- 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
Deduction,
Trento, 1999, vol. 1632 of LNCS, Springer-Verlag, 1999.
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
- 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.
- 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.
- 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.
- 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.
- 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
much further.
These two papers are both on Herwig's home
page.
- 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.