Taming first order logic:

relating the semantic and the syntactic approach

Maarten Marx

Abstract

Out of the joint work of Johan van Benthem and the Hungarian group round Hajnal Andréka, István Németi and Ildikó Sain and their PhD students, two approaches for taming a logic evolved. With taming a logic we mean changing the logic in such a way that it becomes decidable. For first order logic, they took a semantic route using relativisation of models, and a syntactic route focusing on guarded fragments. The purpose of this paper is to show that these two routes are really two sides of the same coin. We do this by showing that a certain guarded fragment (called here the packed fragment) of first order logic forms precisely the set of first order sentences which are invariant for relativisation with a tolerance relation. Besides this technical contribution we provide an intuitive explanation of relativisation in terms of information transmission.

Contents

1 Introduction 2

2 Relativisation interpreted as a sceptical information processing strategy 2

3 Relativised semantics for first order logic 5 3.1 Admissible assignments . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 Different relativisations . . . . . . . . . . . . . . . . . . . . . . . 8 3.3 Bisimulations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

4 Packed fragment 13

5 Conclusion 17

Dedicated to Johan van Benthem on his fiftieth birthday.

1 Introduction

The main purpose of this paper is to give a semantic characterisation of the guarded fragment (here called the packed fragment) in terms of invariance for relativisation (Theorem 4.11). We will argue that relativisation in a first order setting is the analogue of taking generated submodels in modal logic. Our tentative conclusion will be that the packed fragment is the true modal fragment of first order logic, because it has the same “local flavour” and is decidable for very similar reasons. Besides this technical result we provide an interpretation of relativisation as a sceptical information processing strategy in section 2. We show that for sentences in the packed fragment, this sceptical strategy leads to the same results (in terms of validity and satisfaction) as the classical first order interpretation. This result makes the sceptical strategy an interesting alternative because it has great computational advantages over the classical first order way of interpreting sentences.

The technical part of this paper is organised as follows. We introduce relativised semantics for first order logic in Section 3. We take a modal view on first order logic and arrive to the notion of admissible assignments. We show how relativised semantics can be obtained from two primitive concepts: context sets and tolerance relations. Then we introduce our version of the (loosely) guarded fragment, called the packed fragment, and relate it to relativised semantics. We conclude by arguing that the packed fragment is the true modal fragment of first order logic.

2 Relativisation interpreted as a sceptical information processing strategy

We employ a very simple model of information transmission: there are two participants of which one does all the talking and the other merely listens and interprets the incoming information. It will be convenient to ascribe gender to the two participants. We assume that the speaker is male and the listener is female. The language used by the speaker is a first order language, which will be interpreted dynamically, in the style of Dynamic Predicate Logic (DPL) of [3, 4].

The update–semantics version of DPL provides a model for the interpretation process performed by the listener

In the dynamic view the interpretation process consists of two components:

1. finding antecedents for anaphora (interpreting discourse information)

2. building a model of the world described by the speaker (interpretation of world–information).

The speaker however is not God or some other embodiment of the world just reporting what is the case, the speaker is an observer of the world reporting how he perceives it. Thus the interpretation of the world–information is more accurately described by

2’ building a model of the world perceived by the speaker on the basis of his report of it.

Once the listener realises that she is building a model of the world relative to the perception of the speaker, a number of information processing strategies are open to her. In this paper, we will focus on one such a strategy: the listener does not accept universal statements made by the speaker unconditionally, but relativises them with the proviso

“provided that the elements quantified over are perceived together by the speaker.”

We will make this proviso more precise in due course. First an example

Example 2.1 A company like McDonald’s can be modeled in many different ways. A natural way to think about it is as a collection of databases each containing the employees of one outlet, databases containing the managers of a region, databases containing the whatevers of some larger geographical unit, and so on, all the way up to the database containing the president and his companions. In other words, a hierarchical setup of partially overlapping databases.

Let’s look at the following situation. The president of McDonald’s gives his yearly address and says: “In this company, everybody loves each other.” A logician who ows his money baking hamburgers raises his finger and says that he doesn’t love his neighbour in the audience at all, since that man works in an outlet at the other side of the world. The president answers, rather annoyed, that he meant of course that “everyone within a unit in McDonald’s loves each other”.

The president and the logician interpret the first sentence differently because they amalgamated the databases in a different way. The logician used the classical way, while the president amalgamated them in a relativised manner. In this way he could keep the natural structure of the company. For the president, the natural way of interpreting his universal statement was using the proviso given above.

Before we go into the strategy, let’s look at some more basic questions. Why would a listener employ such a strategy? And, supposing there are good reasons, how does she know when elements of discourse are perceived together by the speaker? In other words, can she practically perform such a strategy at all?

To start with the first question, why would a listener not want to accept universal statements unconditionally? The answer is that the computational costs connected to universal statements are very high. They can quickly lead to infinite models, moreover it is undecidable to find out whether a set of sentences has a model at all.

Given this it is reasonable to postulate that the listener uses some kind of mechanism to cope with these difficulties of interpretation. What kind of mechanism she uses is of course open to debate. Whatever mechanism she will use, we can expect some natural properties of it:

• It should be sound: “whatever can still be deduced, can also be deduced in the “classical setting”.

• It shouldn’t lead to too much loss of information: on a large natural fragment of natural language, the classical and the adjusted interpretation process should lead to the same results.

• It should have definite computational advantages.

The strategy we propose satisfies all these. So let’s look at the second question: suppose the listener uses the “proviso–strategy”, how does she implement it? In particular how does she know which elements in the domain of discourse are perceived together by the speaker, and what does that mean?

