Beth definability in the Guarded Fragment

Eva Hoogland, Maarten Marx and Martin Otto

May 10, 1999

Abstract

The guarded fragment (GF) was introduced in [1] as a fragment of first order logic which combines a great expressive power with nice modal behavior. It consists of relational first order formulas whose quantifiers are relativized by atoms in a certain way. While GF has been established as a particularly well-behaved fragment of first order logic in many respects, interpolation fails in restriction to GF, [9]. In this paper we consider the Beth property of first order logic and show that, despite the failure of interpolation, it is retained in restriction to GF. The Beth property for GF is here established on the basis of a limited form of interpolation, which more closely resembles the interpolation property that is usually studied in modal logics. ¿From this we obtain that, more specifically, even every n-variable guarded fragment with up to nary relations has the Beth property.

Contents

1 Introduction 2

2 Preliminaries 4 2.1 Defining the guarded fragment: Syntax . . . . . . . . . . . . . . . 5 2.2 Semantic characterization of the guarded fragment . . . . . . . . 6

3 Interpolation for the guarded fragment 7

4 The Beth theorem for GF 11

1 Introduction

The Guarded Fragment It has proven useful to view modal logics not only as systems in themselves but also as fragments of first order logic. As is wellknown, the basic modal logic K can be seen as a fragment of first order logic via the translation t which maps a proposition letter p to the atom P x, which commutes with the Boolean connectives, and which maps formulas of the form ◇φ to ∃y(Rxy ∧ φ^{t}(y)) and □φ to ∀y(Rxy → φ^{t}(y)). The image of K under this translation is referred to as the modal fragment. This fragment turns out to behave excellently. It shares several nice model-theoretic properties with full first order logic (e.g., interpolation, Beth definability or the Łos-Tarski property), and has in addition good algorithmic qualities: it is decidable and every satisfiable modal formula has a finite model and a tree model (in other words, the modal fragment has the finite model property and the tree model property). Moreover, the decidability of this fragment is robust in the sense that various extensions remain decidable. For example, adding features like counting quantifiers or fixed points to the modal fragment does not affect decidability.

The usefulness of the modal fragment brought logicians to search for generalizations of this fragment which retain the afore-mentioned nice properties. An obvious candidate of such a generalization is the two variable fragment of first order logic, denoted by L_{2}. Although this logic is decidable and has the finite model property, it does not have interpolation nor the Beth property. Neither does it have the tree model property, and also its decidability is not as robust as the modal fragment.

In [1] it is argued that the distinguishing characteristic of the modal fragment is not its restriction to two variables but its restriction on occurrences of quantifiers (nl. to quantifier patterns ∃y(Rxy ∧ φ(y)) or ∀y(Rxy → φ(y))). This brings Andréka, van Benthem and Németi to investigate to what extent these quantifier restrictions can be loosened while retaining the attractive modal behavior. The outcome is the guarded fragment (GF) which allows for quantifications of the form ∃ȳ(Rx̄ȳ ∧ φ(x̄, ȳ)) and ∀ȳ(Rx̄ȳ → φ(x̄, ȳ)), where x̄, ȳ are finite sequences of variables in any order or multiplicity and φ is a guarded formula containing variables from x̄, ȳ which all appear in the atomic formula Rx̄ȳ.

In [1] this fragment is shown to have the finite model property, the Łos-Tarski property and, most importantly, to be decidable. Grädel [3] improves on this result by classifying the satisfiability problem for GF to be complete for deterministic double exponential time; satisfiability for the finite variable guarded fragments is even in Exptime, in fact Exptime-complete. This is worth comparing with the satisfiability problem for L_{2} which is known to be Nexptime-complete (cf. [5]). What is more, GF has a certain tree model property. Since the tree model property of the modal fragment can be seen as the main reason behind the robustness of the decidability of that fragment (cf. e.g., [16]), this gives hope as to the robustness of GF. And indeed, adding least and greatest fixed points to GF yields a decidable extension ([6]).

However, as shown in [9], the interpolation theorem of first order logic fails for GF. In the present paper it will be shown that GF does have an alternative interpolation property that closely resembles the interpolation property usually studied in modal logics. This result turns out to be strong enough to entail the Beth definability theorem for GF.

The Beth (definability) property In a slogan, the Beth definability property states that implicit definability equals explicit definability. Generally, this property may be regarded as an indication that there is a good balance between syntax and semantics of a logic: the semantic phenomenon that the meaning of a basic relation is implicitly determined, guarantees that there is an explicit syntactic expression for that relation. Let us go somewhat more into this. Intuitively, an implicit definition of a relation R is a definition of R (in the sense that it fixes the interpretation of R) in which the relation symbol R may occur. For example, consider the conjunction Σ of formulas saying that “< is an irreflexive linear order”, “there exists a first element and this element has property R”, and “an element has property R iff its successor does not have property R”. Note that these statements can be formulated in first order logic (with equality) using the predicates < and R. It is obvious that on every finite irreflexive linear order the interpretation of the relation R is fixed. In other words, on finite models, Σ implicitly defines R. On the other hand, as first observed by [7], there is no first order formula θ(x) which does not mention R and which would explicitly define R over the finite models of Σ. I.e., there is no formula θ(x) using just < such that Σ ⊧ Rx ↔ θ(x) would be true over all finite models. Obviously, every relation that is explicitly definable is also implicitly definable. As the above example showed, the converse is in general not true. However, in the classical context of not necessarily finite models, implicit definability and explicit definability in first order logic coincide. This property of first order logic has first been observed by E.W. Beth (see Beth (1953)). Nowadays, logics for which an analogous statement holds are said to have the Beth (definability) property. So the above-mentioned example shows that first order logic restricted to finite models does not have the Beth property. Another logic which fails to have this property is L_{2} (cf. [14]. See also Remark 4.4). Besides first order logic, logics with the Beth property include classical (and intuitionistic) propositional calculus, or the modal logics K, K4 and S5.

Note that for GF (and the modal logics), as long as we consider finite set of sentences Σ it does not make a difference for the Beth property whether we are in the classical context of not necessarily finite models or regard finite models only. For, as these logics have the finite model property, a finite set of sentences Σ implicitly defines a relation over finite models if and only if it does so over all models. The same for explicit definitions.

Description Logics Description logics were designed for the purpose of knowledge representation. Roughly speaking, a description logic starts from some some set of primitive concepts (which are unary predicates) and roles (binary predicates). The logic then specifies (or defines) complex concepts out of these primitives and makes assertions about these specifications, mostly in terms of modally expressible dependencies between concepts via roles. E.g., the logic can assert that a certain object, or all objects related to it via a designated role, belongs to a certain concept. Although they originated from entirely different backgrounds, there is a close correspondence between description logics and modal logics. For example the basic multi-modal logic K_{n} is nothing but a syntactic variant of the description logic ALC [15]. Hence the guarded fragment can also be seen as a general framework for description logics, which may express more than the ordinary modal dependencies. In particular, it may go beyond the built-in arity restriction of modal logics, so that one can speak of higher-arity concepts and roles. The interested reader is referred to [4] for a proposal of GF as a framework for description logic and for further references. In the description logic context, the Beth property seems particularly desirable as it guarantees explicit definability of concepts (and roles): e.g., concept specification in the framework of GF is closed in the sense that any concept that can implicitly be characterized can actually be defined explicitly within the logic.

Outline of paper Ever since 1956 when W. Craig gave an alternative proof of the Beth theorem for first order logic via his interpolation theorem, these two properties are almost always studied simultaneously. This paper forms no exception. In Section 3 we will prove a certain interpolation property for GF from which the Beth property for GF will be derived in Section 4. Even better, both these properties will be shown to hold for each of the the n-variable fragments of GF individually, in the presence of at most n-ary relations. Compared to results in [14] this shows that guarded finite variable fragments are much better behaved w.r.t. definability than the full finite variable fragments of first order logic.

2 Preliminaries

In this section we will collect all the necessary preliminaries. It also serves to fix notation and terminology.

Convention 2.1 By a language L we will henceforth understand a relational first order language without function- or constant symbols. Besides variables, and the parentheses ), (, we consider as logical symbols the connectives ∧, ¬, the existential quantifier ∃ and the identity symbol =. ◁

Notation 2.2 Models will be denoted by calligraphic letters like M, N, and their respective universes by M, N, etc. The interpretation of an n-ary predicate R in the model M (notation: IM(R)) is defined as usual. Moreover, we will extend this terminology to sets. That is, for X ⊆ M we will write X ∈ IM(R) if the elements of X are R-related, in any order or multiplicity. E.g., if R is ternary and ⟨n, m, n⟩ ∈ IM(R), then {m, n} ∈ IM(R). For a model M, ⟨m_{1}, …, m_{n}⟩ ∈ M^{n} and a formula φ with free variables among {v_{1}, …, v_{n}}, we will write M ⊧ φ[m_{1}, …, m_{n}] iff each assignment which maps v_{i} to m_{i} satisfies φ in M. If Σ is a formula (or a set of formulas) and ψ a formula, then Σ ⊧ ψ denotes the consequence relation. That is, Σ ⊧ ψ iff any assignment into a model M which satisfies (all formulas in) Σ also satisfies ψ in M. In particular, φ ⊧ ψ is the same as to say that φ → ψ is valid, i.e., ⊧ φ → ψ. For any formula φ, by free(φ) we denote the set of free variables occurring in φ. By L_{φ} (read: the language of φ) we denote the set of relation symbols occurring in φ. ◁

2.1 Defining the guarded fragment: Syntax

Definition 2.3 (Guarded formula) Let L be a language. The atomic Lformulas (or, L-atoms) are of the usual form:

1. v_{1} = v_{2}, for variables v_{1}, v_{2}.

2. P v_{1} ⋯ v_{n}, for n-ary P ∈ L, and variables v_{1}, …, v_{n}, not necessarily distinct.

The guarded L-formulas are defined by induction as follows.

1. Any atomic L-formula is a guarded L-formula.

2. If φ, ψ are guarded L-formulas, then φ∧ψ and ¬φ are guarded L-formulas.

3. Let v̄ be a finite, non-empty sequence of variables, ψ a guarded L-formula, and G an L-atom such that free(ψ) ⊆ free(G). Then ∃v̄(G ∧ ψ) is a guarded L-formula. In this case, the atom G is called the guard of the quantifier. ◁

Note that as a dual of guarded existential quantification we also get guarded universal quantification, of the form ∀v̄(G → ψ).

A typical example of a guarded formula is the one expressing symmetry of a relation: ∀v_{1}v_{2}(Rv_{1}v_{2}→Rv_{2}v_{1}). On the other hand, the formula ∃v_{2}(v_{1} < v_{2} ∧ψ(v_{2})∧∀v_{3}[(v_{1} < v_{3} ∧v_{3} < v_{2})→φ(v_{3})]) (the translation of the tense logical formula Until(φ, ψ)) is non-guarded, as the guard in the subformula expressing betweenness (i.e., the formula ∀v_{3}[(v_{1} < v_{3} ∧ v_{3} < v_{2})→φ(v_{3})]) is not atomic.

Remark 2.4 For readers familiar with [1] we note that contrary to that paper, Definition 2.3 allows for identity atoms as guards. Since this issue does not affect decidability nor interpolation, we decided to concentrate on this slightly more general fragment. This also places us in line with [3]. ◁

Guarded formulas are obviously first order formulas. The fragment of first order logic consisting of guarded formulas is aptly called the guarded fragment (GF). We understand by GF_{n}, n ∈ ω, the fragment of GF that consists of formulas whose variables (free or bound) are among v_{1}, …, v_{n}. The collection of formulas in GF_{n} which are built up from at most k-ary relation symbols will be denoted by GF_{n}^{k}.

2.2 Semantic characterization of the guarded fragment

Similar to modal logics, the guarded fragment can be semantically analyzed via a suitable notion of bisimulation. This has been done in [1]. Here we will recapitulate as much of these results as needed for the purposes of the present paper.

Definition 2.5 (live set) Let Z be a finite subset of a model M. The set Z is called live in M if Z is either a singleton, or there exists a relation R and a set X such that Z ⊆ X ∈ IM(R). In this case we will say that Z is R-live (in M). For any language L we use the notation Z ⊆_{L}^{l} M to denote that Z is L-live in M. That is, Z is R-live in M for some R ∈ L. We will omit the subscript L if it does not cause confusion. ◁

Note that by definition subsets of live sets are again live.

Below, by a partial L-isomorphism we mean a finite one-to-one partial map between two models which preserves the relations in L both ways. By the image of a map f : X ⟶ Y we understand the set {f(x) : x ∈ X}.

Definition 2.6 (Guarded bisimulation) Let L be a language. A guarded L-bisimulation between two models M and N is a non-empty set F of finite partial L-isomorphisms between M and N such that for any f : X ⟶ Y ∈ F the following holds:

1. For any Z ⊆_{L}^{l} M there is a g ∈ F with domain Z such that g and f agree on the intersection of their domains. (The zig-condition)

2. For any W ⊆_{L}^{l} N there is a g ∈ F with image W such that g^{−1} and f^{−1} agree on the intersection of their domains. (The zag-condition) ◁

Guarded bisimulations are defined in such a way as to preserve guarded formulas. That is, for every guarded L-formula φ with free variables among {v_{1}, …, v_{k}}, every guarded L-bisimulation F between models M, N, every f ∈ F and every ⟨m_{1}, …, m_{k}⟩ ∈ dom(f)^{k},

M ⊧ φ[m_{1}, …, m_{k}] ⇔ N ⊧ φ[f(m_{1}), …, f(m_{k})].

This can be shown by a straightforward induction on the complexity of φ. The zig- and zag-conditions take precisely care of the induction step for the existential quantifier. Indeed, preservation under guarded bisimulations is the characteristic feature of GF, in the sense of the following Characterization Theorem from [1]: up to logical equivalence, GF precisely consists of those first order formulas that are preserved under guarded bisimulations.

Note that in the definition of a guarded bisimulation that can be found in [1], the above role of live sets is taken over by what ABN call guarded sets. These are subsets Z of a model M such that Z ∈ IM(R), for some relation R. Mutatis mutandis, all arguments in [1] and in particular the characterization theorem also apply to guarded formulas and guarded bisimulations as defined in this paper. Note e.g., that a guarded formula of the form ∃v(v = v ∧ ¬P v) which is not guarded in the ABN-sense, is preserved under guarded bisimulations in our sense by virtue of the fact that singletons are live.

In the remaining of this section we will dirty our hands on some formalization which paves the way for the proof of Theorem 4.1. Let R be a relation. We will construct a guarded formula λ_{R}(v_{1}, …, v_{l}) in the language {R} which defines the set of R-live l-tuples. That is, for all models M and ⟨m_{1}, …, m_{l}⟩ ∈ M^{l}: M ⊧ λ_{R}[m_{1}, …, m_{l}] iff the set {m_{1}, …, m_{l}} is R-live in M.

Let s be the arity of R. Let e range over all complete equality types in variables v_{1}, …, v_{l}. We regard e both as a quantifier-free formula e(v_{1}, …, v_{l}) in the empty vocabulary and as an equivalence relation on the set {1, …, l} according to (j, i) ∈ e iff e ⊧ v_{j} = v_{i}. Let ρ: {1, …, s} → {1, …, l + s} be a mapping that is onto {1, …, l}/e, i.e., for every j ∈ {1, …, l} there is some i ∈ {1, …, s} such that ρ(i) is in the same e equivalence class with j. Put, for any such pair of e and ρ,

γ_{e,ρ} = e(v_{1}, …, v_{l}) ∧ ∃v̄(Rv_{ρ(1)} … v_{ρ(s)} ∧ true),

where v̄ consist of those v_{ρ(i)} for which ρ(i) > l (if there are such; else no quantification is necessary and γ_{e,ρ} is actually atomic). The desired formula λ_{R}(v_{1}, …, v_{l}) is obtained as the disjunction over all γ_{e,ρ} for matching pairs (e, ρ).

For any finite language L we further obtain a formula λL(v_{1}, …, v_{l}) defining the set of L-live l-tuples by putting

λL(v_{1}, …, v_{l}) =( ⋀_{1≤i,j≤l} v_{i} = v_{j}) ∨ ⋁_{R∈L} λ_{R}(v_{1}, …, v_{l}),

where the first disjunct reflects the fact that all singleton sets are regarded as live (namely, as guarded by equality).

We finally note that ∃v̄(Rv_{ρ(1)} … v_{ρ(s)} ∧ true), can be rewritten in at most s variables. Hence γ_{e,ρ} is equivalent to a formula in GF_{max(l,k)}. We conclude that for every finite language L which contains at most k-ary relations and any l ≤ k, we may assume λL(v_{1}, …, v_{l}) ∈ GF_{k}^{k}.

3 Interpolation for the guarded fragment

As shown in [9], GF does not have the interpolation property.

THEOREM 3.1 (Failure of interpolation in GF) There exist sentences φ, ψ ∈ GF_{3}^{3} such that ⊧ φ → ψ, for which there does not exist a guarded interpolant (in any number of variables). That is, there does not exist a guarded formula ϑ built up from relation symbols which occur both in φ and ψ such that ⊧ φ → ϑ and ⊧ ϑ → ψ.

To see why this property fails for GF, it is useful to compare it to the interpolation property studied in modal logic. In modal logic, the interpolant is usually confined to proposition letters in the common language but may however contain non-shared modalities. Strengthening the requirement on the common language to also include common modalities results in a much stronger interpolation property. [2] shows this property for the basic multi-modal K.

[10] generalizes this result to Sahlqvist axiomatizable multi-modal logics whose axioms correspond to universal Horn frame conditions which do not specify any interaction between the different accessibility relations (e.g., bi-modal S5). When we have interaction, the stronger interpolation property is easily lost as the following example from [2] shows. Consider the multi-modal logic defined by the axiom ◇_{1}p →◇_{2}p. This logic does not have the stronger interpolation property. For, in this logic ◇_{1}T rue → ◇_{2}T rue is a theorem whereas the only formulas in the common language (in the strong sense) are T rue and F alse, which are obviously not interpolants. However, this logic does have the usual interpolation property (cf. [11, Corollary B.4.1]).

Thinking of guarded formulas as translations of modal formulas, we see that Theorem 3.1 formulates exactly this strong version of interpolation, where ‘common language’ means the set of common relation symbols which includes both the relations which are translated proposition letters, and the relations that are obtained in translating the modalities. This suggests to consider an alternative interpolation property for GF that more closely resembles the one that is usually studied in modal logic. For this we will distinguish occurrences of relation symbols as guards from other occurrences.

Notation 3.2 For any guarded formula φ we understand by L_{G(φ)} the set of relations that occur in φ as the guard of some quantifier. ◁

Note that the relations in L_{G(φ)} may at the same time occur in φ at non-guard positions. For example, in φ = ∃x(P x ∧ ∀y(Sxy→P y)), the relation P occurs both as a guard and as a non-guard.

Definition 3.3 (Guarded L_{1}/L_{2}-bisimulation) Let L_{1} ⊆ L_{2} be languages. A guarded L_{1}/L_{2}-bisimulation between models M and N is defined as a non-empty set of finite partial L_{2}-isomorphisms between M, N with zig- and zag- condition stipulated for L_{1}-live sets only. ◁

This type of bisimulation supports a characterization theorem for that fragment of GF in which only L_{1}-predicates may be used as guards, but all predicates in L_{1} and L_{2} may occur at non-guard positions. Analogously to the characterization theorem for GF, the following characterization can be shown, using [9, Proposition 3.11].

PROPOSITION 3.4 Let L_{1} ⊆ L_{2} be languages which contain at most kary relation symbols. A first order sentence φ is preserved under guarded L_{1}/L_{2}-bisimulations iff φ is logically equivalent to an L_{2}-sentence ψ ∈ GF_{k}^{k} with L_{G(ψ)} ⊆ L_{1}.

Notation 3.5 Let L be a language. For models M, N and ⟨m_{1}, …, m_{k}⟩ ∈ M^{k}, ⟨n_{1}, …, n_{k}⟩ ∈ N^{k}, we write

M, m_{1} ⋯ m_{k} ≡L^{GF_{k}} N , n_{1} ⋯ n_{k}

if for any L-formula θ in GF_{k}, M ⊧ θ[m_{1}, …, m_{k}] iff N ⊧ θ[n_{1}, …, n_{k}]. ◁

Recall that for any formula ϑ, by L_{ϑ} we denote the language consisting of all the relation symbols occurring in ϑ. The theorem below states that GF_{k}^{k} (and hence GF) has interpolation provided an interpolant for φ → ψ is allowed to contain relations in L_{G(φ)} and L_{G(ψ)} which are not necessarily in the common language. Modally speaking, an interpolant may contain non-shared modalities.

THEOREM 3.6 (GF_{k}^{k} has interpolation w.r.t. non-guard occurrences) Let k ∈ ω. For any φ, ψ ∈ GF_{k}^{k} such that ⊧ φ → ψ, there exists a ϑ ∈ GF_{k}^{k} such that

1. L_{ϑ} ⊆ (L_{φ} ∩ L_{ψ}) ∪ L_{G(φ)} ∪ L_{G(ψ)}, and

2. ⊧ φ → ϑ and ⊧ ϑ → ψ .

Proof of Theorem 3.6: We will show ‘amalgamation via bisimulation’ in the same spirit as e.g., the proof of interpolation for the basic modal logic K in [1, Theorem 2.5]. Its main construction is a deviation of a fairly standard amalgamation method as can be found in e.g., [12] and [13].

For the course of this proof, let k ∈ ω be fixed but arbitrary. Consider φ, ψ ∈ GF_{k}^{k} such that ⊧ φ → ψ. For brevity, write L for (L_{φ} ∩ L_{ψ}) ∪ L_{G(φ)} ∪ L_{G(ψ)}. Let

Θ =^{def} {ϑ ∈ GF_{k} : L_{ϑ} ⊆ L & ⊧ φ → ϑ}.

Our aim is to show that

Claim 3.7 Θ ⊧ ψ.

By compactness, it follows from this claim that ψ is implied by some finite conjunction ϑ of formulas in Θ. Note that ϑ is again an L-formula in GF_{k}^{k}. Hence ϑ is an interpolant for φ, ψ, and we are done.

To prove Claim 3.7, consider an L_{ψ} ∪ L_{G(φ)}-model N, and ⟨b_{1}, …, b_{k}⟩ ∈ N^{k} such that N ⊧ ϑ[b_{1}, …, b_{k}], for every ϑ ∈ Θ. Our task is to show that N ⊧ ψ[b_{1}, …, b_{k}].

We first note that there exists some L_{φ}∪L_{G(ψ)}-model M and ⟨a_{1}, …, a_{k}⟩ ∈ M^{k} such that

M ⊧ φ[a_{1}, …, a_{k}], and M, a_{1} ⋯ a_{k} ≡L^{GF_{k}} N , b_{1} ⋯ b_{k}.

For, reasoning to contraposition, assume such M, ⟨a_{1}, …, a_{k}⟩ do not exist. In that case, Φ =^{def} {ϑ ∈ GF_{k} : L_{ϑ} ⊆ L & N ⊧ ϑ[b_{1}, …, b_{k}]} ⊧ ¬φ. By compactness it follows that ⊧ φ → ¬ ⋀ Φ_{0}, for some finite conjunction of formulas in Φ. Therefore ¬ ⋀ Φ_{0} ∈ Θ, whence N ⊧ ¬ ⋀ Φ_{0}[b_{1}, …, b_{k}]. Quod non.

By passing to ω-saturated elementary extensions of M and N, we may assume w.l.o.g. M, N to be ω-saturated. As shown in the proof of the Characterization Theorem for GF in [1, Theorem 4.2.2], the relation of guarded L-equivalence between ω-saturated structures induces a guarded L-bisimulation. The same is true for the relation of ≡L^{GF_{k}} if L contains at most k-ary relations. Hence our assumption in particular implies the existence of a guarded L-bisimulation between M, N which links ⟨a_{1}, …, a_{k}⟩ and ⟨b_{1}, …, b_{k}⟩.

The aim of the rest of this proof is to amalgamate the models M and N in such a way that we can define guarded L_{G(φ)}/L_{φ}- (resp. L_{G(ψ)}/L_{ψ}-) bisimulations from the amalgamated model to M (resp. N) which, when composed, will map ⟨a_{1}, …, a_{k}⟩ to ⟨b_{1}, …, b_{k}⟩. Chasing the resulting diagram and using the fact that φ ⊧ ψ will yield the desired conclusion that N ⊧ ψ[b_{1}, …, b_{k}]. This will be made precise in the sequel.

Begin Construction Model We will define a model over the set MN consisting of pairs ⟨m, n⟩ ∈ M × N whose components can not be distinguished by L-formulas in GF_{k}. The interpretation of the predicates will be read of coordinatewise. More precisely,

• MN =^{def} {⟨m, n⟩ ∈ M × N : M, m ≡L^{GF_{k}} N , n}.

• For l-ary R ∈ L_{φ}, set ⟨⟨m_{1}, n_{1}⟩, …, ⟨m_{l}, n_{l}⟩⟩ ∈ IMN (R) iff

– M, m_{1} ⋯ m_{l} ≡L^{GF_{k}} N , n_{1} ⋯ n_{l},

(i.e., m_{i}, n_{i}, i = 1, …, l, are not only pairwise equivalent but jointly so), and

– ⟨m_{1}, …, m_{l}⟩ ∈ IM(R).

• The interpretation of relations in L_{ψ} is defined similarly.

End Construction Model

Note that the interpretation of relations in the common language is well-defined thanks to the requirement on live subsets of MN to be jointly L-equivalent. The upshot of amalgamating our models into a product is that we can take projection functions as building blocks for the desired bisimulations. This is the purport of the following lemma, where π_{i}, i = 1, 2, denotes the projection function to the i-th coordinate, and the k-tuples ⟨a_{1}, …, a_{k}⟩ ∈ M^{k}, ⟨b_{1}, …, b_{k}⟩ ∈ N^{k} are the ones picked at the very beginning of this proof.

LEMMA 3.8 (Amalgamation lemma) The set F_{π_{1}} defined by F_{π_{1}} =^{def} {π_{1} :

X ⟶ Y : X ⊆L_{G(φ)}^{l} MN or X = {⟨a_{1}, b_{1}⟩, …, ⟨a_{k}, b_{k}⟩}}, is a guarded

L_{G(φ)}/L_{φ}-bisimulation between MN and M. The analogously defined set F_{π_{2}} is a guarded L_{G(ψ)}/L_{ψ}-bisimulation between MN and N.

Before proving the above lemma, let us first demonstrate its use and finish the proof of Claim 3.7. Recall that the model M and the sequence ⟨a_{1}, …, a_{k}⟩ ∈ M^{k} were chosen in such a way that M ⊧ φ[a_{1}, …, a_{k}]. We took care to include π_{1} : {⟨a_{1}, b_{1}⟩, …, ⟨a_{k}, b_{k}⟩} ⟶ {a_{1}, …, a_{k}} in F_{π_{1}}. Since φ is invariant under guarded L_{G(φ)}/L_{φ}-bisimulations, it follows from the amalgamation lemma that MN ⊧ φ[⟨a_{1}, b_{k}⟩, …, ⟨a_{k}, b_{k}⟩]. By assumption, then MN ⊧ ψ[⟨a_{1}, b_{1}⟩, …, ⟨a_{k}, b_{k}⟩]. Since π_{2} : {⟨a_{1}, b_{1}⟩, …, ⟨a_{k}, b_{k}⟩} ⟶ {b_{1}, …, b_{k}} is in F_{π_{2}}, the second part of the amalgamation lemma allows us to conclude that N ⊧ ψ[b_{1}, …, b_{k}]. Q.E.D. Claim 3.7.

Now we turn to the proof of the amalgamation lemma.

Proof of Lemma 3.8: We will prove the first part of the lemma concerning F_{π_{1}}. The second statement about F_{π_{2}} can be shown similarly.

F_{π_{1}} is obviously non-empty. Let π_{1} : X ⟶ Y ∈ F_{π_{1}}. Then X =

{x_{1}, …, x_{l}}, for some l ≤ k, and M, π_{1}(x_{1}) ⋯ π_{1}(x_{l}) ≡L^{GF_{k}} N , π_{2}(x_{1}) ⋯ π_{2}(x_{l}).

By construction this implies that for n-ary R ∈ L_{φ}, and ⟨x_{1}, …, x_{n}⟩ ∈ X^{n} it is the case that ⟨x_{1}, …, x_{n}⟩ ∈ IMN (R) iff ⟨π_{1}(x_{1}), …, π_{1}(x_{n})⟩ ∈ IM(R). In other words, π_{1} is a partial L_{φ}-isomorphism.

For the zag-condition, consider π_{1} : X ⟶ Y ∈ F_{π_{1}}, and W ⊆_{R}^{l} M, for some R ∈ L_{G(φ)}. Again, X = {x_{1}, …, x_{l}}, for some l ≤ k, and M, π_{1}(x_{1}) ⋯ π_{1}(x_{l}) ≡L^{GF_{k}} N , π_{2}(x_{1}) ⋯ π_{2}(x_{l}). Recall that the relation ≡L^{GF_{k}} forms a guarded Lbisimulation between M and N. The above equivalence states that the partial map f from M to N which maps π_{1}(x) to π_{2}(x), for any x ∈ X, is an element of this bisimulation. By the zig-condition, there exists a partial L-isomorphism g in this bisimulation with domain W which agrees with f on the intersection of their domains. Let W^{∗} = {⟨w, g(w)⟩ : w ∈ W } ⊆_{R}^{l} MN. Then W^{∗} is the desired pre-image for W. As the zig-condition is trivially fulfilled, this completes the proof. Q.E.D. Lemma 3.8. Q.E.D. Theorem 3.6.

Corollary 3.9 GF has interpolation w.r.t. non-guard occurrences.

4 The Beth theorem for GF

In general, an important reason to investigate the interpolation property is that it can be seen as an intermediate stage in proving the Beth definability theorem. It will be shown that the limited form of interpolation expressed in Theorem 3.6 still serves this purpose for GF.

Let L_{0} be a language and R and R′ distinct relation symbols of the same arity that are not in L_{0}. Let L = L_{0} ∪ {R}. Let Σ be a set of guarded sentences in the language L, and let Σ′ denote the result of renaming R to R′ in Σ.

THEOREM 4.1 (Beth Theorem for GF_{k}^{k}) Let L_{0}, L, R, R′, Σ and Σ′ be as above. Let k ∈ ω be such that Σ ∪ {Rv̄} ⊆ GF_{k}^{k}. If Σ implicitly defines R, i.e., if

Σ, Σ′ ⊧ ∀v̄(Rv̄ ↔ R′v̄),

then there exists some formula φ(v̄) ∈ GF_{k}^{k} in the language L_{0} such that

Σ ⊧ ∀v̄(Rv̄ ↔ φ(v̄)),

i.e., φ is an explicit definition for R relative to Σ.

Proof of Theorem 4.1: Let all data be as in theorem, and assume that

Σ, Σ′ ⊧ ∀v̄(Rv̄ ↔ R′v̄).  (1)

We will first show that this assumption enables us to conclude that any R-live set in a model for Σ is L_{0}-live, i.e., P -live for some P ∈ L_{0}.

Claim 4.2 Assume (1). Let M be a model of Σ, and let Y ⊆_{R}^{l} M. Then

Y ⊆L_{0}^{l} M.

Proof of Claim 4.2: Assume (1). Let M be a model of Σ, and let Y_{0} ⊆_{R}^{l} M. Reasoning to contraposition, suppose Y_{0} ⊈L_{0}^{l} M. We will derive a contradiction from this.

Let \underline{2} denote the two-element universal L-model with domain \{0, 1\}. That is, s̄ ∈ I\underline{2}(P), for every l-ary P ∈ L and every s̄ ∈ \{0, 1\}^{l}. Let M×\underline{2} denote the usual product model. Writing π_{1} for the projection on the first coordinate, this definition entails that s̄ ∈ IM×\underline{2}(P) iff ⟨π_{1}(s_{1}), …, π_{1}(s_{l})⟩ ∈ IM(P), for s̄ ∈ (M ×{0, 1})^{l} and l-ary P ∈ L. As the reader can easily verify, this in its turn implies that F_{1} =^{def} \{π_{1} : X ⟶ Y : X ⊆_{L}^{l} M × \underline{2}\} is a guarded L-bisimulation between M×\underline{2} and M. Since M ⊧ Σ, we conclude that M×\underline{2} ⊧ Σ.

Our aim is to modify the interpretation of R on M×\underline{2} in such a way that the resulting structure is again a model for Σ, contradicting the fact that Σ implicitly defines R. For this, we pick some X_{0} ⊆ (M × {0, 1}) for which π_{1}[X_{0}] = Y_{0}. Consider the model (M×\underline{2})′ on the set (M × \{0, 1\}) which differs from M×\underline{2} only in the respect that X_{0} ∉ I(M×\underline{2})′(R). We claim that F′_{1} =^{def} \{π_{1} : X ⟶ Y : X ⊆_{L}^{l} (M×\underline{2})′\} is a guarded L-bisimulation between (M×\underline{2})′ and M.

F′_{1} is certainly not empty. Consider some π_{1} : X ⟶ Y in F′_{1}. If X_{0} ⊈ X, then L-relations are obviously preserved by π_{1} in both ways. But we changed the interpretation of R such that X_{0} is not R-live in (M×\underline{2})′. As Y_{0} is not L_{0}- live, it follows that X_{0} is not L_{0}-live in (M×\underline{2})′ either, and hence no superset of X_{0} is the domain of some π_{1} ∈ F′_{1}.

The zig-condition needs no comment. For the zag-condition, consider some π_{1} : X ⟶ Y in F′_{1}, and W ⊆_{L}^{l} M. If W ⊆ Y, the condition is trivially fulfilled. If not, then π_{1}^{−1}[Y ∩ W] can be extended in at least two ways to a set Z for which π_{1}[Z] = W. For W ≠ Y_{0}, either one of these two extensions constitutes the domain of a projection in F′_{1} fulfilling the zag condition for π_{1}, W. For W = Y_{0} any extension other than X_{0} can be taken as such.

This shows that (M×\underline{2})′ ⊧ Σ. Summarizing, M×\underline{2} ⊧ Σ, (M×\underline{2})′ ⊧ Σ but IM×\underline{2}(R) ≠ I(M×\underline{2})′(R). This contradicts the fact that Σ implicitly defines R. We conclude that Y_{0} is indeed L_{0}-live, as was to be shown. Q.E.D. Claim 4.2.

By compactness we may assume Σ to be a single formula, and L_{0} finite. Assume R to be l-ary, and let v̄ = ⟨v_{1}, …, v_{l}⟩. Let λ_{0}(v̄) be the canonical L_{0}-formula in GF_{k}^{k} saying that the set {v_{1}, …, v_{l}} is L_{0}-live (cf. page 7). For all L-models M we define R_{0} =^{def} {m̄ ∈ M^{l} : M ⊧ Rv̄ ∧ λ_{0}(v̄)[m̄]}. Note that by Claim 4.2, IM(R) = R_{0}, for models M of Σ. Let Σ_{0} be the result of replacing in Σ any occurrence of Rv̄ by the conjunction λ_{0}(v̄) ∧ R(v̄). In other words, Σ_{0} is the canonical set of formulas which asserts that Σ holds of R_{0} (rather than R itself). It is now straightforward to check the following:

(i) Σ_{0} is preserved under guarded L_{0}/L-bisimulations. Hence, by Proposition 3.4, Σ_{0} is equivalent to an L-formula Γ in GF_{k}^{k} with L_{G(Γ)} ⊆ L_{0}.

(ii) Σ ⊧ Σ_{0}, by Claim 4.2. (iii) For every L_{0}-model M, and every interpretation of R in M: if (M, R) ⊧

Σ_{0}, then (M, R_{0}) ⊧ Σ.

Let Σ′_{0} be the result of replacing R by R′ in Σ_{0}. It follows from (1) and (iii) that

Σ_{0} ∧ λ_{0}(v̄) ∧ Rv̄ ⊧ Σ′_{0} → R′v̄.  (2)

For, consider an L_{0} ∪ {R, R′}-model (M, R, R′) and some m̄ ∈ M^{l} such that (M, R, R′) ⊧ Σ_{0} ∧ λ_{0}(v̄) ∧ Rv̄ ∧ Σ′_{0}[m̄]. We have to show that (M, R, R′) ⊧ R′v̄[m̄]. It follows from (iii) that (M, R_{0}, R′_{0}) ⊧ Σ ∧ Rv̄ ∧ Σ′[m̄]. By (1), then (M, R_{0}, R′_{0}) ⊧ R′v̄[m̄]. Hence certainly, (M, R, R′) ⊧ R′v̄[m̄].

Replace Σ_{0} and Σ′_{0} in (2) by L_{0}-guarded formulae Γ and Γ′ according to (i). We then may apply Theorem 3.6 to obtain, as an interpolant for (2), a formula ϑ(v̄) in GF_{k}^{k} such that L_{ϑ} ⊆ L_{0} and Σ_{0} ∧ λ_{0}(v̄) ∧ Rv̄ ⊧ ϑ(v̄) and ϑ(v̄) ⊧ Σ′_{0} → R′v̄. Applying (ii) and Claim 4.2, we find that Σ ∧ Rv̄ ⊧ ϑ(v̄). Renaming R′ back into R in the second implication and one more appeal to (ii) gives us that ϑ(v̄) ⊧ Σ → Rv̄. Hence Σ ⊧ Rv̄ ↔ ϑ(v̄) and ϑ provides the desired explicit definition of R relative to Σ. Q.E.D. Theorem 4.1.

Corollary 4.3 GF has the Beth definability theorem.

Remark 4.4 Theorem 4.1 shows that guarded finite variable fragments behave much nicer w.r.t. definability than the full finite variable fragments of first order logic (FO). For not only does the Beth theorem fail for any n-variable fragment of FO, n ≥ 2, it fails drastically. Even FO_{2}^{2} (using the terminology FO_{n}^{k} for fragments of FO similar to our use of GF_{n}^{k} for guarded fragments) does not have the Beth property. For more information, the reader is referred to [14] or [8]. ◁

References

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

[2] J. van Benthem. Modal foundations for predicate logic. In E. Orlowska, editor, Memorial Volume for Elena Rasiowa, Studies in fuzziness and soft computing, pages 39–55. Physica-Verlag, Heidelberg, New York, 1999.

[3] E. Grädel. On the restraining power of guards. Technical report, RWTH Aachen, Lehrgebiet Mathematische Grundlagen der Informatik, 1997. To appear in the Journal of Symbolic Logic.

[4] E. Grädel. Guarded fragments of first-order logic: a perspective for new description logics? In Proc. of 1998 Int. Workshop on Description Logics DL ‘98, Trento, CEUR Electronic Workshop Proceedings, 1998. Extended

abstract, available at http://sunsite.informatik.rwth-aachen.de/
Publications/ CEUR-WS/Vol-11.

[5] E. Grädel, P. Kolaitis, and M. Vardi. On the decision problem for two– variable first order logics. Bulletin of Symbolic Logic, 3:53–69, 1997.

[6] E. Grädel and I Walukiewicz. Guarded fixed point logic. Technical report, RWTH Aachen, Lehrgebiet Mathematische Grundlagen der Informatik, 1999.

[7] P. Hájek. Generalized quantifiers and finite sets. Ser. Konfer. No 1 14, Prace Nauk. Inst. Mat. Politech. Wroclaw, 1977.

[8] I. Hodkinson. Finite variable logics. Bull. Europ. Assoc. Theor. Comp. Sci., 51:111–140, 1993. Addendum in vol. 52. Also available at

http://www.doc.ic.ac.uk/~imh/papers/yuri.html.

[9] E. Hoogland and M. Marx. Interpolation in guarded fragments. Technical report, Institute for Logic, Language and Computation, University of Amsterdam, 1999.

[10] M. Marx. Interpolation in (fibered) modal logic. In A. Haeberer, editor, Proceedings of AMAST 1998, Amazonia–Manaus, Brazil, 4–8 January 1999, 1999.

[11] M. Marx and Y. Venema. Multi-dimensional Modal Logic. Applied Logic Series. Kluwer Academic Publishers, 1997.

[12] Maarten Marx. Algebraic Relativization and Arrow Logic. PhD thesis, illc, 1995.

[13] I. Németi. Cylindric relativized set algebras have strong amalgamation. Journal of Symbolic Logic, 50(3):689–700, 1985.

[14] I. Sain. Beth’s and Craig’s properties via epimorphisms and amalgamation in algebraic logic. In C. Bergman, R. Maddux, and D. Pigozzi, editors, Algebraic logic and universal algebra in computer science, volume 24 of Lecture Notes in Computer Science, pages 209–226. Springer Verlag, Berlin, Heidelberg, New York, 1990.

[15] K. Schild. A correspondence theory for terminological logics. In Proceedings of the 12th IJCAI, pages 466–471, 1991.

[16] M. Vardi. Why is modal logic so robustly decidable? In Descriptive Complexity and Finite Models: Proceedings of a DIMACS Workshop, volume 31 of Series in Discrete Mathematics and Theoretical Computer Science, pages 149–184. American Mathematical Society, 1989.