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

Ian Hodkinson^{∗}

Department of Computing, Imperial College, London SW7 2BZ, UK

                   imh@doc.ic.ac.uk  http://www.doc.ic.ac.uk/~imh/

August 4, 2000

Abstract

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.

AMS classification: Primary 03B20; Secondary 03B45, 03C07, 03C13, 03C30, 03G15

Keywords: finite structures, modal logic, modal fragment, packed fragment

1 Introduction

Perhaps because beginning students of modal logic are often told that modal logic is more expressive than first-order logic and indeed has some second-order expressive power, or perhaps because they are hoping for something new, it can come as a surprise to them that every modal formula has a ‘standard translation’ into first-order logic. For example, ♢(p → □q) is translated to

∃y(R(x,y) ∧ (P(y) → ∀z(R(y,z) → Q(z)))).  (1)

The translation mimics the Kripke semantics for modal logic. Not every first-order formula (with one free variable in the appropriate signature) is the translation of a modal formula; so the formulas that are form a proper fragment of first-order logic, and one that inherits the nice properties of modal logic, such as decidability with reasonable complexity, interpolation, and the finite model property. The situation is similar for various multimodal, temporal, and dynamic logics — each corresponds by standard translation to a well-behaved modal-style fragment of classical logic.

Finding ‘modal fragments’ of first-order logic is an old problem in modal correspondence theory. One way to take it is to try to identify the first-order formulas that are equivalent to translations of modal formulas. Van Benthem [22, 25] proved that a first-order formula is equivalent to the translation of a modal one iff it is preserved under bisimulation. However, we cannot effectively identify these formulas, since it is undecidable whether a first-order formula is bisimulation-invariant [23, remark 4.19]. In certain restricted situations, this difficulty disappears. For example, the expressive completeness results of Kamp [16] show that over Dedekind-complete linear time, every first-order formula is equivalent to the translation of a temporal formula written with the binary modalities Until and Since. In such cases, the whole of first-order logic can be viewed as a modal fragment. But the situation here is rather special, and the lowish computational complexity of temporal logic (Pspace-complete over a wide range of flows of time including the natural numbers) is not matched by first-order logic (non-elementary over the natural numbers). These problems are to be expected if we do not explicitly bound the complexity of proving the equivalence of a first-order formula to a modal one.

∗Research partially supported by UK EPSRC grants GR/K54946, GR/L85978. Thanks to Ágnes Kurucz and Maarten Marx for stimulating discussions and helpful comments on drafts of this paper.

Let us focus instead on first-order formulas that are not merely equivalent to but actually are the translations of modal formulas of various kinds. The aim here is to define syntactically fragments of first-order logic containing the standard translations of various modal logics, and sharing their nice properties ‘for the same reasons’. Gabbay [4] suggested that the true modal fragments of first-order logic in this sense were the finite-variable fragments, since the standard translation of modal formulas can always be done with a bounded number of variables (by re-using them — in (1), we could have used x instead of z). This proposal is natural from the first-order viewpoint, general in that it is not confined to special situations, and for many-dimensional modal logic it is provably correct (cf. [4, lemma 3, p. 115]); but it suffered the objection that finite-variable fragments do not share the nice properties that (one-dimensional) modal logic has.

A different kind of (hopefully) modal fragment of first-order logic, the guarded fragment, was put forward by Andréka, van Benthem, and Németi [2]. Their idea was to look at quantification patterns instead. Only relativised quantification (along the accessibility relation of the Kripke frame) is allowed in modal formulas; so in the guarded fragment, all quantification must be relativised to some atomic formula. Thus, if φ(x,y,z) is a formula of the guarded fragment, then so are ∃yz(R(x,y,z) ∧ φ(x,y,z)) and ∀yz(R(x,y,z) → φ(x,y,z)), because x and the quantified y,z are ‘guarded’ by the relation symbol R. The plain ∃yzφ(x,y,z) would not be acceptable.

The guarded fragment does have the hoped-for nice properties. Decidability, and other results such as a �oś–Tarski theorem, were proved in [2, 23, 24]. Complexity results are established in [5, 18]: deciding validity for sentences of the guarded fragment, with or without equality, is complete for double-exponential time, but n-variable fragments of the guarded fragment (for finite n ≥ 2) are Exptime-complete, and some 2-variable guarded fragments are even in Pspace. It was proved in [5] that the guarded fragment has the finite model property — any guarded sentence with a model has a finite model. (For further discussion of surrounding issues, see, e.g., [3, 19, 26] as well as the citations already given.) Because of these results and others, the guarded fragment and various extensions of it (e.g., by fixed-point operators) have become rather popular. But the guarded fragment also was objected to on the ground that the standard translations of some quite respectable modalstyle formulas, such as temporal formulas involving Since and Until, fall outside the fragment. (The translation of U(p,q) is

∃y(x < y ∧ P(y) ∧ ∀z(x < z ∧ z < y → Q(z)))  (2)

— this is not in the guarded fragment because ∀z(x < z ∧ z < y → Q(z)) is not.) However, the ∀z is clearly guarded to some extent in (2): z doesn’t occur with x,y in a single atomic formula, but each pair of variables from x,y,z do (x and y become guarded in this way higher up the formula, by x < y). So van Benthem [24] proposed the loosely guarded fragment, which he also calls the pairwise guarded fragment. This fragment is our main topic here.

Roughly speaking, in the loosely guarded fragment, quantified variables must be pairwise guarded by atomic formulas. For example, if φ(x,y,z) is a formula of the loosely guarded fragment then so is ∃yz(R(x,y) ∧ R(y,z) ∧ S(x,z) ∧ φ(x,y,z)). (See definition 3.1 for details.) The loosely guarded fragment does contain (2). It is much more powerful than the guarded fragment, but still has many nice properties, such as decidability and reasonable complexity [2, 5, 18, 24]: identical complexity results to those already cited for the guarded fragment hold for the loosely guarded fragment.

Our results In the current paper (corollary 3.4), we prove that the loosely guarded fragment has the finite model property. In theorem 3.3, we do the same for the ‘packed fragment’, in which the guards themselves may be existentially quantified — this fragment was defined by Marx in order to characterise the loosely guarded fragment in terms of back-and-forth systems of partial isomorphisms defined on packed sets [19]. Our proofs use a slight modification, rather along the lines of [9], of part of a model-theoretic construction of Herwig [8]. The construction is effective and yields the decidability of these fragments, but we have not tried to fine-tune it to obtain smallest possible models or the complexity results already cited.

Our results add weight to the idea that these fragments are useful, though of course they do not exclude the possibility that larger ‘modal’ fragments exist. As a bonus, we derive some corollaries for predicate temporal logic, algebraic logic, and arrow logic, concerning decidability and the finite base/model property. Some of them were already known.

In a recent technical report [10], a tableau decision prodecure for the ‘clique guarded fragment’ is given. This fragment is related to the packed fragment referred to above. It is claimed that the finite model property for this fragment and the loosely guarded fragment follows from the proof, though the current version (May 19, 2000) states that there is still a gap in one of the lemmas needed for this corollary.

Outline of paper In section 2 we explain the modified Herwig construction, and then in section 3 we use it to derive the finite model property for the packed fragment and (as a corollary) the loosely guarded fragment. Some consequences in temporal, algebraic, and arrow logic are given in section 4.

Notation 1.1 We write ā∈ A to denote that āis an n-tuple of elements of the set A, for some finite n. For a tuple ā= (a_{1},...,a_{n}), we let rng(ā) denote the set {a_{1},...,a_{n}}. We write |ā| for the length of the tuple ā(so āis an |ā|-tuple). If ā= (a_{1},...,a_{n}) and b̄= (b_{1},...,b_{m}) are tuples, we write āb̄for their concatenation (a_{1},...,a_{n},b_{1},...,b_{m}). We often regard an element as a 1-tuple, so that ab̄denotes the tuple (a,b_{1},...,b_{m}), for example.

All maps are treated formally (as sets of ordered pairs, so we can write f ⊆ g, f ∪ g, etc), and are written on the left of their arguments — f(x) rather than xf, so that fg(x) and f ∘g(x) denote f(g(x)). For partial maps p,q, composition p∘q (or just pq) and inverse p^{−1} (for one-one p) are defined in the obvious way; note that ∘ is associative. We write the domain and range of a map f as domf,rng f respectively. If f is a map defined on rng(ā), where ā= (a_{1},...,a_{n}), we let f(ā) denote the tuple (f(a_{1}),...,f(a_{n})), and if A ⊆ domf, we write f(A) for {f(a) : a ∈ A}. (The potential ambiguity if ā or A is a member of domf is never a problem here.)

We usually use the same notation for a structure M as for its domain. Unless otherwise stated, when we write a formula as φ(x̄) it is implicit that x̄is a tuple of distinct variables containing at least the free variables of φ.

2 Herwig’s construction

Herwig’s theorems [7, 8] give a way of extending a finite structure to a larger one, still finite and inheriting some properties of the original structure, in such a way that all partial isomorphisms of the smaller structure extend to automorphisms of the larger one. Earlier results in this direction include [21], and in particular, those of Hrushovski [15]; the currently-used construction originated in [15] and the techniques used by Herwig are based on it. The construction consists of a ‘type-realising’ step and a second, ‘amalgamation’ step. In the Herwig–Lascar paper [9], the amalgamation step was absorbed into the more general context of free groups — this paper established striking equivalences between partial isomorphism extension results and known theorems in free groups, and proved a very strong extension theorem.

This work was motivated by pure model-theoretic considerations. Using it to prove the finite model property originated in joint work with several people [13, 1], and in Grädel [5] the finite model property for the guarded fragment was proved this way. For applications in other areas, see, e.g., [6].

Here, we will only need (a modification of) the type-realising part of the construction. Our approach is based on both [8, 9] but our notation is closer to that of the latter paper. The main new features are theorem 2.2(2) and definition 2.7. We need the following definition; the first four items are standard in model theory.

Definition 2.1 Let L be a finite relational signature (i.e., with no function or constant symbols), and M,N be L-structures.

1. We write M ⊆ N, and say that M is a substructure of N and that N is an extension of M, if dom(M) ⊆ dom(N), and for all n-ary R ∈ L and all n-tuples ā∈ M, we have M ⊧ R(ā) iff N ⊧ R(ā). An expansion of M is a structure in a larger signature got by adding interpretations of the new symbols; no new elements are added to the domain. A reduct of M to a smaller signature is got by forgetting the interpretations of the surplus symbols; no domain elements are removed.

2. A partial map p: M → N is said to be a partial isomorphism if it is one-one, and for all R ∈ L, of arity n, say, and for all n-tuples ā∈ dom(p), we have M ⊧ R(ā) iff N ⊧ R(p(ā)).

3. An automorphism of M is a bijective partial isomorphism from M to M. The set of all automorphisms of M is written AutM; it is a group under composition of maps.

4. A homomorphism from M to N is a total map f : M → N such that for all n-ary R ∈ L and n-tuples ā∈ M, if M ⊧ R(ā) then N ⊧ R(f(ā)).

5. For n > 0, an n-tuple ā∈ M is said to be live (in M) if n = 1 or there is an n-ary relation symbol R ∈ L with M ⊧ R(ā).

6. A subset A of M is said to be packed (in M) if whenever a,b ∈ A are distinct, there is c̄∈ A which is live in M and with a,b ∈ rng(c̄). A tuple ā∈ M is said to be packed if rng(ā) is packed.

The dependence on M in (6) is really only a dependence on the signature of M; we will use that a set packed in M is packed in any expansion of M. Every subset of M of size at most 1 is vacuously packed. Note that for non-binary signatures, with relation symbols of higher arity than two, not every subset of a packed set need be packed.

We aim to prove the following, which (we repeat) is a modification of work in [8, 9].

Theorem 2.2 Let L be a finite relational signature and K a finite L-structure. Let r < ω. Then there is a finite L-structure H = H_{r}(K), a substructure \overline{K}⊆ H, and a surjective homomorphism π: \overline{K}→ K, with the following properties:

1. For every partial isomorphism p of K, there is p̂ ∈ AutH such that if a ∈ \overline{K} and π(a) ∈ domp then p̂(a) ∈ \overline{K}and pπ(a) = πp̂(a). That is, p ∘ π ⊆ π ∘ p̂.

2. If A ⊆ H and A is packed in H then there is g ∈ AutH with g(A) ⊆ \overline{K}.

3. For every prenex universal L-formula θ(x̄) = ∀ȳφ(x̄,ȳ), where φ is quantifier-free and x̄ȳis a non-repeating tuple of variables of length at most r, and every ā∈ \overline{K} such that π↾rng(ā) is one-one and rng(ā) ⊆ A for some packed A ⊆ H, we have \overline{K}⊧ θ(ā) ⇒ K ⊧ θ(π(ā)).

This will be proved in section 2.3.

Problem 2.3 (Marx) For L,K as above, is there a finite L-structure H ⊇ K such that any partial isomorphism of K extends to an automorphism of H, and any packed subset of H can be mapped by an automorphism of H into K?

Theorem 2.2 is an approximation to this, as is one of the main results in [8], which (roughly speaking) constructs H such that any partial isomorphism of K extends to an automorphism of H, any live tuple of H can be mapped by an automorphism of H into K, and any packed subset of H can be mapped by a homomorphism into K. A positive solution to problem 2.3 would allow a simpler proof of our results.

2.1 The construction informally

It may help to outline the proof of theorem 2.2 to be given in sections 2.2 and 2.3. Those readers not interested may of course skip this section. Those who are are hereby warned that while we will make every effort not to mislead, because of lack of space we will not be able to discuss every detail of the proof, nor even to be completely accurate about the details we do discuss. Nothing said here should be taken as contradicting the formal definitions given in the proof later on.

2.1.1 The structure K^{(r)} and its parts

To prove the theorem, we will construct an auxiliary structure K^{(r)} ⊇ K.

• K^{(r)} will consist of disjoint blocks or components K = K_{0},K_{1},...,K_{r}.

• Part of each component is (roughly speaking) a copy of K. \overline{K}^{(r)} will denote the the substructure of K^{(r)} whose domain is the union of these copies of K.

• We let K̂^{(r)}denote the substructure of K^{(r)} with domain K^{(r)}\K; this structure will be the H_{r}(K) of theorem 2.2.

• The part of \overline{K}^{(r)} inside K̂^{(r)}will be the substructure \overline{K} of theorem 2.2. The fact that \overline{K} consists of ‘copies’ of K yields part 3 of theorem 2.2 (π projects each copy back onto K).

See figure 1.

2.1.2 Extending partial isomorphisms of K to K^{(r)}

K^{(r)} is stretched in that no component K_{i} for i > 0 contains more than one element of any live tuple of elements of K^{(r)}, though this element can crop up several times in the tuple. (The term ‘stretched’ is from [9]. Note that K_{0} has a special status.) The ‘copy’ of K in a component K_{i} (i > 0) is therefore not an exact copy, because it contains no live tuple of length > 1. We call it a ‘copy’ because if a_{1}, ...,a_{n} are elements of K and its copies, the corresponding elements of the original K being b_{1},..., b_{n}, then for any n-ary R ∈ L, R(a_{1},...,a_{n}) will hold in K^{(r)} iff R(b_{1},...,b_{n}) holds in K and |{a_{1},..., a_{n}} ∩ K_{i}| ≤ 1 for each i > 0.

\underbrace{K^{(r)}} \underbrace{K̂^{(r)}(= H_{r}(K))} . . . . . .  K_{r} K_{2} K_{1} K  \} \overline{K}^{(r)} (= K ∪ \overline{K})
Figure 1: The structure K^{(r)}, components K,K_{1},...,K_{r} and substructures K̂^{(r)},\overline{K}^{(r)}.

Stretchedness of K^{(r)} means that the only ‘definable’ relations that hold within a single component are essentially unary. This makes it quite easy to extend any partial isomorphism p of K to the new components of K^{(r)}, and even so as to form a permutation of each component extending the map induced by p on the ‘copy’ of K in the component. To do it, we will build the components K_{1},...,K_{r} by induction, ensuring that each new component has just the right number of elements of any given isomorphism type over the existing components.

Let us discuss in more detail what this means. Suppose inductively that we have built K^{(r)}, for some r ≥ 0, and extended p to a partial isomorphism ψ of K^{(r)} such that ψ↾K_{i} is a permutation of K_{i} for 1 ≤ i ≤ r. K^{(r+1)} will be some stretched extension of K^{(r)}, including a new component K_{r+1} . Here we discuss what properties it needs to have.

Let ψ′ be any extension of ψ such that ψ′↾K_{r+1} is a permutation of K_{r+1} . Consider what is required for ψ′to be a partial isomorphism of K^{(r+1)} . By stretchedness, it is sufficient (and necessary) that for any a ∈ K_{r+1} , the tuples ab̄and ψ′(a)ψ(b̄) satisfy exactly the same atomic formulas (in K^{(r+1)} of course), for any tuple b̄∈ domψ. Here and below, ‘atomic’ formulas exclude equalities.

The set t of atomic formulas α(x,b̄), for b̄ ∈ domψ, satisfied by a is called the type of a (over domψ), and b̄ is a tuple of parameters of t. Abstractly, a type over a set D ⊆ K^{(r)} is a set of atomic formulas with parameters from D. Now ψ ‘translates’ t to the type ψ(t) = {α(x,ψ(b̄)) : α(x,b̄) ∈ t}. So what we require for ψ′to be a partial isomorphism of K^{(r+1)} is that for any a ∈ K_{r+1} with type t over domψ, ψ′(a) has type ψ(t) over rngψ.

For any D ⊆ K^{(r)} and type t over D, let E_{t}^{D} denote the set of elements of K_{r+1} with type t over D. K_{r+1} is both the disjoint union of the E_{t}^{domψ} and the disjoint union of the E_{ψ(t)}^{rngψ}, as t ranges over

types over domψ. Then ψ′is a partial isomorphism of K^{(r+1)} iff ψ′↾E_{t}^{domψ} is a bijection from E_{t}^{domψ} to E_{ψ(t)}^{rngψ} for each type t over domψ. So to have any hope of extending ψ to such a ψ′, we need to

construct K_{r+1} so that for any type t over domψ, E_{t}^{domψ} and E_{ψ(t)}^{rngψ} have the same size. But given this, since the ‘copy’ q of p induced on the copy of K in K_{r+1} is necessarily a partial one-one map from E_{t}^{domψ} to E_{ψ(t)}^{rngψ}, we may extend q to a bijection : E_{t}^{domψ} → E_{ψ(t)}^{rngψ}. This can be done for all t, yielding a partial isomorphism of K^{(r+1)} extending both ψ and the copy of p and acting as a permutation on K_{r+1} . In fact, this argument works for any q such that ψ ∪ q is a partial isomorphism of K^{(r+1)} .

So we want to construct K_{r+1} so that E_{t}^{domψ} and E_{ψ(t)}^{rngψ} have the same cardinality, for every t and for the extension ψ of each partial isomorphism p of K. The type over domψ of a new element introduced into K_{r+1} is determined once and for all at the time we add it, for each ψ, and its types over different domψs interact. For example, if we add elements satisfyng precisely the formulas in the type t, the sets E_{t}^{domψ} increase in size for all ψ defined on the parameters of t. So it seems we have a difficult problem here. The ingenious method used to solve it comes from [15, 7, 8, 9], and constitutes the most crucial idea in the proof. We shift attention from an element having a given type, to its realising a type.

An element realises type t if it satisfies all the formulas in t. Clearly, it may satisfy more formulas than these. Write R_{t} for the set of elements of K_{r+1} that realise t. Unlike E_{t}^{D}, R_{t} depends only on t, not on any set D. Because of this simpler situation, we can easily arrange that the number |R_{t}| of elements of K_{r+1} realising a given type t depends only on |t|, the number of formulas in t. This can be done as follows. We construct K_{r+1} starting with a fresh copy of K. The copies of elements of K have the same types over K^{(r)} as the originals. We then add further elements in stages, realising first the largest possible types over K^{(r)}, then the next largest, and so on, down to the empty type. Each stage is used to ‘pad out’ the numbers of elements realising the types of the currently-considered size to be the same. In this way we can control the interaction between types: elements added at earlier stages may realise types considered later, but not vice versa, because the sizes of types are decreasing. So our work in the current stage will not be destroyed in later stages. The totality of elements added in this way (after deleting any that violate stretchedness) constitute the new component K_{r+1} , and these elements plus the old ones in K^{(r)} constitute the extension K^{(r+1)} .

It can now be shown by induction that |E_{t}^{domψ}| = |E_{ψ(t)}^{rngψ}| for all ψ,t as above, using the obvious

fact that |t| = |ψ(t)|. Assume inductively that |E_{u}^{domψ}| = |E_{ψ(u)}^{rngψ}| for all types u over domψ with

u ⊃ t. The elements of E_{t}^{domψ} are those elements of K_{r+1} that (a) realise t, and (b) are not in E_{u}^{domψ} for any u ⊃ t. Similarly, E_{ψ(t)}^{rngψ} is the set of elements of K_{r+1} that (a) realise ψ(t) and (b) are not in E_{ψ(u)}^{rngψ} for any u ⊃ t. By construction, the number of (a)-elements is the same on both sides, and by the inductive hypothesis the same goes for the number of elements excluded by (b). So we obtain |E_{t}^{domψ}| = |E_{ψ(t)}^{rngψ}|. See lemma 2.15 for details.

2.1.3 Admissible types

We can get this far, proving part 1 of theorem 2.2, without caring which types over K^{(r)} the elements of K_{r+1} have, but only how many elements have a given type. To impose extra properties on the structures K^{(r)} — in particular, to obtain part 2 of the theorem, that any packed subset of K̂^{(r)}is mapped by an automorphism of K̂^{(r)}into the union ‘\overline{K}^{(r)}’ of the copies of K — we need to control which types are realised in K_{r+1} . This is in fact quite easy to do: K_{r+1} is built in stages and we have great freedom at each stage to choose which types to realise, so long as we then equalise the numbers of realisations as already described.

Much of the evolution of the construction through [15, 7, 8, 9] can be viewed (at least by the author) as refining the selection of types to realise in K_{r+1} . We will call the types chosen to be realised the admissible types. To extend partial isomorphisms as already described, it is sufficient that the chosen notion of admissibility satisfies the following axioms (cf. lemmas 2.8–2.11):

1. the type over K^{(r)} of any element of K is admissible [so we can start K_{r+1} with a copy of K],

2. no tuple of parameters in an admissible type violates stretchedness of K^{(r+1)} ,

3. any restriction of an admissible type to a smaller parameter set is admissible,

4. if ψ is a partial isomorphism of K^{(r)} inducing a permutation of each non-zero component, and t is an admissible type over domψ, then ψ(t) is also admissible.

In the construction of K_{r+1} , we now arrange at each stage that all types of new elements over K^{(r)} are admissible and that the number of elements realising a given admissible type t depends only on |t|. The axioms (especially the last two) allow us to replicate the argument of section 2.1.2 and obtain theorem 2.2(1). But they do not appear to be sufficient to prove theorem 2.2(2): we need further restrictions on which types are realised in K_{r+1} .

Roughly, we will define a type t over K^{(r)} to be admissible if there is a partial isomorphism ψ of K^{(r)} inducing a permutation of each non-zero component, defined on t, and such that ψ(t) is the type of some element of K (i.e., K_{0}). The above axioms all easily follow from this. Furthermore, assuming that all elements of K_{r+1} have admissible types over K^{(r)} in this sense, we can show that any packed subset of K^{(r)} is mapped into \overline{K}^{(r)} by a partial isomorphism ψ of K^{(r)} that induces (by restriction) an automorphism of K̂^{(r)}. This clearly implies theorem 2.2(2).

The way we show this constitutes the second most crucial idea of the proof. Again, we assume the property inductively for K^{(r)} and try to prove it for K^{(r+1)} . So let A ⊆ K^{(r+1)} be a packed set. If A ⊆ K^{(r)}, the result is easily proved using the inductive hypothesis. So assume that A ⊈ K^{(r)}. As A is packed and K^{(r+1)} is stretched, A ∩ K_{r+1} consists of a single element, say a. By packedness, the definition of admissibility, and the argument of section 2.1.2, we can assume without loss of generality that a ∈ \overline{K}^{(r+1)} . Let B ⊆ K^{(r)} be obtained by replacing a by the corresponding element, say b, of the original K ( = K_{0}). Then B is also packed, so inductively we may take a partial isomorphism ϕ of K^{(r)} that induces by restriction a permutation of each K_{i} (i > 0), and satisfies ϕ(B) ⊆ \overline{K}^{(r)}. Let p = ϕ↾K, and let q be the map induced by p on the copy of K in the new component K_{r+1} . By construction of K_{r+1} , ϕ ∪ q is a partial isomorphism of K^{(r+1)} , so by the argument of section 2.1.2, it extends to a partial isomorphism ϕ′of K^{(r+1)} that induces a permutation on K_{r+1} . Now a corresponds to b, so ϕ′(a) = q(a) corresponds to p(b). Since p(b) ∈ K, we have ϕ′(a) ∈ \overline{K}^{(r+1)} . So ϕ′(A) ⊆ \overline{K}^{(r+1)} , as required.

2.2 The construction formally

We adopt these conventions for the proof:

Convention 2.4

1. All structures mentioned are finite L-structures.

2. By atomic formula we will mean an atomic L-formula other than an equality. We write α(x̄) for such a formula (see notation 1.1 here).

We prove theorem 2.2 by establishing an auxiliary proposition, which also gives more information about the structure of H_{r}(K). Figure 1 may help in picturing it.

Proposition 2.5 Let L be a finite relational signature and K a finite L-structure. For each r < ω, there is a finite L-structure K^{(r)} ⊇ K, whose domain is the disjoint union of ‘components’ K = K_{0}, K_{1},...,K_{r}, and one-one maps ν_{i} : K → K_{i} for each i ≤ r (where ν_{0} is the identity map on K), with properties 1– 4 below. We use the following notation:

• We write K̂^{(r)}for the substructure of K^{(r)} with domain K^{(r)}\ K.

• We write \overline{K}^{(r)} for the substructure of K^{(r)} with domain ⋃ _{i≤r} ν_{i}(K).

• A set A of elements of K^{(r)} is said to be stretched (in K^{(r)}) if |A∩K_{i}| ≤ 1 for every i with 1 ≤ i ≤ r. A tuple āis stretched if rng(ā) is stretched. (This notion occurs in about the same form in [9].)

1. Any live tuple of K^{(r)} is stretched.

2. For each i ≤ r, each atomic formula α(x,ȳ), and each a ∈ K, b̄∈ ⋃ _{j<i} K_{j}, we have

K^{(r)} ⊧ α(a,b̄) ↔ α(ν_{i}(a),b̄).

3. For every partial isomorphism p of K and each i with 1 ≤ i ≤ r, there is a permutation p_{i} of K_{i} such that:

• p_{i}∘ ν_{i} extends ν_{i}∘ p. That is, p_{i}(ν_{i}(a)) = ν_{i}(p(a)) for all a ∈ dom(p).

• The map p ∪ ⋃ _{1≤i≤r} p_{i} is a partial isomorphism of K^{(r)}.

4. If A ⊆ K^{(r)} is packed (in K^{(r)}) then there is a partial isomorphism ψ of K^{(r)} such that ψ↾K_{i} is a permutation of K_{i} for all i with 1 ≤ i ≤ r, and satisfying ψ(A) ⊆ \overline{K}^{(r)}.

Proof The proof will occupy most of this section. For the duration, we fix L,K as in the formulation of the proposition. The proof is by induction on r. For r = 0, we may let K^{(0)} = K; for condition 4 we take ψ to be the identity map on K. Assume inductively that K^{(r)},ν_{0},...,ν_{r} have been constructed, satisfying the conditions of the proposition. We will obtain K^{(r+1)} from K^{(r)} by adding a new component K_{r+1} disjoint from K^{(r)}. To do this, we will use types.

2.2.1 Types

Definition 2.6

1. A type over K^{(r)}, or for short, type, is a set t of atomic formulas with one free variable, always x, and parameters in K^{(r)}: i.e., formulas of the form α(x,c̄), where α(x,ȳ) is atomic (not an equality — see convention 2.4) in which x occurs free, and c̄∈ K^{(r)}.

2. For a type t, |t| denotes the cardinality of (i.e., number of formulas in) t, and base t denotes the set of all elements of K that genuinely occur in formulas in t — so base t = {a ∈ K : α(x,a,b̄) ∈ t for some b̄∈ K^{(r)} and atomic α(x,y,z̄) in which x,y occur free}.

3. If t is a type and D ⊆ K, we write t↾D for {α(x,ā) ∈ t : ā∈ K̂^{(r)}∪ D}.

4. Let M ⊇ K^{(r)} and a ∈ M.

(a) If t is a type, a is said to realise t if M ⊧ α(a,c̄) for all α(x,c̄) ∈ t.

(b) If D ⊆ K, we write tp(a/D) for the set

{α(x,c̄) : α(x,ȳ) atomic with x among its free variables, c̄∈ K̂^{(r)}∪ D, M ⊧ α(a,c̄)}.

The definition of base reflects our interest in parameters from K; use of parameters from K̂^{(r)} in types is unrestricted and the reader should always bear in mind that formulas in a type can have parameters that are not in the base of the type. It is critical to note that a realising t does not imply that tp(a/base t) = t, but only tp(a/base t) ⊇ t. Also, base(tp(a/D))⊆ D, but we may not have equality. These and other simple facts about bases, such as tp(a/D) = tp(a/base (tp(a/D))) for any a ∈ K, D ⊆ K, will be used without mention later on.

Strictly, the definitions in (4) depend on M, so we should say that a realises t in M, and write tp_{M}(a/D). But formulas in types are atomic, so a realises t in M iff a realises t in M′, for any M′⊇ M, and similarly for tp(a/D). Consequently, the dependence never makes a difference in practice, and therefore we refrain from overloading the notation.

2.2.2 Admissible types

There is a lot of freedom in the construction to choose the kinds of type we wish to realise. We will choose the ‘admissible’ types.

Definition 2.7

1. We write Ψ^{(r)} for the set of all partial isomorphisms ψ of K^{(r)} such that ψ↾K_{i} is a permutation of K_{i} for all 1 ≤ i ≤ r.

2. If ψ ∈ Ψ^{(r)} and t is a type with base t ⊆ domψ, we write ψ(t) for the type {α(x,ψ(ā)) : α(x,ā) ∈ t}. A conjugate of t is any type of the form ψ(t) for ψ ∈ Ψ^{(r)} with base t ⊆ domψ.

3. A type t is said to be admissible if it is a conjugate of tp(a/D) for some a ∈ K and D ⊆ K.

So if t is admissible then t = ψ(tp(a/D)) for some ψ,a,D as above; so base(tp(a/D)) ⊆ domψ, but D may be larger than base(tp(a/D)) and we may not have D ⊆ domψ. The only properties of admissible types needed to extend partial isomorphisms are encapsulated in the following simple lemmas.

Lemma 2.8 Any conjugate of an admissible type is admissible.

Proof Since Ψ^{(r)} contains the identity map on K^{(r)} and is closed under inverse and composition, conjugacy is an equivalence relation on types. The lemma follows immediately from this. □

Lemma 2.9 If a ∈ K then tp(a/K) is admissible.

Proof Trivial. □

Lemma 2.10 If t is an admissible type, α(x,ȳ) is an atomic formula in which all variables of xȳ occur, and α(x,c̄) ∈ t, then c̄is stretched in K^{(r)}.

Proof Let t,α,c̄ be as stated. As t is admissible, there are a ∈ K, D ⊆ K, and ψ ∈ Ψ^{(r)} with base (tp(a/D)) ⊆ domψ and ψ(tp(a/D)) = t. So α(x,ψ^{−1} (c̄)) ∈ tp(a/D) and K^{(r)} ⊧ α(a,ψ^{−1} (c̄)). So rng(aψ^{−1} (c̄)) = rng(b̄) for some live tuple b̄∈ K^{(r)}. Inductively, by proposition 2.5(1) for K^{(r)}, b̄, and hence aψ^{−1} (c̄), ψ^{−1} (c̄), and c̄, are stretched in K^{(r)}. □

Lemma 2.11 Let t be any admissible type. Then t↾D is admissible for every D ⊆ K.

Proof We have t = ψ(tp(a/E)) for some a ∈ K, E ⊆ K and ψ ∈ Ψ^{(r)} with base (tp(a/E)) ⊆ domψ. Let D′= ψ^{−1} (D ∩ rngψ). Then base t ⊆ rngψ, so clearly, t↾D= t↾(D ∩ rngψ) = t↾ψ(D′) = ψ(tp(a/E)↾D′) = ψ(tp(a/E ∩ D′)). This is of the required form, and so t↾D is admissible. □

2.2.3 Building the structure K^{(r+1)}

We are going to start the construction of K^{(r+1)} now, by building its new component K_{r+1} . This component will itself be built by an inductive construction: we build a chain of sets S_{0} ⊆ S_{1} ⊆ ···⊆ S_{l} = K_{r+1} , and a chain of structures K^{(r)} ⊆ K_{0}^{(r+1)} ⊆ K_{1}^{(r+1)} ⊆ ···⊆ K_{l}^{(r+1)} = K^{(r+1)} , where l is the largest cardinality of any admissible type. See figure 2. We will also define a bijection ν_{r+1} : K → S_{0}. The structures K_{j}^{(r+1)} (for each j = 0,1,...,l) will have the following properties:

. . . . . .  K_{r} K_{2} K_{1} K  ⋮ K_{r+1} ⋮ S_{0} S_{1} S_{2} ⋮ S_{l}
Figure 2: The new component K_{r+1} of K^{(r+1)}

(i) The domain of K_{j}^{(r+1)} is the disjoint union of K^{(r)} and S_{j}. The components of K_{j}^{(r+1)} are

K,K_{1},...,K_{r}, and S_{j}. (So in K_{j}^{(r+1)} , the notion of stretched tuple makes sense.)

(ii) Any live tuple in K_{j}^{(r+1)} is stretched.

(iii) For any atomic formula α(x,ȳ), a ∈ K, and b̄∈ K^{(r)}, we have K_{j}^{(r+1)} ⊧ α(a,b̄) ↔ α(ν_{r+1} (a),b̄).

(iv) For any admissible type t with |t| > l − j, the number of elements of S_{j} that realise t in K_{j}^{(r+1)} depends only on |t|.

(v) tp(a/K) is admissible for every a ∈ S_{j}.

Below, we will refer to these as ‘property (i)’, etc.

S_{0} is obtained simply by taking a new copy of K, disjoint from K^{(r)}. Formally, we may let S_{0} = K × {K^{(r)}}. Thus, K_{0}^{(r+1)} has domain K^{(r)}∪ S_{0}, for i ≤ r, its ith component is defined to be the same as that of K^{(r)}, and its (r + 1)th component is defined to be S_{0}. We let ν_{r+1} : K → S_{0} be given by ν_{r+1} (a) = (a,K^{(r)}), for a ∈ K.

We define K_{0}^{(r+1)} as an L-structure as follows. Let μ: K_{0}^{(r+1)} → K^{(r)} be the map that is the identity on K^{(r)} and is ν_{r+1}^{−1} on S_{0}. Then if R ∈ L is n-ary and ā∈ K_{0}^{(r+1)} is an n-tuple, we define

K_{0}^{(r+1)} ⊧ R(ā) iff āis stretched in K_{0}^{(r+1)} andK^{(r)} ⊧ R(μ(ā)).  (3)

Note that μ is a homomorphism.

Lemma 2.12 K_{0}^{(r+1)} ⊇ K^{(r)}, and K_{0}^{(r+1)} satisfies properties (i)–(v) above.

Proof By the definition of K_{0}^{(r+1)} ((3) above), K_{0}^{(r+1)} ⊇ K^{(r)}. Clearly, K_{0}^{(r+1)} has components K,K_{1}, ...,K_{r},S_{0} and all live tuples in it are stretched.

We check property (iii). Take α(x,ȳ),a,b̄ as in property (iii); we may assume that all variables in xȳ occur in α. Then K_{j}^{(r+1)} ⊧ α(a,b̄) iff ab̄ is stretched and K_{j}^{(r)} ⊧ α(a,b̄) [by (3), noting as in lemma 2.10 that the change from R to α does not affect stretchedness], iff ν_{r+1} (a)b̄ is stretched and K_{j}^{(r)} ⊧ α(μ(ν_{r+1} (a)),b̄) [by definition of ‘stretched’ and because μ(ν_{r+1} (a)) = a], iff K_{j}^{(r+1)} ⊧ α(ν_{r+1} (a),b̄) [by (3)], as required.

Property (iv) holds vacuously since there is no admissible type t with |t| > l. To check property (v), let a ∈ S_{0} and let t = tp(a/K). By property (iii), tp(μ(a)/K) = t. By lemma 2.9, t is admissible. □

Assume now that j < l and that K_{j}^{(r+1)} is defined. We will construct K_{j+1}^{(r+1)} along the lines of section 2.1.2, which the reader may wish to review. Remember that types have parameters in K^{(r)}.

First, a definition. If M ⊇ K^{(r)} and t is an admissible type, we write M + t for the L-structure extending M obtained by adding to M a single new point b, say, and defining M + t ⊧ α(b,c̄) iff α(x,c̄) ∈ t, for all atomic formulas α(x,ȳ) and all c̄∈ M. Of course, as the parameters of t are in K^{(r)}, M + t ⊧ α(b,c̄) implies c̄∈ K^{(r)}. M + t is unique up to isomorphism. For types t_{1},...,t_{n}, we define M + t_{1}+ ··· + t_{n} to be (··· ((M + t_{1}) + t_{2}) + ··· ) + t_{n}.

Let the admissible types of cardinality l − j be t_{0},...,t_{s−1} , say, enumerated without repetitions. Let

m_{i} = |{a ∈ S_{j} : a realises t_{i} inK_{j}^{(r+1)} }|, for each i < s,
m = max{m_{i} : i < s},
K_{j+1}^{(r+1)} = K_{j}^{(r+1)} + \underbrace{t_{0}+ t_{0}+ ··· + t_{0}}_{m−m_{0} times}+··· + \underbrace{t_{s−1} + t_{s−1} + ··· + t_{s−1}}_{m−m_{s−1} times},

and define S_{j+1} to consist of S_{j} plus all the new points of K_{j+1}^{(r+1)} \ K_{j}^{(r+1)} . So S_{j+1} = K_{j+1}^{(r+1)} \ K^{(r)}.

Define the components of K_{j+1}^{(r+1)} to be K_{0},...,K_{r},S_{j+1} .

Lemma 2.13 K_{j+1}^{(r+1)} ⊇ K_{j}^{(r+1)} , and K_{j+1}^{(r+1)} satisfies properties (i)–(v).

Proof Clearly, K_{j+1}^{(r+1)} ⊇ K_{j}^{(r+1)} . Property (i) holds for K_{j+1}^{(r+1)} by construction. For property (ii),

assuming inductively that the property holds for K_{j}^{(r+1)} , we need only show that if āis live in K_{j+1}^{(r+1)}

and rng(ā) ⊈ K_{j}^{(r+1)} then ā is stretched. We assume for notational simplicity that ā= bc̄ where

b ∈ S_{j+1} \ S_{j} and c̄∈ K_{j+1}^{(r+1)} , and that K_{j+1}^{(r+1)} ⊧ α(b,c̄) for some atomic α(x,ȳ) in which all variables

in xȳ occur free. But then by definition of K_{j+1}^{(r+1)} , α(x,c̄) ∈ t_{i} for some i < s. As t_{i} is admissible,

lemma 2.10 yields that c̄is stretched in K^{(r)}. As b ∈ S_{j+1} , bc̄is clearly stretched in K_{j+1}^{(r+1)} .

Property (iii) is immediate, because it holds for the substructure K_{0}^{(r+1)} of K_{j+1}^{(r+1)} .

We now check property (iv). First, note that if i,i′< s and i ≠ i′ then |t_{i}| = |t_{i′}|, t_{i} ≠ t_{i′}, so that t_{i′} ⊈ t_{i}. Because by construction the elements of S_{j+1} \ S_{j} realise exactly the formulas in some t_{i}, and no more, each of them realises exactly one type t_{i} (for some i < s). So, any point of S_{j+1} realising t_{i} is in fact in K_{j}^{(r+1)} + t_{i}+ t_{i}+ ··· + t_{i} (in the obvious sense). There are m_{i} such points in S_{j}, and we added m − m_{i} more to S_{j+1} . So the number of realisations of t_{i} in S_{j+1} , for any i < s, is exactly m.

We must check that we have not destroyed the inductive hypothesis (for larger types than the t_{i}) by adding the new points. For any admissible type u with |u| > l − j, we have u ⊈ t_{i} for any i < s. Because the points of S_{j+1} \S_{j} satisfy only the formulas of some unique t_{i}, none of them realise u. So all realisations of u in S_{j+1} are in fact in S_{j}. By property (iv) for K_{j}^{(r+1)} , the number of them depends only on |u|. Thus, property (iv) holds for all admissible types of size > l − (j + 1).

Property (v) is easily seen. Inductively, it holds for all a ∈ S_{j}. Let a ∈ S_{j+1} \ S_{j}, and suppose that a realises type t_{i} for (unique) i < s. Then tp(a/K) = t_{i}, which is admissible. □

We now define K^{(r+1)} = K_{l}^{(r+1)} and K_{r+1} = S_{l}. As K^{(r+1)} ⊇ K^{(r)}, the inductive hypothesis and properties (i)–(iii) above imply that the first two conditions of proposition 2.5 hold and that the components of K^{(r+1)} are as demanded.

2.2.4 Defining permutations of K_{r+1}

Here, we show how to take any extension of a map ψ in Ψ^{(r)} to a partial isomorphism of K^{(r+1)} , and extend it to an element of Ψ^{(r+1)} . (Here, as for r, Ψ^{(r+1)} is the set of all partial isomorphisms ψ′of K^{(r+1)} such that ψ′↾K_{i}is a permutation of K_{i} for each i with 1 ≤ i ≤ r + 1.) The crucial observation needed to do it is property (iv) of the construction of K_{r+1} — that in K^{(r+1)} , the number of realisations of any admissible type depends only on the cardinality of the type. This extension result will be used in section 2.2.5 to establish conditions 3 and 4 of proposition 2.5.

Fix ψ ∈ Ψ^{(r)}, and define:

D = K ∩ domψ,
D′ = ψ(D),
A = {t : t an admissible type with base t ⊆ D},
and for t ∈ A, E_{t} = {a ∈ K_{r+1} : tp(a/D) = t},
and E′_{t} = {a ∈ K_{r+1} : tp(a/D′) = ψ(t)}.

E_{t}is the set of elements of K_{r+1} whose type over D is exactly t. The E_{t}(t ∈ A) are pairwise disjoint, as are the E′_{t}. By property (v) of the construction of K^{(r+1)} , and lemma 2.11, K_{r+1} = ⋃ _{t∈A} E_{t} = ⋃ _{t∈A} E′_{t}.

Lemma 2.14 Let q be a 1–1 partial map : K_{r+1} → K_{r+1} . Then in the notation above, the following are equivalent:

1. ψ ∪ q is a partial isomorphism of K^{(r+1)} .

2. Whenever α(x,ȳ) is atomic, x occurs free in α, a ∈ domq, and c̄∈ dom(ψ), we have K^{(r+1)} ⊧ α(a,c̄) ↔ α(q(a),ψ(c̄)).

3. ψ(tp(a/D)) = tp(q(a)/D′) for any a ∈ domq.

4. For any t ∈ A, q↾E_{t}is a 1–1 partial map from E_{t} to E′_{t}.

Proof As ψ is a partial isomorphism of K^{(r)}, K^{(r)} ⊆ K^{(r+1)} , and all live tuples in K^{(r+1)} are stretched, it is clear that ψ ∪ q is a partial isomorphism of K^{(r+1)} iff condition 2 holds.

Now let α,a,c̄ be as in (2). Then K^{(r+1)} ⊧ α(a,c̄) iff α(x,c̄) ∈ tp(a/D), since c̄∈ dom(ψ) = D ∪ K̂^{(r)}. Similarly, K^{(r+1)} ⊧ α(q(a),ψ(c̄)) iff α(x,ψ(c̄)) ∈ tp(q(a)/D′). We conclude that (2) holds iff α(x,c̄) ∈ tp(a/D) ⟺ α(x,ψ(c̄)) ∈ tp(q(a)/D′) for all a,α,c̄as above. But this just says that ψ(tp(a/D)) = tp(q(a)/D′) for all a ∈ domq. Hence, (2) and (3) are equivalent.

For (3) ⇒ (4), if t ∈ A and a ∈ E_{t}∩ domq then tp(a/D) = t, and assuming (3), we obtain tp(q(a)/D′) = ψ(t), so q(a) ∈ E′_{t}. Thus, (4) holds. For the converse, assume (4) and let a ∈ domq. As K_{r+1} = ⋃ _{t∈A} E_{t}, a ∈ E_{t} for some (unique) t ∈ A, so that tp(a/D) = t. By (4), q(a) ∈ E′_{t} so tp(q(a)/D′) = ψ(t), giving (3). □

The following originated in [7] and is the heart of the matter.

Lemma 2.15 Let t ∈ A. Then |E_{t}| = |E′_{t}|.

Proof For t ∈ A let

R_{t} = {a ∈ K_{r+1} : a realises t inK^{(r+1)} },
R′_{t} = {a ∈ K_{r+1} : a realises ψ(t) in K^{(r+1)} }.

If a ∈ K_{r+1} , then a ∈ R_{t} iff tp(a/D) ⊇ t, and because tp(a/D) is by property (v) and lemma 2.11 admissible, this is iff a ∈ E_{u} for some u ∈ A with u ⊇ t. Similarly, a ∈ R′_{t}iff a ∈ E′_{u} for some u ∈ A with u ⊇ t. We obtain

R_{t} = ⋃_{t⊆u∈A} E_{u}  and  R′_{t}= ⋃_{t⊆u∈A} E′_{u},  for all t ∈ A.

As A is finite, (A,⊃) is well-founded; we now proceed by induction on it. Let t ∈ A, and assume inductively that |E_{u}| = |E′_{u}| for any u ∈ A with u ⊃ t. We show that |E_{t}| = |E′_{t}|. As the E_{u} for varying u ∈ A are pairwise disjoint, and similarly for the E′_{u}, we have

E_{t} = R_{t}\ ⋃_{t⊂u∈A} E_{u},  and  E′_{t}= R′_{t}\ ⋃_{t⊂u∈A} E′_{u}.

Obviously, |t| = |ψ(t)|, and ψ(t) is admissible (by lemma 2.8). So by construction of K^{(r+1)} , we have |R_{t}| = |R′_{t}|. With the inductive hypothesis, this gives:

|E_{t}| = |R_{t}| − ∑_{t⊂u∈A} |E_{u}| = |R′_{t}| − ∑_{t⊂u∈A} |E′_{u}| = |E′_{t}|.

This completes the induction and the proof. □

We now obtain:

Proposition 2.16 Let q be a 1–1 partial map : K_{r+1} → K_{r+1} such that ψ∪q is a partial isomorphism of K^{(r+1)} . Then ψ ∪ q extends to a partial isomorphism in Ψ^{(r+1)} .

Proof We know that the E_{t} are pairwise disjoint, as are the E′_{t}. For any type t ∈ A, lemma 2.15 shows that |E_{t}| = |E′_{t}|, and by lemma 2.14, q↾E_{t} is a partial 1–1 map : E_{t} → E′_{t}. So for each t, we may extend q↾E_{t} to a bijection : E_{t} → E′_{t}. We let q^{+} be the union of all these extensions. Since K_{r+1} = ⋃ {E_{t}: t ∈ A} = ⋃ {E′_{t}: t ∈ A}, q^{+} is a well-defined permutation of K_{r+1} . By lemma 2.14, ψ ∪ q^{+} is a partial isomorphism of K^{(r+1)} , and so ψ ∪ q^{+} ∈ Ψ^{(r+1)} . □

This has a corollary:

Corollary 2.17 Any ψ ∈ Ψ^{(r)} extends to ψ′∈ Ψ^{(r+1)} such that ν_{r+1} ψ′(a) = ψ′ν_{r+1} (a) for all a ∈ K ∩ domψ (that is, ν_{r+1} ∘ ψ′⊆ ψ′∘ ν_{r+1} ).

Proof Let ψ be as in the formulation of the corollary. Define a partial one-one map q: K_{r+1} → K_{r+1} by

q = ν_{r+1} ψν_{r+1}^{−1} .

By proposition 2.16, we need only show that ψ ∪ q is a partial isomorphism of K^{(r+1)} . For this, it suffices by lemma 2.14 to prove that for any atomic α(x,ȳ) in which x is free, and any a ∈ domq and c̄∈ domψ,

K^{(r+1)} ⊧ α(a,c̄) ↔ α(q(a),ψ(c̄)).

Well, take a′∈ K with ν_{r+1} (a′) = a. Note that a′∈ domψ. Then K^{(r+1)} ⊧ α(a,c̄) iff K^{(r+1)} ⊧ α(a′,c̄) (by property (iii)), iff K^{(r+1)} ⊧ α(ψ(a′),ψ(c̄)) (as ψ is a partial isomorphism of K^{(r+1)} ), iff K^{(r+1)} ⊧ α(ν_{r+1} ψ(a′),ψ(c̄)) (by property (iii) again), iff K^{(r+1)} ⊧ α(q(a),ψ(c̄)) (by definition of q). □

2.2.5 Proving conditions 3 and 4 of proposition 2.5

We now obtain condition 3 of proposition 2.5 for K^{(r+1)} by taking ψ in corollary 2.17 to be p ∪ ⋃ _{1≤i≤r} p_{i}, for any partial isomorphism p of K, where p_{1},...,p_{r} are given inductively. Letting ψ′be as in the corollary, we may let p_{r+1} = ψ′↾K_{r+1}.

We also obtain the last condition (condition 4) of the proposition, in the manner sketched in section 2.1.3. Let A ⊆ K^{(r+1)} be packed. We must find ψ ∈ Ψ^{(r+1)} with A ⊆ domψ and ψ(A) ⊆ \overline{K}^{(r+1)} .

If A ⊆ K^{(r)}, then by condition 4 for K^{(r)}, there is ψ ∈ Ψ^{(r)} with A ⊆ domψ and ψ(A) ⊆ \overline{K}^{(r)}; by corollary 2.17, ψ extends to ψ′∈ Ψ^{(r+1)} , and clearly, ψ′(A) ⊆ \overline{K}^{(r+1)} . We are done.

So assume that A ∩ K_{r+1} ≠ ∅. As A is packed and live tuples in K^{(r+1)} are stretched, we have A ∩ K_{r+1} = {a} for some a. Let

t = tp(a/K), and D = base t.

By property (v), t is admissible, so there are b ∈ K, E ⊆ K, and ψ ∈ Ψ^{(r)} with D ⊆ domψ and tp(b/E) = ψ(t). By restricting ψ and E, we may assume that K ∩domψ = D and E = base(tp(b/E)) = ψ(D). By property (iii), we have tp(ν_{r+1} (b)/E) = ψ(t), too. Let q be the partial map : K_{r+1} → K_{r+1} defined only on a and with q(a) = ν_{r+1} (b). Since K ∩ domψ = D, lemma 2.14(3) applies, telling that ψ ∪ q is a partial isomorphism of K^{(r+1)} . By proposition 2.16, ψ ∪ q extends to ψ′∈ Ψ^{(r+1)} (which may not commute with ν_{r+1} ).

Now A ∩ K ⊆ D. To see this, let d ∈ A ∩ K. As A is packed, there is atomic α(x,y,z̄) in which x,y occur, and b̄∈ A ∩ K^{(r)}, with K^{(r+1)} ⊧ α(a,d,b̄). Then α(x,d,b̄) ∈ t and d ∈ base t = D, as required. Hence, A \ {a} ⊆ domψ, and we may define

B = ψ(A \ {a}) ∪ {b} ⊆ K^{(r)}.

Then by property (iii), the map μψ′↾A: A → B preserves all L-relations, so B is packed. So by proposition 2.5(4) for K^{(r)}, there is ϕ ∈ Ψ^{(r)} with B ⊆ domϕ and ϕ(B) ⊆ \overline{K}^{(r)}. By corollary 2.17, ϕ extends to ϕ′∈ Ψ^{(r+1)} such that ν_{r+1} ∘ ϕ′⊆ ϕ′∘ ν_{r+1} .

Now we have ϕ′ψ′∈ Ψ^{(r+1)} , A ⊆ dom(ϕ′ψ′), and ϕ′ψ′(A) ⊆ \overline{K}^{(r+1)} . The first statement is clear. For the others, we consider elements of A in turn. First consider a. We have ϕ′ψ′(a) = ϕ′ν_{r+1} (b). Because b ∈ domϕ, we have ν_{r+1} ϕ′(b) = ϕ′ν_{r+1} (b) by choice of ϕ′. Hence, ϕ′ψ′(a) = ν_{r+1} ϕ′(b) ∈ \overline{K}^{(r+1)} . For c ∈ A \ \{a\}, we have ϕ′ψ′(c) ∈ ϕ′(B) ⊆ \overline{K}^{(r)} ⊆ \overline{K}^{(r+1)} . This completes the proof of condition 4 of proposition 2.5 for K^{(r+1)} .

We have now finished the induction on r and proved proposition 2.5. □

2.3 Proof of theorem 2.2

Proof Let K,L,r be as in the formulation of the theorem. We assume r > 0, set H = H_{r}(K) =^{def} K̂^{(r)} as in proposition 2.5, let \overline{K}be the substructure of H with domain \overline{K}^{(r)}∩ K̂^{(r)}, and let π =^{def}⋃ _{1≤i≤r} ν_{i}^{−1} : \overline{K} → K. Then π is obviously surjective. To check that it is a homomorphism, we will show a little more: that

(†) if ā∈ \overline{K}is stretched then K^{(r)} ⊧ α(ā) ↔ α(π(ā)) for all atomic α(x̄).

We may assume that ā= (a_{0},...,a_{n−1} ) with a_{j} ∈ K_{i_{j}} for each j < n, where 0 < i_{0} < i_{1} < ···< i_{n−1} ≤ r. Then for each j < n, we have ν_{i_{j}}π(a_{j}) = a_{j} and a_{0},...,a_{j−1} ,π(a_{j+1} ),...,π(a_{n−1} ) ∈ ⋃ _{l<i_{j}} K_{l}, so by proposition 2.5(2) we obtain

K^{(r)} ⊧ α(a_{0},...,a_{n−1} ) ↔ α(a_{0},...,a_{n−2} ,π(a_{n−1} )),
K^{(r)} ⊧ α(a_{0},...,a_{n−2} ,π(a_{n−1} )) ↔ α(a_{0},...,a_{n−3} ,π(a_{n−2} ),π(a_{n−1} )),
⋮
K^{(r)} ⊧ α(a_{0},π(a_{1}),...,,π(a_{n−1} )) ↔ α(π(a_{0}),...,π(a_{n−1} )),

proving (†). Now, if R ∈ L and \overline{K}⊧ R(ā) then K^{(r)} ⊧ R(ā); by proposition 2.5(1), āmust be stretched, so by (†), K^{(r)} ⊧ R(π(ā)). As K ⊆ K^{(r)}, we get K ⊧ R(π(ā)), and hence π is a homomorphism.

We check the other requirements of the theorem.

1. If p is a partial isomorphism of K, let p̂ = p_{1}∪...∪p_{r} as in proposition 2.5(3). Then p̂ ∈ AutH. Let a ∈ \overline{K}with π(a) ∈ domp. We require pπ(a) = πp̂(a). Say, a ∈ K_{i} (some i, 1 ≤ i ≤ r). Then by the proposition again, ν_{i}pπ(a) = p̂ν_{i}(π(a)) = p̂(a). Since ν_{i} is one-one, pπ(a) = ν_{i}^{−1} p̂(a) = πp̂(a).

2. This is immediate from proposition 2.5(4).

3. Take a universal formula θ(x̄) = ∀ȳφ(x̄,ȳ), where φ is quantifier-free, x̄ȳis non-repeating, |x̄| = n, |ȳ| = m, say, and n + m ≤ r. Take ā= (a_{0},...,a_{n−1} ) ∈ \overline{K} with rng(ā) contained in a packed subset of K̂^{(r)} and such that π↾rng(ā) is one-one, and with \overline{K} ⊧ θ(ā). Write b̄ for π(ā), so b_{i} = π(a_{i}) for i < n. We show K ⊧ θ(b̄).

Let c̄= (c_{0},...,c_{m−1}) ∈ K be any m-tuple; we require K ⊧ φ(b̄,c̄). Choose 1 ≤ l_{0},...,l_{m−1} ≤ r satisfying, for all i,j < m and k < n:

• if c_{i} = b_{k} then a_{k} ∈ K_{l_{i}},

• if c_{i} ∉ rng(b̄) then K_{l_{i}} ∩ rng(ā) = ∅,

• if c_{i} = c_{j} then l_{i} = l_{j},

• if c_{i} ≠ c_{j} and c_{i},c_{j} ∉ rng(b̄) then l_{i} ≠ l_{j}.

This is possible since π↾rng(ā)is one-one and n+m ≤ r. Let d_{i} = ν_{l_{i}}(c_{i}) for i < m, and d̄= (d_{0}, ...,d_{m−1}).

Claim. The map π↾rng(ād̄)preserves all quantifier-free formulas.

Proof of claim. Because π is one-one on rng(ā), by choice of the l_{i} it is one-one on rng(ād̄) too, so preserves all equalities and inequalities. Further, because ā is contained in a packed subset of K̂^{(r)}, it is stretched in K^{(r)}; by choice of the l_{i}, it follows that ād̄is also stretched. By (†) above, π↾rng(ād̄)preserves all atomic relations in both directions. This proves the claim.

But \overline{K} ⊧ θ(ā), so \overline{K} ⊧ φ(ā,d̄). Since φ is quantifier-free, and by definition π(ād̄) = b̄c̄, the claim gives K ⊧ φ(b̄,c̄), as required.

This completes the proof of theorem 2.2. □

3 Loosely guarded and packed fragments

Here we apply the combinatorics of section 2, together with some simple, tedious syntactic manipulations, to prove the finite model property for the loosely guarded and packed fragments. Convention 2.4 is no longer in force, so that ‘atomic’ formulas may be equalities; but notations φ(x̄) still indicate by default that x̄is non-repeating and contains the free variables of φ.

3.1 The loosely guarded and packed fragments

We begin by recalling the definition of the loosely guarded fragment.

Definition 3.1 (van Benthem, [24, p. 9]) Let L be a signature without function symbols. The loosely guarded fragment LGF(L) over L consists of (just) the following kinds of L-formula:

• Any atomic L-formula is in LGF(L).

• LGF(L) is closed under Boolean combinations.

• If

– γ (the ‘guard’) is a conjunction of atomic L-formulas,^{1}

– φ ∈ LGF(L),

– every free variable of φ is free in γ,

– ȳis a tuple of free variables of γ,

– if x is a free variable of γ, y is a variable from ȳ, and x ≠ y,^{2} then there is a conjunct of γ in which x,y both occur,

then ∃ȳ(γ ∧ φ) ∈ LGF(L).

Note that γ may have more free variables than φ, and more than two variables may be ‘guarded’ by a single conjunct of γ. The reader may check that the standard translation of U(p,q) (formula (2) of section 1) is loosely guarded.

We will also prove the finite model property for the ‘packed fragment’.

Definition 3.2 (Marx, [19]) Let L be a signature without function symbols. An L-formula γ is said to be a packing guard if γ is a conjunction of atomic and existentially-quantified atomic formulas such that for any distinct free variables x,y of γ, there is a conjunct of γ in which x,y both occur free.

The packed fragment PF(L) consists of (just) the following formulas:

• Any atomic L-formula is in PF(L).

• PF(L) is closed under boolean combinations.

• If the L-formula γ is a packing guard, φ ∈ PF(L), every free variable of φ is free in γ, and ȳis a tuple of free variables of γ, then ∃ȳ(γ ∧ φ) ∈ PF(L).^{3}

LGF(L) is not a subfragment of PF(L) because guards γ of PF(L) must bind every pair of free variables of φ. For example, the standard translation of U(p,q) (formula (2) of section 1) is loosely guarded but not packed. However, as we will see in lemma 3.9, every LGF(L)-sentence is equivalent to a sentence of PF(L). An example, due to Marx, of a packed sentence which is not equivalent to a loosely guarded sentence is ∃xyz(∃wR(x,y,w) ∧ ∃wR(x,z,w) ∧ ∃wR(z,y,w) ∧ ¬R(x,y,z)).

Note that if γ is a quantifier-free packing guard with free variables precisely x_{0},...,x_{n−1} , M is an L-structure, a_{0},...,a_{n−1} ∈ M, and M ⊧ γ(a_{0},...,a_{n−1} ), then {a_{0},...,a_{n−1} } is packed in M.

1The original definition [24] did not allow equalities in guards, but their presence does not affect the expressive power or the finite model property so we include them.

2[5, definition 2.2] omits the restriction x ≠ y; this does not reduce the expressive power if equalities are allowed as conjuncts of γ.

3[19] requires that γ and φ have exactly the same free variables. We do not need this restriction, but adding it does not reduce the expressive power since we may add conjuncts x = x to φ until its free variables are the same as γ’s. Also, [19] does not allow existentially-quantified equalities in guards, and not all variables in ȳneed be free in γ; it is plain that these differences do not change the expressive power either.

Packed subformulas It is convenient to introduce the notion of packed subformula of a formula φ ∈ PF(L). This is done by induction on the construction of φ. If φ is atomic then φ is a packed subformula of itself. The packed subformulas of a boolean combination φ of formulas in PF(L) are φ and the packed subformulas of the combinants. And if φ ∈ PF(L) and γ is a packing guard, then the packed subformulas of ∃ȳ(γ ∧ φ) are itself and those of φ.

3.2 Finite model property

In section 3.3 we will prove:

Theorem 3.3 For any relational signature L, the packed fragment PF(L) has the finite model property.

This easily gives the following, which will be proved in section 3.4:

Corollary 3.4 For any relational signature L, the loosely guarded fragment LGF(L) has the finite model property.

Remark 3.5 It is not hard to see that we can add constants to L and keep the finite model property for PF(L) and LGF(L). (Note that guards need not guard constants, so, e.g., ∀x(x = x → R(c,x)) is a loosely guarded sentence.) However, the loosely guarded fragment in signatures with function symbols is undecidable (this follows from results in [20]) and therefore does not have the finite model property.

3.3 Proof of the finite model property for the packed fragment

To prove theorem 3.3, it clearly suffices to show that for any finite relational signature L, any sentence of PF(L) with a model has a finite model. Fix such an L. The proof proceeds in two stages: first, for sentences with only quantifier-free packing guards, and then for arbitrary sentences. The first stage is done in two lemmas: first, assuming that the sentence has an irreflexive model, and then the general case.

Definition 3.6 An L-structure M is said to be irreflexive if whenever R ∈ L, a_{1},...,a_{n} ∈ M, and M ⊧ R(a_{1},...,a_{n}), then a_{1},...,a_{n} are distinct.

Lemma 3.7 Suppose that σ ∈ PF(L), all guards in σ are quantifier-free, and σ has an irreflexive model M. Then σ has a finite model.

Proof Assume the hypotheses. Let σ be written with variables v_{0},...,v_{r−1} only, where 0 < r < ω, and write v̄for (v_{0},...,v_{r−1} ). For any formula φ written with variables v̄, and any r-tuple ā∈ M, we will write M ⊧ φ(ā) to mean that φ is true in M when v_{i} is assigned to a_{i} for each i < r.

Introduce a new r-ary relation symbol R_{φ} for each packed subformula φ of σ, and define an expansion M^{+} of M by interpreting each R_{φ} equivalently in M to φ:

M^{+} ⊧ R_{φ}(a_{0},...,a_{r−1} ) ⟺ M ⊧ φ(a_{0},...,a_{r−1} ),

for any a_{0},...,a_{r−1} ∈ M. Of course, if some v_{i} is not free in φ then we can change a_{i} without changing the truth of φ or R_{φ}; and if φ is a sentence then R_{φ} will hold for all r-tuples in M, or for none. M^{+} is in general not irreflexive. Take a finite substructure K ⊆ M^{+} containing an isomorphic copy of every substructure A ⊆ M^{+} with |A| ≤ 2r. Let H = H_{r}(K), \overline{K}, and π be as in theorem 2.2. K,\overline{K},H are finite structures in the expanded language. We will show that H ⊧ σ.

Claim. For every packed subformula φ of σ and any r-tuple ā∈ H that is packed in the L-reduct H↾L of H, we have H ⊧ R_{φ}(ā) ↔ φ(ā). Proof of claim. First note that because āis packed in H↾L and hence in H, by theorem 2.2(2) there is g ∈ AutH with g(ā) ∈ \overline{K}. Since automorphisms preserve all first-order formulas, we may assume that ā∈ \overline{K}. Next, note that because M is irreflexive and π is a homomorphism, if ā∈ \overline{K} is packed in H↾Lthen π↾rng(ā)is one-one. So by theorem 2.2(3), π↾rng(ā)preserves forwards all ‘small’ prenex universal formulas, and all quantifier-free formulas.

We prove the claim by induction on φ. For atomic φ it is clear, since K ⊧ φ(π(ā)) ↔ R_{φ}(π(ā)) and π↾rng(ā) preserves quantifier-free formulas. For conjunction, inductively assume the claim for θ,φ, and let ā∈ \overline{K}be packed in H↾L. Then inductively, H ⊧ (θ∧φ)(ā) iff H ⊧ R_{θ}(ā)∧R_{φ}(ā). Since π↾rng(ā) preserves quantifier-free formulas, this is iff M^{+} ⊧ R_{θ}(π(ā)) ∧ R_{φ}(π(ā)). By definition of M^{+} this is iff M ⊧ (θ ∧ φ)(π(ā)), iff M^{+} ⊧ R_{θ∧φ} (π(ā)). Again using preservation, this is iff H ⊧ R_{θ∧φ} (ā), as required. Negation is handled similarly.

Now consider the case θ(x̄) = ∃ȳ(γ(x̄,ȳ)∧φ(x̄,ȳ)), where φ ∈ PF(L), γ is a quantifier-free packing guard, x̄,x̄ȳare non-repeating tuples of variables from v̄enumerating the free variables of θ,γ respectively, and ȳis non-empty. Let z̄enumerate the variables of v̄that are not in x̄ȳ, if any, and let y be any variable in ȳ. We will use the following notation: if w̄ = (v_{i_{0}},...,v_{i_{k−1}}) is a tuple of variables from v̄= (v_{0},...,v_{r−1} ), and ā= (a_{0},...,a_{r−1} ) is any r-tuple, we write āw̄ for the tuple (a_{i_{0}},...,a_{i_{k−1}}), corresponding to āas w̄does to v̄. Similarly, we write ā_{v_{i}} for a_{i}.

Let ā∈ \overline{K}be packed in H↾L, and inductively assume the claim for φ.

⇒ First assume that H ⊧ R_{θ}(ā); we show H ⊧ θ(ā). Write b̄ for π(ā). As π is a homomorphism, M^{+} ⊧ R_{θ}(b̄). By definition of R_{θ} in M^{+} , M ⊧ θ(b̄), so there is an r-tuple c̄∈ M with c̄x̄= b̄x̄ and M ⊧ (γ ∧ φ)(c̄), and thus, M^{+} ⊧ γ(c̄) ∧ R_{φ}(c̄). Since the variables of z̄are not free in γ ∧ φ, we may assume that each element of c̄z̄is equal to c̄_{y}.

As |rng(b̄c̄)| ≤ 2r, there is b̄′c̄′∈ K isomorphic to b̄c̄. As γ,R_{φ} are quantifier-free, K ⊧ γ(c̄′) ∧ R_{φ}(c̄′). Let χ(x̄) be the prenex existential formula

∃ȳz̄( γ ∧ ( ⋀_{z in z̄}z = y) ∧ R_{φ}(v_{0},...,v_{r−1} )) .

Then clearly, K ⊧ χ(b̄′ ; x̄).

Let p : b̄ ↦ b̄′, a partial isomorphism of K, and take p̂ ∈ AutH satisfying the provisions of theorem 2.2(1). Letting ā′= p̂(ā), it is clear that ā′is packed in H↾L and so π↾rngā′is oneone, and π(ā′) = b̄′. Since |x̄ȳz̄| ≤ r, by theorem 2.2(3) π↾rngā′ ; x̄ preserves ¬χ forwards, and hence \overline{K} ⊧ χ(ā′ ; x̄). As \overline{K} ⊆ H and χ is existential, H ⊧ χ(ā′ ; x̄). As p̂ ∈ AutH and p̂(ā) = ā′, H ⊧ χ(āx̄). So there is an r-tuple d̄∈ H with d̄x̄= āx̄, each element of d̄z̄equal to d̄_{y}, and with H ⊧ γ(d̄) ∧ R_{φ}(d̄). By the form of γ and because rng(d̄) = rng(d̄x̄ ; ȳ), d̄is packed in H↾L,^{4} so inductively, H ⊧ γ(d̄) ∧ φ(d̄). Thus, H ⊧ θ(ā) by definition of θ.

⇐ Conversely, suppose that H ⊧ θ(ā); we require H ⊧ R_{θ}(ā). There is an r-tuple b̄ ∈ H with b̄x̄= āx̄and H ⊧ (γ∧φ)(b̄). As before, we may assume that each element of b̄z̄is equal to b̄_{y}. By the form of γ, b̄is packed in H↾L(see footnote 4), and hence in H. So by theorem 2.2(2) there is g ∈ AutH with g(b̄) ∈ \overline{K}. Write c̄for g(b̄). Inductively, H ⊧ γ(b̄)∧R_{φ}(b̄), so H ⊧ γ(c̄)∧R_{φ}(c̄). Writing d̄= π(c̄), because π is a homomorphism we have M^{+} ⊧ γ(d̄)∧R_{φ}(d̄). By definition of relations in M^{+} , we have M ⊧ φ(d̄). Hence, certainly, M ⊧ θ(d̄), so M^{+} ⊧ R_{θ}(d̄) by definition of M^{+} .

4This fails in the loosely guarded fragment, which is why we use the packed fragment with quantifier-free packing guards.

There are now two cases. If θ is a sentence, then every r-tuple is related by R_{θ} in M^{+} . In particular, K ⊧ R_{θ}(π(ā)). By theorem 2.2(3), \overline{K}⊧ R_{θ}(ā), and so H ⊧ R_{θ}(ā) as required.

Assume otherwise, so x̄is non-empty. Choose x in x̄; for any r-tuple w̄, write w̄′for the r-tuple given by w̄′ ; x̄= w̄x̄, and w̄′_{u}= w̄_{x}for every u in ȳz̄. Note that

(∗) \overline{K}⊧ R_{θ}(m̄) ↔ R_{θ}(m̄′) for any r-tuple m̄∈ \overline{K}that is packed in H↾L.

(∗) follows because m̄is packed so π↾rng(m̄) preserves the formula R_{θ}(v̄) ↔ R_{θ}(v̄′), and K ⊧ ∀v̄(R_{θ}(v̄) ↔ R_{θ}(v̄′)) because v̄,v̄′agree on the free variables of θ.

We know M^{+} ⊧ R_{θ}(d̄), and as c̄is certainly packed in H↾L, we obtain \overline{K}⊧ R_{θ}(c̄). By (∗), \overline{K}⊧ R_{θ}(c̄′). As g ∈ AutH and (clearly) g(ā′) = c̄′, we have \overline{K}⊧ R_{θ}(ā′). By (∗) again, \overline{K}⊧ R_{θ}(ā), so H ⊧ R_{θ}(ā) as required. This proves the claim.

Take any packed r-tuple ā∈ \overline{K} (for example, a tuple of equal elements). Since M ⊧ σ, we have M ⊧ R_{σ}(π(ā)). We now obtain H ⊧ R_{σ}(ā) by theorem 2.2(3), and thus, by the claim, H ⊧ σ. We have found a finite model of σ, completing the proof of the lemma. □

Lemma 3.8 Let σ be a sentence of PF(L) with only quantifier-free guards, and suppose that σ has a model, say M. Then σ has a finite model.

Proof We make M into an irreflexive structure, adjust σ accordingly, and apply the preceding lemma. This will show that σ has a finite model.

For each n-ary R ∈ L and each equivalence relation ε on n, with k equivalence classes, say, introduce a new k-ary relation symbol R_{ε}, and define an expansion M^{♯} of M interpreting the new symbols as follows. Let 0 = e_{0} < e_{1} < ··· e_{k−1} < n be representatives of the ε-classes, each being minimal in its ε-class. We call the e_{i} the canonical representatives of ε. For distinct elements b_{0},...,b_{k−1} ∈ M, define a_{0},...,a_{n−1} ∈ M by a_{i} = b_{j} iff i ε e_{j}, for each i < n, j < k, and define

M^{♯}⊧ R_{ε}(b_{0},...,b_{k−1}) iff M ⊧ R(a_{0},...,a_{n−1} ).

For example, if n = 5 and the ε-classes are {0,2},{1,3},{4}, then e_{0} = 0, e_{1} = 1, e_{2} = 4, and if a,b,c ∈ M are distinct, we define M^{♯}⊧ R_{ε}(a,b,c) iff M ⊧ R(a,b,a,b,c).

Write M^{≠} for the reduct of M^{♯}to the new relation symbols R_{ε} (for all n-ary R ∈ L and equivalence relations ε on n). Then M^{≠} is irreflexive.

Write E_{n} for the set of all equivalence relations on n. For each atomic L-formula of the form R(x̄), for n-ary R ∈ L and any n-tuple x̄= (x_{0},...,x_{n−1} ) of variables, perhaps with repetitions, and for ε ∈ E_{n} with canonical representatives e_{0},...,e_{k−1}, define R(x̄)^{ε} to be the following formula, with the same free variables x̄:

( ⋀_{iεj} x_{i} = x_{j}) ∧ ⋀ {R_{ε}(x_{i_{0}},...,x_{i_{k−1}}) : i_{0},...,i_{k−1} < n, i_{l} ε e_{l} for each l < k}.

Now define R(x̄)^{≠} = ⋁ _{ε∈E_{n}} R(x̄)^{ε}. Observe that for any h: {x_{0},...,x_{n−1} } → M, if h(x_{i}) = a_{i} (i < n), ā= (a_{0},...,a_{n−1} ), and η ∈ E_{n} is defined by i η j iff a_{i} = a_{j}, then M^{♯} ⊧ R(ā) ↔ R(x̄)^{η}(ā). (That is, R(x̄) ↔ R(x̄)^{η} is true in M^{♯}under assignment h.) Also, for any ε ∈ E_{n}, if M^{≠} ⊧ R(x̄)^{ε}(ā) then because M^{≠} is irreflexive, ε = η. Hence, M^{♯}⊧ ∀x̄(R(x̄) ↔ R(x̄)^{≠} ).

For any formula φ ∈ PF(L) with quantifier-free guards, let φ^{≠} be obtained from φ by replacing every atomic subformula R(x̄) of φ (for R ∈ L) by R(x̄)^{≠} — this includes both packed subformulas and formulas occurring in guards.

Claim. φ^{≠} is logically equivalent to a packed formula with quantifier-free guards. Proof of claim. This can be seen by induction on φ. We sketch the argument. The case of atomic φ is easy, as are the boolean cases. For formulas ∃ȳ(γ(x̄,ȳ) ∧ φ(x̄,ȳ)), we observe that for each R ∈ L and any x̄, every pair of free variables of R(x̄) also occur free in some conjunct of each disjunct R(x̄)^{ε} of R(x̄)^{≠} . Hence, by distributing the conjunctions from γ over the disjunctions in the R(x̄)^{≠} , we see that γ^{≠} (x̄,ȳ) can be put in disjunctive normal form ⋁ _{i}γ_{i}(x̄,ȳ) such that each pair of distinct variables of x̄ȳoccurs in a conjunct of each γ_{i}. So ∃ȳ(γ(x̄,ȳ) ∧ φ(x̄,ȳ))^{≠} is equivalent to ⋁ _{i}∃ȳ(γ_{i}(x̄,ȳ) ∧ φ(x̄,ȳ)^{≠} ), which inductively is equivalent to a packed formula with quantifier-free guards. This proves the claim.

We can now rapidly conclude the proof. Since for all R, R(x̄) and R(x̄)^{≠} are equivalent in M^{♯}, and M ⊧ σ, we have M^{≠} ⊧ σ^{≠} . As M^{≠} is irreflexive, by the claim and lemma 3.7 there is a finite model N ⊧ σ^{≠} . Now make N an L-structure N^{♯} by interpreting each R(x̄) as R(x̄)^{≠} . More formally, for n-ary R ∈ L, take an n-tuple ȳof distinct variables and let N^{♯}⊧ R(ā) iff N ⊧ R(ȳ)^{≠} (ā), for any n-tuple ā∈ N. It is easily checked that if x̄ is any n-tuple of variables, then N^{♯} ⊧ ∀x̄(R(x̄) ↔ R(x̄)^{≠} ). So clearly, N^{♯}⊧ σ. □

We can now prove theorem 3.3.

Proof Let σ be a sentence of PF(L), and let M be a model of σ. For each existential conjunct β(z̄) = ∃v̄α(z̄,v̄) of each guard in σ, where α(z̄,v̄) is atomic with free variables just those in z̄v̄, introduce a new |z̄|-ary relation symbol R_{β(z̄)} and interpret it in M in the same way as β(z̄): i.e., let M ⊧ R_{β(z̄)}(ā) iff M ⊧ β(ā), for all ā∈ M of length |z̄|. We continue to write M for this definitional expansion. Notice that M ⊧ χ_{β(z̄)}, where

χ_{β(z̄)} = ∀z̄(R_{β(z̄)}(z̄) → ∃v̄(α(z̄,v̄) ∧ ⊤)) ∧ ∀z̄v̄(α(z̄,v̄) → R_{β(z̄)}(z̄)).

Of course, χ_{β(z̄)} is logically equivalent to ∀z̄(R_{β(z̄)}(z̄) ↔ β(z̄)), but we write it in the above form to obtain a sentence of the packed fragment with quantifier-free guards. Let σ′be the result of replacing each existential conjunct β(z̄) of each guard of each subformula of σ by R_{β(z̄)}(z̄). Let σ′′be the conjunction of σ′ and all the sentences χ_{β(z̄)}, for each existential conjunct β(z̄) of each guard in σ. Then σ′′is a sentence of the packed fragment with only quantifier-free guards, and M ⊧ σ′′.

By lemma 3.8, there is a finite model N ⊧ σ′′. For each β as above, N ⊧ χ_{β(z̄)}, so R_{β(z̄)}(z̄) is equivalent in N to β(z̄). So it is clear that N ⊧ σ. □

3.4 Finite model property for the loosely guarded fragment

We can easily derive this from the finite model property for the packed fragment.

Lemma 3.9 Let L be a relational signature, let the L-formula δ be a packing guard (definition 3.2) with free variables precisely v̄, and let φ(v̄) ∈ LGF(L). Then δ ∧ φ is logically equivalent to δ ∧ φ′for some formula φ′(v̄) ∈ PF(L).

Proof By induction on φ. If φ is atomic, we let φ′= φ. Assuming the result for φ,ψ, we let (¬φ)′= ¬φ′ and (φ ∧ ψ)′= φ′∧ ψ′, as usual. Then δ ∧ ¬φ is equivalent to δ ∧ ¬(δ ∧ φ), which is equivalent to δ ∧ ¬(δ ∧ φ′) and to δ ∧ ¬φ′= δ ∧ (¬φ)′; the case of ∧ is similar.

Finally let φ(x̄) = ∃ȳ(γ(x̄,ȳ) ∧ ψ(x̄,ȳ)) be a loosely guarded L-formula, where the free variables of γ are precisely x̄ȳ, and rng(x̄) ⊆ rng(v̄). Assume the result for ψ, and consider δ(v̄) ∧ φ(x̄). For each pair of distinct variables x,x′from x̄, pick a conjunct χ_{x,x′}(x,x′,z̄) of δ in which they both occur free, and let χ_{x,x′}^{∘}(x,x′) = ∃z̄χ_{x,x′}. Let δ^{∘}(x̄) = ⋀ _{x,x′}χ_{x,x′}^{∘}. Then δ ⊢ δ^{∘}, and δ ∧ φ is equivalent to δ ∧ ∃ȳ(γ(x̄,ȳ) ∧ δ^{∘}(x̄) ∧ ψ(x̄,ȳ)). Now γ ∧ δ^{∘} is a packing guard with free variables x̄ȳ, so inductively, γ ∧ δ^{∘} ∧ ψ(x̄,ȳ) is equivalent to γ ∧ δ^{∘} ∧ ψ′ for some ψ′(x̄,ȳ) ∈ PF(L). Then δ ∧ φ is equivalent to δ ∧ ∃ȳ(γ ∧ δ^{∘}∧ ψ′); the second conjunct here is in PF(L) and its free variables are all from v̄. □

Proof of corollary 3.4 It is immediate from the lemma that any sentence of LGF(L) is logically equivalent to a sentence of PF(L). The corollary now follows from theorem 3.3. □

4 Applications

We end by outlining some applications of our results.

4.1 Decidable fragments of predicate temporal logic

In [14], certain decidable fragments of predicate temporal logic with Until and Since (the ‘monodic’ fragments) were introduced. The idea is to restrict the predicate part of the logic to a known decidable fragment of first-order logic (such as the loosely guarded fragment) and restrict temporal operations to formulas with at most one free variable. Monodic fragments are decidable over a wide range of linear flows of time. Moreover, if it is decidable whether a sentence of the chosen first-order fragment (roughly speaking) has a finite model, the corresponding monodic temporal logic with finite domains is also decidable.

Since the loosely guarded fragment is decidable and has the finite model property, it is decidable whether a sentence of the loosely guarded fragment has a finite model, and thus the loosely guarded monodic fragment of predicate temporal logic and finite domains is decidable.

4.2 Finite base property in algebraic logic

The ‘finite algebra on finite base property’ for weakly associative algebras [17] follows easily from the finite model property for the loosely guarded fragment. Let A = (A,+,−,0,1,1,,˘ ,;) be a finite weakly associative algebra. Regard each a ∈ A as a binary relation symbol. Then a relativised representation of A is a model of the following theory:

∀xy[1,(x,y) ↔ x = y]
∀xy[r(x,y) ↔ s(x,y) ∨ t(x,y)] for each r,s,t ∈ A with r = s + t
∀xy[1(x,y) → (r(x,y) ↔ ¬s(x,y))] for each r,s ∈ A with r = −s
∀xy[r(x,y) ↔ s(y,x)] for each r,s ∈ A with r = s̆
∀xy[1(x,y) → (r(x,y) ↔ ∃z(s(x,z) ∧ t(z,y)))] for each r,s,t ∈ A with r = s;t
∃xy r(x,y) for each r ∈ A with r ≠ 0.

Every weakly associative algebra has a relativised representation [17].

It is easily seen that the conjunction of the above theory can be written as a loosely guarded sentence. Thus, by corollary 3.4, any finite weakly associative algebra has a finite relativised representation. One may also show in much the same way that WA has the finite base property: any universal sentence true in every finite weakly associative algebra is true in all weakly associative algebras. (These results were proved in [1].)

Various related results can also be derived. For example, similar arguments will show that for finite n ≥ 3, any finite relation algebra in RA_{n} has a finite n-square relativised representation, and that if n ≥ 4, any subalgebra of the relation algebra reduct of a finite n-dimensional cylindric algebra has a finite n-flat relativised representation. For definitions of these terms, see [12, 11]; these results solve open problems stated there.

4.3 Finite model property for arrow logic in relativised interpretation

Arrow logic is the logical counterpart of relation algebra, and fits into the paradigm of dynamic logic: see [23] for more information. Formulas of arrow logic can be given relativised semantics, corresponding to weakly associative algebras. It is immediate from the finite base property for WA (above) that any formula of arrow logic with a relativised model has a finite relativised model.

References

[1] H Andréka, I Hodkinson, and I Németi, Finite algebras of relations are representable on finite sets, J. Symbolic Logic 64 (1999), 243–267.

[2] H Andréka, J van Benthem, and I Németi, Modal logics and bounded fragments of predicate logic, J. Philosophical Logic 27 (1998), 217–274.

[3] C. Areces, C. Monz, H. de Nivelle, and M. de Rijke, The guarded fragment: Ins and outs, JFAK (J. Gerbrandy, M. Marx, M. de Rijke, and Y. Venema, eds.), Vossiuspers, AUP, Amsterdam, 1999, Essays Dedicated to Johan van Benthem on the Occasion of his 50th Birthday.

[4] D M Gabbay, Expressive functional completeness in tense logic (preliminary report), Aspects of Philosophical Logic (U Monnich, ed.), Reidel, Dordrecht, 1981, pp. 91–117.

[5] E Grädel, On the restraining power of guards, J. Symbolic Logic 64 (1999), 1719–1742.

[6] M Grohe, Arity hierarchies, Ann. Pure Appl. Logic 82 (1996), 103–163.

[7] B. Herwig, Extending partial isomorphisms on finite structures, Combinatorica 15 (1995), 365–371.

[8] , Extending partial isomorphisms for the small index property of many ω–categorical structures, Israel J. Math. 107 (1998), 93–124.

[9] B. Herwig and D. Lascar, Extending partial isomorphisms and the profinite topology on the free groups, Trans. Amer. Math. Soc. 352 (2000), 1985–2021.

[10] C Hirsch and S Tobies, A tableau algorithm for the clique guarded fragment, Tech. Report LTCS-Report 00-03, Aachen University of Technology, 2000. See http://www-lti.informatik.

rwth-aachen.de/Forschung/Reports.html.

[11] R Hirsch and I Hodkinson, Relation algebras from cylindric algebras, I, Ann. Pure Appl. Logic, provisionally accepted.

[12] , Relation algebras with n-dimensional relational bases, Ann. Pure Appl. Logic 101 (2000), 227– 274.

[13] R Hirsch, I Hodkinson, M Marx, Sz Mikulás, and M Reynolds, Mosaics and step-by-step, Logic at Work (E. Or�owska, ed.), Studies in Fuzziness and Soft Computing, vol. 24, Physica-Verlag, Heidelberg/New York, 1998, Appendix to ‘A Modal Logic of Relations’ by Y Venema and M Marx, pp. 158–167.

[14] I Hodkinson, F Wolter, and M Zakharyaschev, Decidable fragments of first-order temporal logics, Ann. Pure Appl. Logic, to appear.

[15] E Hrushovski, Extending partial isomorphisms of graphs, Combinatorica 12 (1992), 411–416.

[16] J A W Kamp, Tense logic and the theory of linear order, Ph.D. thesis, University of California, Los Angeles, 1968.

[17] R Maddux, Some varieties containing relation algebras, Trans. Amer. Math. Soc. 272 (1982), 501–526.

[18] M Marx, Complexity of modal logics of relations, preprint, 1997. Available at

     http://www.wins.uva.nl/research/illc/Publications/ResearchReports/ML-1997-02.text.ps.gz

[19] , Tolerance logic, Tech. Report IR–469, Vrije Universiteit, Amsterdam, 1999, to appear in J.

     Logic, Language and Information. Available at http://www.wins.uva.nl/~marx/pub/tolerance.ps.gz

[20] Sz Mikulás and M Marx, Undecidable relativizations of algebras of relations, J. Symbolic Logic 64 (1999), 747–760.

[21] J K Truss, Generic automorphisms of homogeneous structures, Proc. London Math. Soc. 64 (1992), 121– 141.

[22] J van Benthem, Modal correspondence theory, Ph.D. thesis, Mathematical Institute, University of Amsterdam, 1976.

[23] , Exploring logical dynamics, Studies in Logic, Language and Information, CSLI Publications & FoLLI, Stanford, 1996.

[24] , Dynamic bits and pieces, Tech. Report LP-97-01, ILLC, University of Amsterdam, 1997. Avail-

     able at http://preprint.beta.uva.nl/server/bp search.show doc?p srvr id=3&p doc id=468

[25] , Modal logic and classical logic, Bibliopolis, Naples, 1985.

[26] M Vardi, Why is modal logic so robustly decidable?, Descriptive complexity and finite models, Amer. Math. Soc., Providence, RI, 1996, pp. 149–183.