We start with the latter. Given a domain D of individuals, and a subset X ⊆ D, how can we describe when the elements in X are perceived together by the speaker? One natural way to do this is to postulate that there exists a “distance” function f : D × D ⟶ ℝ, which describes for the speaker the distance between each two elements in D. With distance we mean something inherently vague with many dimensions. It has at least spatial, temporal, conceptual and cultural components, but also cognitive ones, individualised to each speaker. The listener could now state that the elements in X are perceived together by the speaker if for all a, b in X, the distance between a and b is less than some fixed value d. But if the listener cannot know the function f, she also has no idea about d. So what is left for her is just the abstract information that there exists a tolerance relation on D for the speaker. With the assumption that the distance between one object is arbitrarily small, the only thing she knows then is that there exists a binary relation δ(x, y) on D which is reflexive and symmetric.

So far so good, but how does she know which elements stand in this relation? She can’t know anything but the discourse of the speaker provides her with clues. That is, from the discourse she gets information which makes it reasonable to assume that indeed the speaker can perceive certain individuals together. The following are examples of such clues:

Named individuals all individuals which the speaker gives a name are perceived together.

Existentially introduced individuals If the speaker introduces two individuals existentially in the same discourse, then their denotation can be perceived together by him.

Primitive relations If the speaker puts certain individuals together in a primitive relation, then he can perceive them together. (We can view this as “naming” a group.)

Related to named individuals Quite a bit stronger is to postulate that the distance between any individual and any named individual is arbitrarily small.

Macho or classical δ is the universal relation on the domain of discourse. That is, the speaker can perceive each two individuals in the domain of discourse together.

The last clue brings us back to the classical interpretation of a discourse. Clearly such clues can be provided by the speaker. We will assume though that he can only do this outside the object language that we are studying. So the speaker should make a kind of meta–statement in order to effectuate this information. (Think of a math teacher who starts a class with: “Everything I will say holds for all the natural numbers and for them only”.)

This concludes our view on relativisation in a discourse setting. We wil now turn to the technical work. The clues presented above will re-occur there.

3 Relativised semantics for first order logic

We provide first order logic with a different semantics than the standard semantics. We assume we are working with a standard first order language without function symbols: thus the language contains equality, the usual first order connectives, a countable stock of variables and individual constants, and a countable stock of n-ary relation symbols, for every n. In addition we will assume that we have as primitive symbols also ∃v̄, where v̄ is a finite set of variables. When v̄ = {v_{1}, …, v_{k}}, then ∃v̄φ just means ∃v_{1} … ∃v_{k}φ in classical logic. For φ a formula in this language, FV (φ) denotes the set of free variables of φ, defined in the standard way.

In classical first order logic, the interpretation of a formula in a model (D, I) is given relative to an assignment of the variables s. Given a domain D, the set of assignments consists of all functions from the set of variables into D. The key idea of relativised semantics is that meaning of formulas becomes relativised to a subset of the set of all assignments. We call such a set the admissible assignments.

In what follows we will first define this relativised semantics. Then we see what intuitions one can develop about the set of admissible assignments. We finish with providing the connection with standard first order logic and establish a notion of bisimulation.

3.1 Admissible assignments

Assignments. Given a model (D, I), an assignment is a function from the set of variables into D. We assume our language has ω many variables v_{0}, v_{1}, …,. An assignment g can then be viewed as a sequence from ^{ω}D: g(i) then gives the value of v_{i} according to g.

To define the meaning of the existential quantifier, it is handy to create the following relation between assignments:

s ≡_{i} t iff for all j ≠ i: s(j) = t(j).  (1)

That is: two assignments s and t are ≡_{i} related iff they agree on all values of the variables except possibly for v_{i}. We can also define these relations for sets of variables v̄:

s ≡v̄ t iff for all j ∉ v̄: s(j) = t(j).  (2)

Using the relation ≡_{i}, we can give an alternative equivalent definition of the meaning of the existential quantifier. Given a model 𝔐 = (D, I) and an assignment s ∈ ^{ω}D, define

𝔐 ⊧ ∃v_{i}φ[s] ⟺ there exists a t ≡_{i} s such that 𝔐 ⊧ φ[t].

Let us now look at this definition from a modal perspective. We view the assignments as worlds and ≡_{i} as an accessibility relation. Then this definition is just the standard modal truth–definition of the “diamond” ∃v_{i}.

Given a first order model (D, I), the set of assignments (worlds) is uniquely determined: it is the set ^{ω}D. The theory we will develop below abandons this classical rigidness: we will allow other subsets of ^{ω}D to be set of “worlds” of our first order models.

Before we can start we have to solve a technical difficulty. First order logic satisfies the following appealing locality condition. It says that the meaning of a formula depends only on the model and the variables occurring free in the formula.

Fact 3.1 [Locality] Let φ be a first order formula. Let 𝔐 = (D, I) be a model, and s, t be two assignments such that s(i) = t(i) for all v_{i} ∈ FV (φ). Then

𝔐 ⊧ φ[s] if and only if 𝔐 ⊧ φ[t].

When we give first order logic a relativised semantics, locality does not necessarily hold, cf [1, 6]. We will give meaning to the existential quantifier using the dual of the relation ≡v̄. This relation was introduced into cylindric algebra theory by Y. Venema. On relativised models, this will ensure locality, and on standard models, the meaning of the existential quantifier is just the same. Define for s, t assignments, v̄ a set of variables,

s ≡∂ ; v̄ t iff for all v_{i} ∈ v̄ s(i) = t(i).  (3)

Admissible assignments. The key idea of relativised semantics for first order logic is that given a model 𝔐 = (D, I), only a subset of the set of all assignments ^{ω}D is available for the interpretation of the formulas. We will now provide the truth definition for a first order language relative to such an admissible set of assignments V ⊆ ^{ω}D. First we give meaning to terms: let s be an assignment, and 𝔐 = (D, I) a model. We define a function i from the set of terms into D as

i(t) = \{ \begin{matrix}I(t) & if t is a constant \\ s(i) & if t is the variable v_{i} \end{matrix}  (4)

Now for 𝔐 = (D, I) a model, and V ⊆ ^{ω}D a set of assignments, we define truth of a formula in 𝔐 relative to assignments in V. For s ∈ V,

𝔐 ⊧_{V} R(t_{1}, …, t_{n})[s] ⟺ (i(t_{1}), …, i(t_{n})) ∈ I(R)
𝔐 ⊧_{V} t_{1} = t_{2}[s]  ⟺ i(t_{1}) = i(t_{2})
𝔐 ⊧_{V} ¬φ[s]  ⟺ 𝔐 |̸=_{V} φ[s]
𝔐 ⊧_{V} φ ∧ ψ[s]  ⟺ 𝔐 ⊧_{V} φ[s] and 𝔐 ⊧_{V} ψ[s]
𝔐 ⊧_{V} ∃v̄φ[s]  ⟺ there exists a t ∈ V such that
s ≡_{FV (∃v̄φ)}^{∂} t and 𝔐 ⊧_{V} φ[t].

Note that the only difference with the definition in any textbook on first order logic is in the clause for the existential quantifier: the assignment t witnessing φ must be admissible, and we use the dual relation ≡^{∂}. For comparison, let us define ⊧_{V}^{c} —for “classical ⊧”, where all clauses are the same as for ⊧_{V} above, except the existential quantifier is defined as

𝔐 ⊧_{V}^{c} ∃v̄φ[s] ⟺ there exists a t ∈ V such that s ≡v̄ t and 𝔐 ⊧_{V}^{c} φ[t].

The next fact states that the two definitions are equivalent on classical models.

Fact 3.2 Let 𝔐 = (D, I) be a model and let V = ^{ω}D. Then for any s ∈ V, for any formula φ,

𝔐 ⊧_{V} φ[s] if and only if 𝔐 ⊧_{V}^{c} φ[s].

Proof. The only difference is in the meaning of the existential quantifier. That case goes through by the facts that locality holds on classical models and s ≡v̄ t implies that s ≡_{FV (∃v̄φ)}^{∂} t. qed

The next fact states that on relativised models, locality holds as well.

Fact 3.3 Let 𝔐 = (D, I) be a model and V ⊆ ^{ω}D a set of admissible assignments. For any formula φ, for any s, t ∈ V such that s ≡_{FV (φ)}^{∂} t (that is, s and t assign the same values to the free variables in φ):

𝔐 ⊧_{V} φ[s] if and only if 𝔐 ⊧_{V} φ[t].

Truth at non–admissible assignments. Given a model 𝔐 = (D, I) and a set of admissible assignments V ⊆ ^{ω}D, we have defined what it means for a formula to be true in 𝔐 at assignments in V. But what about the assignments in ^{ω}D \ V? The obvious way to do this for s ∈ ^{ω}D \ V is as follows,

𝔐 ⊧_{V} φ[s] ⟺ there exists t ∈ V such that t ≡_{FV (φ)}^{∂} s and 𝔐 ⊧_{V} φ[t].

Note that for formulas φ, 𝔐 ⊧_{V} φ[s] can still be undefined. If we assume that V is always non–empty, then for sentences however it is always defined. We now have two ways of defining truth in a model for sentences:

\begin{matrix}𝔐 ⊧_{V}^{1} φ & iff & (∀s ∈ ^{ω}D) : 𝔐 ⊧_{V} φ[s] \\ 𝔐 ⊧_{V}^{2} φ & iff & (∀s ∈ V) : 𝔐 ⊧_{V} φ[s]. \end{matrix}

For sentences, these two definitions give the same result:

Fact 3.4 For every model 𝔐, for every non–empty V ⊆ ^{ω}D, for every sentence φ,

𝔐 ⊧_{V}^{1} φ if and only if 𝔐 ⊧_{V}^{2} φ.

Since ⊧_{V}^{2} is more economical, we will use this notion from now on and delete the superscript.

Finally we define the notion of validity and of valid consequence. As usual we will overload the meaning of the symbol ⊧. Let Σ be a set of conditions on sets of admissible assignments. Let φ be a sentence and Γ a set of sentences. We define

⊧_{Σ} φ iff for every first order model 𝔐 = (D, I),
for every V ⊆ ^{ω}D satisfying Σ,𝔐 ⊧_{V} φ.
Γ ⊧_{Σ} φ iff for every first order model 𝔐 = (D, I),
for every V ⊆ ^{ω}D satisfying Σ, 𝔐 ⊧_{V} Γ implies 𝔐 ⊧_{V} φ.

3.2 Different relativisations

Above we have defined relativised semantics for any choice of V ⊆ ^{ω}D. In the literature several restrictions on V have been proposed.

Here we will show how one can define a set of admissible assignments from a tolerance relation on the domain of the model and from the notion of a context set [9]. Tolerances were introduced in the previous section. For 𝔐 = (D, I) a model, a context is just a subset of D. The intuitive meaning of a context X ⊆ D is

all elements in X can be perceived together by the speaker.

We will now define these notions and investigate their effects.

Let 𝔐 = (D, I) be a first order model. Suppose f : D × D ⟶ ℝ_{0}^{+} is a function associating with every pair of elements in the model a value, which we think of as the distance between the elements. We can then define δ(x, y) ⟺ f(x, y) ≤ d for some fixed positive d. If we assume that f(x, x) = 0, then δ satisfies

\begin{matrix}δ1 & (∀x ∈ D) : δ(x, x) \\ δ2 & (∀xy ∈ D) : (δ(x, y) → δ(y, x)). \end{matrix}

We call a relation δ ⊆ D × D satisfying these two requirements a tolerance on D.

Let C be a collection of subsets of D. Let C satisfy the following two conditions:

C 1 all singleton sets belong to C
C 2 C is closed under subsets.

If in addition C satisfies the following packed dense condition,

C P D if for all x, y ∈ X, {x, y} ∈ C , then also X ∈ C ,

we call C a context set. Tolerances and context sets are closely related.

Fact 3.5 (i) If δ is a tolerance on D, then the set C defined by

X ∈ C iff for all x, y ∈ X, δxy,

satisfies C 1, C 2 and C PD. (ii) If C ⊆ P(D) satisfies C 1, then δ defined by

δxy iff there exists a set X ∈ C such that {x, y} ⊆ X,

defines a tolerance on D. (iii) Tolerances and context sets are inter definable by the above definitions.

We now relate tolerances and context sets to sets of admissible assignments.

Definition 3.6 Let (D, I) be a model, and let δ be a tolerance and C a context set on (D, I). We define two sets of admissible assignments V_{δ} and V_{C} as the smallest subsets of ^{ω}D satisfying

s ∈ V_{δ} iff (∀i, j) : δ(s(i), s(j))
s ∈ V_{C} iff {s(i) | i ∈ ω} ∈ C ,

respectively.

The following fact is immediate by Fact 3.5.

Fact 3.7 Let (D, I) be a model, and let δ be a tolerance and C a context set on (D, I). Then V_{δ} = V_{C} .

Until now we have given only minimal requirements on the notions of context sets and tolerances. With our intended interpretation it makes sense to make them language–dependent as well (cf., the clues provided in Section 2).

The following extra conditions make sense in a language with constants. ¿From the perspective of a distance function, it says that the distance between any element and a named element is arbitrarily small.

δ3 (∀x ∈ D) : δ(x, I(m)) for all constants m
C 3 (∀x ∈ D) : {x, I(m)} ∈ C for all constants m.

A further restriction on δ (and hence C ) is to ask that the distance between two elements which stand together in a primitive relation is arbitrarily small. This would lead to the following extra conditions on δ and C :

δ4 (∀x, y ∈ D) : if (∃z_{1} … z_{k}(x = z_{i} ∧ y = z_{j} ∧ (z_{1}, …, z_{k}) ∈ I(R)

for some R, i, j, then δ(x, y).

C 4 (∀x, y ∈ D) : if (∃z_{1} … z_{k}(x = z_{i} ∧ y = z_{j} ∧ (z_{1}, …, z_{k}) ∈ I(R)

for some R, i, j, then {x, y} ∈ C .

We now look at the effect of the extra restrictions about constants and primitive relations on the logic. The condition δ3 does have an effect (of course only in languages with constants in the signature), while δ4 does not.

Fact 3.8 There exists a sentence which can be falsified on a model with a set of admissible assignments V_{δ} defined by a tolerance δ, but which holds on all models where V_{δ} is defined by a tolerance satisfying δ3.

Proof. Consider the first order tautology

[∀x∃yRxy ∧ ∀xyz((Rxy ∧ Ryz) → Sxz)] → ∃xySxy.

The counter model has the natural numbers as its domain, R is interpreted as successor, S = ∅ and δ is generated by the successor relation (that is δ(x, y) iff x = y or Rxy or Ryx holds). Clearly δ is a tolerance and the consequent fails on this model. To see that the antecedent holds, observe that for no assignment s ∈ V_{δ}, the range of s contains more than two elements. Thus the second conjunct in the antecedent cannot be falsified.

On the other hand, consider any model 𝔐 where V_{δ} is defined from a tolerance satisfying δ3. Assume the antecedent holds in 𝔐. Let a be the element named by some constant a. Then by the first conjunct, there exists a b ∈ D such that Rab. Let s be the assignment sending every variable to b. Then 𝔐 ⊧_{V} ∃yRby[s], whence there exists a c such that Rbc and δ(b, c) holds. But by δ3, also δ(a, b) and δ(b, c). But then {a, b, c} ∈ V_{δ}, whence by the truth of the second conjunct of the antecedent, Sac must hold. qed

For sentences, condition δ4 does not lead to extra validities.

Fact 3.9 For every sentence φ,

⊧_{{δ1,δ2,δ3}} φ if and only if ⊧_{{δ1,δ2,δ3,δ4}} φ.

The same holds when we disregard condition δ3.

Proof. From left to right is obvious. For the other direction, assume 𝔐 ⊧_{V} φ where V is defined from a tolerance not satisfying δ4. Change the valuation of the relation symbols such that δ4 holds as well, by deleting any tuple ā containing elements a_{i}, a_{j} which are not δ–related from the interpretation of every relation symbol. Call this model 𝔐′. But then still 𝔐′ ⊧_{V} φ, since to determine the truth of a sentence at an assignment in V_{δ} one only needs to consider assignments in V_{δ}. qed

Summing up. We have given several ways of defining relativised semantics. Now it is time to make a choice. In a language without constants this would be easy: we only allow admissible assignments defined from a tolerance δ. Then, just because it is handy, we can ask for condition δ4 as well, since it does not alter the logic anyway. With constants in the language we should make a decision about δ3. Since it seems a natural condition and it makes the logic stronger, we have chosen to include that as well. So from now on we only use relativised models where the set of admissible assignments is defined from a tolerance δ satisfying δ3 and δ4 (or equivalently, from a context set C which satisfies C 3 and C 4). ¿From now on a tolerance means a tolerance satisfying δ3 and δ4.

Definition 3.10 Let 𝔐 = (D, I) be a model, and δ ⊆ D × D. The relation δ is called a tolerance if it satisfies δ_{1}, δ_{2}, δ_{3} and δ_{4}.

3.3 Bisimulations

Explicit relativisations. Let 𝔐 = (D, I) be a model and C ⊂ P(D) a context set on it. Recall that the intuitive meaning of C was as follows:

X ∈ C if and only if all elements in X can be perceived together by the speaker.

The language does not have explicit means to state that two elements are perceived together. So we could add constants δ_{ij} for every i, j ∈ ω, and provide them with the following meaning. For any s ∈ ^{ω}D,

𝔐 ⊧ δ_{ij}[s] if and only if {s(i), s(j)} ∈ C .  (5)

Following Tarski, we call an operation logical if it’s truth is preserved under automorphisms. Clearly δ_{ij} is not a logical constant. But intuitively it should not be one in this sense. δ_{ij} indicates that the elements denoted by s(i) and s(j) are part of a group of elements which can be perceived together. Arbitrary automorphisms can destroy this intuitive meaning of δ_{ij}. On the other hand, the truth of δ_{ij} is preserved under automorphisms which respect C .

Fact 3.11 Let 𝔐 = (D, I) be a model and C ⊂ P(D) a context set on it. Let g be an automorphism of 𝔐 such that for any set X ⊆ D, X ∈ C if and only if {g(x) | x ∈ X} ∈ C . Then for any s ∈ ^{ω}D,

𝔐 ⊧ δ_{ij}[s] if and only if 𝔐 ⊧ δ_{ij}[g(s)].

Note that δ_{ij} is true on every s ∈ V_{C} , so on admissible assignments it is equivalent to ⊤. In particular the following equivalence holds.

𝔐 ⊧_{V_{C}} ∃v̄φ[s] if and only if 𝔐 ⊧_{V_{C}} ∃v̄(⋀{δ_{ij} | v_{i}, v_{j} ∈ FV (φ)} ∧ φ)[s].

What we just did is to make the implicit relativisation to admissible assignments in the meaning definition of the quantifiers explicit in the object language. This provides us with a translation to ordinary first order logic as follows.

Define recursively the following translation function (·)^{δ} from first order formulas to first order formulas. (·)^{δ} does nothing to atomic formulas, it commutes with the booleans and

(∃v̄φ)^{δ} = ∃v̄(⋀{δ(v_{i}, v_{j}) | v_{i}, v_{j} ∈ FV (φ)} ∧ φ^{δ}).

Here δ is just a binary predicate. As expected we have,

Fact 3.12 Let 𝔐 = (D, I) be a model and δ a tolerance on it. Then for every formula φ, for all s ∈ V_{δ},

𝔐 ⊧_{V_{δ}} φ[s] if and only if (D, I, \overline{δ}) ⊧ φ^{δ}[s].

Here \overline{δ} is defined as the set

{(x, y) ∈ D × D | x, y stand in the tolerance relation δ},

and forms the interpretation of the binary predicate δ.

Bisimulations and packed sets. Let (D, I) be a model and δ a tolerance on it. We call a set X ⊆ D δ–packed if δ(x, y) holds for all x, y ∈ X. Then V_{δ} —the set of admissible assignments defined from δ— is just the set of all sequences whose elements form a δ–packed subset of D. Using this we can define the appropriate notion of bisimulation for this logic. Note that the definition is very close to the one for the guarded fragment in [2].

Two pieces of notation come handy: define for s ∈ ^{ω}D,

R(s) = {s(i) | i ∈ ω}.

Also for g a function from D to D′, and s ∈ ^{ω}D, define

g(s) = that sequence in ^{ω}D′ such that for all i, g(s)(i) = g(i).

Definition 3.13 (Bisimulation) Let 𝔐 = (D, I) and 𝔑 = (D′, I′) be two models for the same signature. Let δ_{𝔐} and δ_{𝔑} be tolerances on them respectively. A family F of finite partial isomorphisms between D to D′ is called a δ–bisimulation if F satisfies the following conditions:

• if f ∈ F and g ⊆ f, then also g ∈ F

• (totality)

– for every δ–packed set X ⊆ D, there exists an f ∈ F whose domain is X

– similar for δ–packed subsets of D′

• (forth) if f ∈ F and dom(f) ⊆ X for some δ–packed set X, then there exists a g ∈ F which extends f and whose domain is X

• (back) a similar condition in the other direction.

Note that bisimulations are always non–empty, by totality and the fact that every singleton set is δ–packed. Of course we have the following

Fact 3.14 For every φ, for every 𝔐, 𝔑, for every δ–bisimulation F between them, for every f ∈ F, and for every assignment s such that R(s) = dom(f),

𝔐 ⊧_{V} φ[s] if and only if 𝔑 ⊧_{V} φ[f(s)].

Proof. The proof is by induction on formulas. We only consider the case for the existential quantifier. So let 𝔐 ⊧_{V} ∃v̄φ[s] and f ∈ F with dom(f) = R(s). The case when ∃v̄φ is a sentence is easy and left to the reader (use totality). So suppose otherwise. Then there exists a t ∈ V_{δ} such that t ≡_{FV (∃v̄φ)}^{∂} s and 𝔐 ⊧_{V} φ[t]. Let s′ be such that R(s′) = {s(i) | v_{i} ∈ FV (∃v̄φ)}. Then by locality also 𝔐 ⊧_{V} ∃v̄φ[s′]. Since F is closed under subsets, also f_{↾R(s′)} ∈ F. From t ≡_{FV (∃v̄φ)}^{∂} s it follows that R(s′) ⊆ R(t). Whence by forth, there exists a g ⊇ f_{↾R(s′)} with dom(g) = R(t). Thus by induction hypothesis, 𝔑 ⊧_{V} φ[g(t)]. But g ⊇ f_{↾s′} implies f_{↾R(s′)}(s′) ≡_{FV (∃v̄φ)}^{∂} g(t). Thus 𝔑 ⊧_{V} ∃v̄φ[f_{↾R(s′)}(s′)], whence by locality 𝔑 ⊧_{V} ∃v̄φ[f(s)]. qed

4 Packed fragment

In this section, we look for sentences whose truth in a model is unaffected by adding or deleting a tolerance. The syntactic characterisation of this fragment forms a slight generalisation of van Benthem’s loosely guarded fragment. We first define the fragment. We work in a standard first order language with equality with one restriction: terms are variables or constant symbols.

We say that a formula φ packs a set of variables {x_{1}, …, x_{k}} if φ is a conjunction of formulas of the form t_{i} = t_{j} or R(t_{1}, …, t_{n}) or ∃ȳR(t_{1}, …, t_{n}) such that for every x_{i} ≠ x_{j}, there is a conjunct in φ in which x_{i} and x_{j} both occur free.

In the definition of the packed fragment we use generalised quantifiers ∀x̄(φ, ψ) where x̄ = x_{1}, x_{2}, …, x_{n} is a sequence of variables. The meaning of this quantifier is nothing but the meaning of ∀x_{1} … ∀x_{n}(φ → ψ) in first order logic.

A generalised quantifier ∀x̄(φ, ψ) is called packed if φ packs all free variables of ψ. We call φ the guard of ∀x̄(φ, ψ). Note that if ψ contains only one free variable, then the first argument of the universal quantifier can be anything: packedness only speaks about pairs of variables.

The packed fragment is defined as follows: a packed formula is constructed from atoms using the booleans and packed universal quantification ∀x̄(φ, ψ), where ψ must be a packed formula.

It will be useful to define two more fragments. A packed existential quantification is nothing but ¬∀v̄(φ, ¬ψ), where ∀v̄(φ, ¬ψ) is a packed universal quantification (i.e., it is of the form ∃v̄(φ ∧ ψ), where φ packs all free variables of ψ).

The ∀–packed fragment is defined as follows: formulas are constructed from atoms and their negations using ∧, ∨, ∃ and packed universal quantification ∀x̄(φ, ψ), where ψ must be a ∀–packed formula. The ∃–packed fragment is defined dually: so we may use unpacked ∀, but only packed ∃.

The three fragments are of course closely related

Fact 4.1 A first order sentence φ is equivalent to a packed sentence if and only if it is equivalent to a ∀– and a ∃–packed sentence.

We will now related the packed fragment to relativised semantics. One direction is obvious, and observed in [8].

Fact 4.2 The translation (·)^{δ} goes to the packed fragment.

Just as all first order sentences are invariant for δ–bisimulations when they are interpreted relativised to a set of admissible assignments, all packed sentences are invariant for δ–bisimulations when they are classically interpreted.

Definition 4.3 A sentence φ is invariant for δ–bisimulations if for all models 𝔐, 𝔑, for all tolerances δ_{𝔐}, δ_{𝔑}, and for all δ–bisimulations F: 𝔐 ≃_{F} 𝔑,

𝔐 ⊧ φ if and only if 𝔑 ⊧ φ.

Fact 4.4 All packed sentences are invariant for δ–bisimulations.

Proof. Let 𝔐, 𝔑 be models, δ_{𝔐}, δ_{𝔑} tolerances and F: 𝔐 ≃_{F} 𝔑 a δ– bisimulation. We show by induction that for every packed formula φ, for every f ∈ F, and for every assignment s such that R(s) = dom(f),

𝔐 ⊧ φ[s] if and only if 𝔑 ⊧ φ[f(s)].

Then the result follows by the non–emptyness of δ–bisimulations.

The inductive proof goes through for the atomic cases because the functions in F are partial isomorphisms. The boolean cases are trivial. For packed existential quantification we reason as follows. Let us call an assignment s small for φ if (∀x ∉ FV (φ))(∃y ∈ FV (φ)) : s(x) = s(y). Suppose 𝔐 ⊧ ∃x̄(φ, ψ)[s]. By locality we may assume that s is small for ∃x̄(φ, ψ). Then there exists a t ≡x̄ s such that 𝔐 ⊧ φ ∧ ψ[t]. Again we may assume that t is small for φ ∧ ψ. Since φ packs all free variables of ψ, the set R(t) is packed by δ_{𝔐}. Moreover R(s) ⊆ R(t) because both are small. But then by forth, there exists a g ∈ F extending f whose domain is R(t). Thus by inductive hypothesis 𝔑 ⊧ φ ∧ ψ[g(t)], and finally 𝔑 ⊧ ∃x̄(φ, ψ)[f(s)], since g extends f. qed

Facts 3.12 and 4.2 show that on any model 𝔐, and any relativisation defined by a tolerance δ, the question whether 𝔐 ⊧_{V} φ[s] is equivalent to the question whether the packed formula φ^{δ} is classically satisfied in 𝔐 at s. The other direction was shown in [5], to give an alternative proof of the decidability of the loosely guarded fragment. The following fact is a generalisation of that result. It reduces the question of first order satisfiability of ∀–packed formulas to that of relativised satisfiability. We present the fact and its proof here since the construction used in the proof is typical for the packed fragment, and will later be used to give a semantic characterisation of it.

Fact 4.5 Every ∀–packed formula is classically satisfiable iff it is satisfiable on a relativised model.

Proof. ¿From left to right is obvious, just take the tolerance to be the universal relation. For the other direction, let 𝔐 = (D, I) be a model, δ a tolerance on D and suppose 𝔐 ⊧_{V_{δ}} φ. We prove by induction for every s ∈ V_{δ}, for every formula ψ,

(∗) 𝔐 ⊧_{V_{δ}} ψ[s] ⇒ 𝔐 ⊧ ψ[s],

from which the result follows. For literals and formulas of the form ∃x̄(R(t_{1}, … t_{k})) (∗) holds in both directions. For ∧, ∨ and ∃, the proof is trivial.

For the universally quantified formulas, suppose 𝔐 |̸= ∀v̄(φ, ψ)[s]. Then there exists a t ≡v̄ s such that 𝔐 ⊧ φ[t] but 𝔐 |̸= ψ[t]. By locality we may assume that R(t) = {t(i) | v_{i} ∈ FV (φ → ψ)}. Since φ packs all free variables of ψ, R(t) is δ–packed (since we assume condition δ4), so t ∈ V_{δ}. Then 𝔐 ⊧_{V_{δ}} φ[t], since (∗) holds in both directions for all conjuncts of φ. An application of the induction hypothesis leads to 𝔐 |̸=_{V_{δ}} ψ[t]. Whence 𝔐 |̸=_{V_{δ}} ∀v̄(φ, ψ)[s], because s ≡_{FV (∀v̄(φ,ψ))}^{∂} t holds as a consequence of s ≡v̄ t. qed Because he satisfaction problem for first order formulas on relativised models is decidable [5], we obtain

Corollary 4.6 The satisfaction problem for ∀–packed formulas is decidable.

The reader familiar with modal logic might recognise a basic construction from modal logic. If we view the elements of V_{δ} as worlds, then essentially we added worlds to the model. The reverse action would correspond roughly to the generated submodel construction from modal logic. Reading the last proof dually, it shows that ∃–packed sentences are preserved under adding a tolerance and interpreting sentences in a relativised manner. Formally,

Definition 4.7 Let 𝔐 = (D, I) be a model, and δ any tolerance on D. We say that a first order sentence φ is preserved under δ–relativisation if 𝔐 ⊧ φ in the classical sense only if 𝔐 ⊧_{V_{δ}} φ. A sentence φ is invariant for δ–relativisation if 𝔐 ⊧ φ in the classical sense if and only if 𝔐 ⊧_{V_{δ}} φ.

The last proof showed the following preservation result.

Fact 4.8 The ∃–packed fragment is preserved under δ–relativisation.

The converse of this preservation result does not hold. In fact this is to be desired since

Fact 4.9 The validity problem for the first order fragment preserved under δ–relativisation is undecidable.

Proof. Consider arrow logic interpreted on relativised pair–frames, and expand it with a coordinate wise difference operator D_{1}, with the following meaning, interpreted on a model with relativised domain V:

𝔐 ⊧ D_{1}φ(x, y) iff there exists a (x, z) ∈ V and z ≠ y and 𝔐 ⊧ φ(x, z).

This logic is introduced in [5] and shown to be undecidable. It is easy to check that the range of the translation of this logic to first order logic is preserved under δ–relativisation. qed

Corollary 4.10 The ∃–packed fragment does not capture all first order sentences preserved under δ–relativisation.

Proof. An ∃–packed sentence is valid iff its negation (which is equivalent to a ∀–packed sentence is not satisfiable. By Fact 4.5 and the fact that the satisfaction problem for relativised semantics is decidable, the validity problem for ∃–packed sentences is decidable. This contradicts Fact 4.9. qed

We come to the central result of this paper: a semantic characterisation of the packed fragment in terms of relativised semantics.

Theorem 4.11 Let φ be a first order sentence. The following are equivalent. (i) φ is equivalent to a packed sentence. (ii) φ is invariant for δ–bisimulation. (iii) φ is invariant for δ–relativisation.

Proof. From (i) to (ii) was shown in Fact 4.4. From (ii) to (iii) is immediate since every model δ–bisimulates with itself for every tolerance defined on it. For the proof of (iii) implies (i), we use a “diagram–chasing” argument well–known from van Benthem’s work (see e.g., [7, 8]).

Let φ be a sentence which is invariant under δ–relativisation. Define P F (φ) as the set of all packed sentences (in the same signature as φ) which classically follow from φ. We will show that P F (φ) ⊧ φ, from which the result follows by compactness. If P F (φ) is inconsistent, there is nothing to prove. So let 𝔐 = (M, I) be a model for P F (φ), in the signature of φ. We will show that 𝔐 ⊧ φ. Consider the complete packed theory P F (𝔐) of 𝔐, together with φ. This set of sentences is finitely satisfiable by a simple argument. Thus by compactness it has some model 𝔑 = (N, I′). Again we can equate the signature of 𝔑 with the signature of φ.

Now take ω–saturated extensions 𝔐^{+} and 𝔑^{+}, respectively. Let δ_{𝔐} (δ_{𝔑}) be the smallest tolerance which can be defined on 𝔐^{+} (𝔑^{+}). Since 𝔐 and 𝔑 have the same finite signature, on the extensions δ can be defined as a finite disjunction of terms of the form

t_{i} = t_{j}, R(t_{1}, …, t_{n}), and ∃v̄R(v̄, v_{i}, v_{j}).  (6)

Since packed formulas are invariant under δ–relativisation, and φ as well, we have

𝔐^{+} ⊧_{V_{δ_{𝔐}}} P F (φ) and 𝔑^{+} ⊧_{V_{δ_{𝔑}}} P F (𝔐) ∪ {φ}.

We call finite δ–packed sets X ⊆ M^{+}, Y ⊆ N^{+} δ–relativised equivalent if there exists a bijection f : X ⟶ Y, and for some s ∈ ^{ω}M^{+}, such that R(s) = X, we have

for all formulas φ, 𝔐^{+} ⊧_{V_{δ_{𝔐}}} φ[s] ⟺ 𝔑^{+} ⊧_{V_{δ_{𝔑}}} φ[f(s)].  (7)

Claim 1 The relation of δ–relativised equivalence is a δ–bisimulation between the models 𝔐^{+} and 𝔑^{+}, with tolerances δ_{𝔐} and δ_{𝔑}, respectively.

Proof of Claim. Obviously, the relation is closed under subsets. The proof that it is total needs some extra argumentation. First observe that by Fact 3.12,

(7) is equivalent to

for all formulas φ, 𝔐^{+} ⊧ φ^{δ}[s] ⟺ 𝔑 ⊧^{+} φ^{δ}[f(s)],  (8)

where (·)^{δ} is the translation function defined just above Fact 3.12. But since δ is the smallest tolerance, for every two variables v_{i}, v_{j}, δ(v_{i}, v_{j}) is equivalent with a disjunction of formulas of the form given in (6). But then, using distributivity of ∨ over ∧ and of ∨ over ∃v̄, every formula φ^{δ} can be equivalently written as a packed formula in the φ-signature. Whence (8) is equivalent to

for all packed formulas φ, 𝔐^{+} ⊧ φ[s] ⟺ 𝔑^{+} ⊧ φ[f(s)].  (9)

But now the standard argument can be applied. Let X ⊆ M^{+} be some finite δ–packed set, with |X| = n. Let s ∈ ^{ω}M^{+} be such that R(s) = X. Let P F (s) be the set of packed formulas true at s in 𝔐^{+}. Then for every finite subset Ψ of P F (s), 𝔐^{+} ⊧ ∃v_{1} … v_{n}(φ, ⋀ Ψ), where φ describes how X is packed. Note that this is a packed sentence. So it also holds in 𝔐, whence also in 𝔑+. But then, by ω–saturation, P F (s) is satisfied in 𝔑^{+} at some t. Then R(t) is the required witness.

The other direction of totality uses a symmetric argument. The back and forth clauses are now proved similarly, again exploiting the fact that the models are saturated. ◀

Now we are almost finished. Since 𝔑^{+} ⊧_{V_{δ_{𝔑}}} φ, by Fact 3.14, 𝔐^{+} ⊧_{V_{δ_{𝔐}}} φ, whence since φ is invariant for δ–relativisation, also 𝔐^{+} ⊧ φ. Whence, since 𝔐 is an elementary submodel of 𝔐, 𝔐 ⊧ φ, as required. qed

5 Conclusion

Theorem 4.11 provides us with a semantic characterisation of the packed fragment. Moreover it indicates a strong connection between the packed fragment and relativised semantics. The packed fragment forms precisely the set of first order sentences for which it does not matter whether they are interpreted classically or relativised on a model.

Another perspective on the packed fragment is obtained by analogy with modal logic. In describing the difference between first order logic and modal logic, modal logicians often first come up with the fact that truth is determined locally in modal logic. What is meant is that truth of a modal formula at some state s only depends on the states which are finitely accessible from s. In other words, truth at s is invariant for adding or deleting states which are not accessible from s. Put differently, modal formulas are invariant under generated submodels.

Relativisation implements this modal “local evaluation” in first order logic by relativising the meaning of the quantifiers to admissible assignments. In modal terminology: in a model (D, I), every assignment s ∈ ^{ω}D is accessible to every other assignment t ∈ ^{ω}D; relativisation restricts the number of accessible assignments to the admissible ones, and thus localises first order logic. ¿From this perspective, Theorem 4.11 tells us that the packed fragment is the “local” fragment of first order logic. Whence, if we are willing to equate local with modal, it states that the packed fragment is the true modal fragment of first order logic.

References

[1] N. Alechina. Modal quantifiers. PhD thesis, Institute for Logic, Language and Computation, University of Amsterdam, 1995. ILLC Dissertation Series 1995–20.

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

[3] J. Groenendijk and M. Stokhof. Dynamic predicate logic. Linguistics and Philosophy, 14:39–100, 1991.

[4] J. Groenendijk, M. Stokhof, and F. Veltman. Coreference and modality. In S. Lappin, editor, The Handbook of Comtempory Semantic Theory, pages 179–213. Blackwell, 1996.

[5] M. Marx. Complexity of modal logics of relations. Technical Report ML– 97–02, Institute for Logic, Language and Computation, University of Amsterdam, May 1997.

[6] I. Németi. A fine-structure analysis of first-order logic. In M. Marx, L. Pólos, and M. Masuch, editors, Arrow Logic and Multimodal Logics, Studies in Logic, Language and Information, pages 221–247. CSLI Publications, Stanford, 1995.

[7] J. van Benthem. Modal Logic and Classical Logic. Bibliopolis, Naples, 1983.

[8] J. van Benthem. Exploring Logical Dynamics. Studies in Logic, Language and Information. CSLI Publications, Stanford, 1996.

[9] D. Westerstahl. Determiners and context sets. In J. van Benthem and A. ter Meulen, editors, Generalized Quantifiers and Natural Language, pages 45– 71. Foris, Dordrecht, 1985.