Finite base property and guarded fragments

Go to home page

There are many examples of finite relation algebras that are representable but which only have infinite representations. The same holds for n-dimensional cylindric algebras (n>2). However, if we weaken the notion of representation, by relativising the relation operations (such as relative product, or cylindrification/quantification) to some distinguished relation, more positive results can be obtained.  See papers 1, 2 below.  The arguments use a combinatorial theorem of Herwig from model theory.

Herwig's theorem was modified in (3) below to prove that the packed fragment of first-order logic (similar to the clique-guarded fragment) has the finite model property.  In (4) a much simpler proof is given.  It uses Grädel's result that the guarded fragment has the finite model property (which he proved using Herwig's theorem).

Relevant references

Currently (June 00) available from Herwig's home page or via Freiburg Logik preprints page.

1. Mosaics and step-by-step -- Appendix to `A modal logic of relations' by Y Venema & M Marx

Robin Hirsch, Ian Hodkinson, Maarten Marx, Szabolcs Mikulás, and Mark Reynolds
In: Logic at Work, Essays dedicated to the memory of Elena Rasiowa. E. Orlowska (ed), Studies in Fuzziness and Soft Computing, vol. 24, Physica-Verlag, Heidelberg/New York, 1998, ISBN 3-7908-1164-5, pp. 158-167.
We give a proof of completeness, decidability and finite base property for the modal logic corresponding to the n-variable fragment of first-order logic, with modal semantics relativised to 'locally cubic' sets of assignments (worlds). All these results were already known, but the proofs we give appear new and use a combinatorial theorem of Herwig.

2. Finite algebras of relations are representable on finite sets

H. Andréka, I. Hodkinson, I. Németi
J. Symbolic Logic 64 (1999) 243-267.
Using a combinatorial theorem of Herwig on extending partial isomorphisms of relational structures, we give a simple proof that certain classes of algebras, including Crs, polyadic Crs, and WA, have the `finite base property' and have decidable universal theories, and that any finite algebra in each class is representable on a finite set. These results were first established by Andréka and Németi.

3. Loosely guarded fragment of first-order logic has the finite model property

I. Hodkinson
Studia Logica 70 (2002) 205-240.
We show that the loosely guarded and packed fragments of first-order logic have the finite model property. We use a construction of Herwig.  We point out some consequences in temporal predicate logic and algebraic logic.

4. Finite conformal hypergraph covers and Gaifman cliques in finite structures

I. Hodkinson and M. Otto
Bull. Symbolic Logic 9 (2003) 387-405.
Every finite hypergraph is shown to admit a cover by a finite conformal hypergraph. The notion of a hypergraph cover is based on homomorphisms that induce a bisimulation like back-and-forth system of local bijections between hyperedges. It is here introduced to capture the essential features of guarded bisimulations in the hypergraph setting. The classical hypergraph notion of conformality, defined by the requirement that all induced cliques be contained within hyperedges, thus corresponds to the collapse of clique guardedness to plain guardedness. As far as conformality is concerned, our construction can serve as a substitute in finite model theory for the straightforward but generally infinite unravelling of hypergraphs or relational structures.
Two immediate applications to the finite model theory of relational structures are presented: