Tangled Modal Logic for Spatial Reasoning

1 Introduction

The archetypical modal logic of space is S4, given its topological interpreation dating back to Tarski and others [Tarski, 1938] and its renewed interest for modeling spatial reasoning: see for example [Artemov et al., 1997; Mints and Zhang, 2005; van Benthem and Bezhanishivili, 2007]. This logic is also sound and complete for the class of transitive, reflexive Kripke models.

Recently, two papers have suggested that, when dealing with transitive models, the basic modal language strikes a more natural balance in terms of expressive power when enriched with a certain polyadic operator. On a finite model, this operator allows us to describe the existence of clusters satisfying given sets of formulas.

It should be noted that the motivations for the two papers are entirely distinct. The first is [Dawar and Otto, 2009], which is quite general and characterizes the modal language over many classes of frames. However, when considering transitive frames which are not necessarily partial orders, they found it useful to add formulas of the form ♦∗pϕ expressing what we call the 'tangled closure' operation. They call the extended systemML∗ and obtain the following:

∗This research is partially supported by the IALNoC project HUM-5844 of the Junta de Andaluc´ıa

Theorem (Dawar and Otto, 2007). ML∗ is expressively equivalent to the bisimulation-invariant fragments of both first-order logic and monadic second-order logic over the class of finite S4 models. 1

This is only one of many results of this nature proven in [Dawar and Otto, 2009], but it is the most relevant for our discussion.

The other paper is [Fern´andez-Duque, 2011], which uses a very similar language L♮ . It considers the question of definability of simulability. A simulation is defined like a bisimulation satisfying the 'forth' but not necessarily the 'back' clause. We say that a pointed model 〈W, w〉 simulates 〈V, v〉 if there is a simulation S between them such that w S v.

The main results presented there are:

Theorem (Fern´andez-Duque, 2011). There exists a finite, pointed model 〈W,w〉 such that the property of being simulated by 〈W, w〉 is not definable in the basic modal language over the class of finite S4 models.

However, in L♮ , the property of being simulated by a finite model 〈W,w〉 is always definable, even over the class of all S4 models (including topological models).

We have expressed these results in the notation of the original sources, but the system S4∗ that we shall use is a notational variant of both ML∗ and L♮ and hence they are all interchangeable as far as expressivity is concerned. In fact, our formal language is a straightforward simplification of ML∗ exploiting the fact that we are restricting attention to S4 models.

In ML∗ , formulas of the form ♦∗Γ are added to the basic modal language 2 , where Γ is a finite set of formulas. The language we propose for S4∗ differs from that of ML∗ in two ways:

1 The original result demands that the models be 'tree-like' but every model is bisimilar to a tree-like model.

2 More specifically, [Dawar and Otto, 2009] introduces formulas of the form ♦∗pϕ, where p is a finite set of formulas, and goes on to suggest ♦∗ (γ0, ..., γn) as an alternative notation.

1. We drop the standard modal operator ♦ and include only the polyadic ♦∗ . This is justified because, over the class of S4 models, the standard ♦γ is equivalent to ♦∗ {γ}.
2. Given that we no longer need to distinguish between ordinary and poliadic operators, we omit the star and write ♦Γ instead of ♦∗Γ.

This will allow us to give standard and polyadic modalities a uniform treatment and make complex formulas easier to read. However, we should stress that S4∗ is essentially the restriction of ML∗ to S4 models.

The formula ♦Γ is then interpreted as the tangled closure of the valuations of the elements of Γ. This is a modification of the 'tangle' operator from [Fern´andez-Duque, 2011] obtained, in topological terms, by taking the closure of the latter. It is identical to the operation used in interpreting ♦∗ in [Dawar and Otto, 2009], although there it is not described topologically.

We call the resulting system S4∗ . Our objective is to give it a sound and complete axiomatization. There are some general completeness results available for related systems, but to the best of our knowledge, none of these results implies the completeness of S4∗ .

Since the tangled closure can be expressed as a fixpoint operator, S4∗ can be seen as a subsystem of the μ-calculus [Kozen, 1983]. Kozen suggests an axiomatization which is proven complete in [Walukiewicz, 2000]. However, the proof uses complex syntactic manipulations which are not available in our more restrictive language.

Meanwhile, [Santocanale and Venema, 2010] considers a fragment of the μ-calculus which does not allow alternation between least- and greatest-fixpoints. They obtain a family of languages which, syntactically, generalize the language of S4∗ and define appropriate logics for these systems which are proven complete. However, they only consider the class of K models. While an S4 modality could be defined in the μcalculus using the transitive, reflexive closure of the accessibility relation, the polyadic version requires alternation between a least- and a greatest-fixpoint, which is not permitted in the context of flat fixpoints.

Because of this we must prove completeness from scratch, borrowing only from the completeness of the modal logic S4.

2 The tangled closure operator

The language we will consider allows us to express the tangled closure of sets in a Kripke model.

Recall that a (transitive, reflexive) Kripke frame is a pair 〈W, ≼〉 where W is a set and ≼ a (transitive, reflexive) binary relation on W .

We will also use the notation w ≺ v for w ≼ v but v ̸≼ w and w ∼ v for w ≼ v and v ≼ w.

Transitive reflexive frames can be seen as topological spaces if we consider open sets to be downward-closed sets under ≼. Although we will not work directly with topology in this paper this is the motivation for the term tangled closure, which can also be seen as a generalization of the standard topological closure.

Definition 2.1 (Tangled closure). Let 〈W,≼〉 be a Kripke model and S ⊆ 2W . We define S to be the union of all sets E ⊆ W such that, for all S ∈ S and w ∈ E, there is v ≼ w with v ∈ E ∩ S. 3

The tangled closure is a straighforward generalization of the closure of a single set; namely, S = {S}. Thus we will maintain the symbol ♦, but allow sets of formulas under its scope. We consider the language L∗ , where ♦ acts on finite sets of propositions of arbitrary size; that is, if γ0, ..., γn are formulas of L∗ then so is ♦{γ0, ..., γn}. We will use L to denote the standard modal language, i.e., the fragment of L∗ where all occurrences of ♦ are monadic.

Formally, our grammar is built from a countable set of propositional variables PV; if ϕ, ψ are formulas then ¬ϕ, ϕ∧ ψ are formulas and, if Γ ⊆ L∗ is finite, then ♦Γ is also a formula.

A Kripke model is a Kripke frame 〈W,≼〉 equipped with a valuation llbracket·rrbracket : L∗ → 2W such that 4 llbracket¬αrrbracket = W \ llbracketαrrbracket, llbracketα ∧ βrrbracket = llbracketαrrbracket ∩ llbracketβrrbracket and

Note that ♦Γ can be defined in the μ-calculus in terms of the unary ♦ by

In general, we will write ♦γ instead of ♦{γ}. We also write □Γ as a shorthand for ¬♦¬Γ, where ¬Γ is to be understood as {¬γ : γ ∈ Γ}.

We will only be dealing with finite models in this paper, and in this setting the meaning of ♦Γ becomes much simpler. 5

Recall that a cluster in a Kripke frame 〈W, ≼〉 is a set C ⊆ W such that, for all v, w ∈ C, v ∼ w; every world w belongs to a unique cluster, which we denote [w].

Lemma 2.1. If 〈W,≼, llbracket·rrbracket〉 is a finite S4 model and w ∈ W, w ∈ llbracket♦Γrrbracket if and only if there is v ≼ w such that, for all γ ∈ Γ there is u ∼ v with u ∈ llbracketγrrbracket.

Proof. If w ∈ llbracket♦Γrrbracket, pick v ≼ w such that v is minimal among all worlds satisfying ♦Γ. Then, by the definition of the tangled closure for every γ ∈ Γ there is u ≼ v with v ∈ llbracketγrrbracket, but by minimality this implies that u ∼ v.

For the other direction, if there is v ≼ w such that, for all γ ∈ Γ there is u ∼ v with v ∈ llbracketγrrbracket, it is clear that {w} ∪ [v] satisfies the fixpoint property defining the tangled closure.

3 For readers familiar with [Fern´andez-Duque, 2011], we have that S = S ♮ , and similarly S ♮ = S ∩ ⋃ S.

4 Note that we use ≼ conversely to many authors in the definition of ♦; here, w satisfies ♦γ if some v ≼ w satisfies γ.

5 Note, however, that our system is also sound for the class of arbitrary S4 models; the results proven here show that it is also complete and has the finite model property.

3 Polyadic S4

Our proposed axiomatization for S4∗ consists of the following:

Taut All propositional tautologies.

Axioms for ♦:

Rules:

MP Modus ponens

Subs Substitution

This system is sound for the class of S4 Kripke models and, more generally, for the class of all topological models. Although we focus on finite models in this paper, we shall state this in its more general form:

Theorem 3.1. If S4∗ ⊢ ϕ, then ϕ is valid on the class of all topological S4 models.

Proof. It suffices to check that all axioms and rules preserve validity. For simplicity we shall restrict our proof to finite S4 models. Most cases should be familiar, except for those involving the polyadic modality, and we shall only consider these.

T Suppose 〈W, ≼, llbracket·rrbracket〉 is a model with w ∈ llbracket∧ Γrrbracket.

Then, using Lemma 2.1, it is enough to observe that [w] satisfies all formulas in Γ, since w itself does. Hence w ∈ llbracket♦Γrrbracket, as desired.

• 4 Suppose that w satisfies ♦♦Γ; then there is u ≼ w satisfying ♦Γ, and thus v ≼ u such that [v] satisfies Γ. But by transitivity v ≼ w, so w satisfies ♦Γ.

Fix This is the fixpoint condition satisfied by the tangled closure.

Ind Suppose w satisfies the antecedent, so that there is v ≼ w satisfying

We can assume v is ≼-minimal among such worlds, given that we are working over finite models.

Then, for any γ ∈ Γ, v satisfies ♦(p ∧ γ), so that there is u ≼ v satisfying p ∧ γ. By transitivity we have that u satisfies □(p → ∧γ∈Γ ♦(p ∧ γ)); but v is minimal among such worlds and hence we have that u ∼ v.

Hence we can use Lemma 2.1 to conclude that w satisfies ♦Γ.

The remainder of this paper will be devoted to proving that S4∗ is also complete. The symbol ⊢ refers to derivability in this system unless specified otherwise.

4 Typed models

We define a type to be a finite set of formulas. For a type Φ, define sub±(Φ) as the set of all formulas which are either subformulas of some ϕ ∈ Φ or of the form ¬ψ, where ψ does not begin with a negation and is a subformula of some ϕ ∈ Φ. It is to be understood that all γ ∈ Γ are subformulas of ♦Γ.

Definition 4.1 (Saturation). Say a set of formulas Φ is saturated if , whenever ϕ ∈ Φ and ψ is a subformula of ϕ which does not begin with a negation, then either ψ ∈ Φ or ¬ψ ∈ Φ.

Ψ is a saturation of Φ if Ψ is saturated and Ψ ⊆ sub±(Φ). We denote the set of saturations of Φ by sat(Φ), and the set of consistent saturations of Φ by cons(Φ).

Lemma 4.1. If Φ is a consistent type, then Φ has a consistent saturation.

Proof. By propositional reasoning we have that Φ ⊢ ∨Ψ∈sat(Φ) ∧ Ψ; if Ψ is inconsistent ⊢ ¬ ∧ Ψ, so again by propositional reasoning we can remove all such disjuncts and obtain Φ ⊢ ∨Ψ∈cons(Φ) ∧ Ψ.

But then cons(Φ) must be non-empty, otherwise it would follow that Φ is inconsistent.

Given a set of formulas Φ, we write Φ♦ for the set of formulas in Φ of the form ♦Γ and Φ♦□ for the set of formulas of Φ either of the form ♦Γ or □Γ. We say a type Φ is modal if Φ = Ψ♦□ for some Ψ, and saturated modal if Φ = Ψ♦□ for some saturated Ψ.

We will work with typed models, which are very similar to ordinary models which include additional syntactic information. For these models to be typed correctly, it is useful to introduce the notion of a task.

Definition 4.2. Say a type Σ of the form {♦Γ} ∪ {□Δ : Δ ∈ D} is a task.

A set C of saturations of Σ realizes Σ if (1) Γ ⊆ ⋃ C; (2) Ψ♦□ = Θ♦□ whenever Ψ,Θ ∈ C and (3) for all Δ ∈ D, there is δ ∈ Δ such that δ ∈ ⋂ C.

With this we can now define our typed models:

Definition 4.3 (typed model). We define a typed model

as a finite preorder 〈|w|, ≼w〉 with a function tw assigning a saturated type to each w ∈ |w| and such that:

• for every w ∈ |w| and ♦Γ ∈ tw(w) we have that either {♦Γ} ∪ t□w(w) is realized by tw([w]) or else there is v ≺w w such that ♦Γ ∈ tw(v) and
• if □Δ ∈ tw(w), ♦¬Δ is not realized by tw(w) and, for all v ≼w w, □Δ ∈ tw(v).

In the above definition, t([w]) = {t(v) : v ∼ w}.

A typed model gives rise to a model ˙w in the obvious way, by setting llbracketprrbracket ˙w = {w ∈ |w| : p ∈ tw(w)} .

We then have that:

Lemma 4.2. If w is a typed model, w ∈ |w| and ϕ is any formula, ϕ ∈ tw(w) implies that w ∈ llbracketϕrrbracket ˙w .

Proof. We omit the proof, which proceeds by a standard induction on formulas.

So in order to show that a formula is satisfiable, it suffices to construct a typed model that satisfies it.

Often we will want to construct a typed models from smaller pieces. Here we define the basic operation we will use to do this, and establish the conditions that the pieces must satisfy. In the following definition, ∐ denotes the disjoint union of sets.

Definition 4.4. Let G be a set of saturated types and ⃗v = 〈vi〉i<I a sequence of typed models.

Define a structure w = G ⊕ ⃗v by setting

and

Not all constructions of the form G⊕⃗v yield typed models; for this they must satisfy the following condition:

Figure 1: If G = {Γj}j<J and ⃗v = 〈vi〉i≤I , G ⊕ ⃗v has a cluster typed by G at the root and each vi as a submodel.

Definition 4.5 (coherence). Let G be a set of types and ⃗v = 〈vi〉i<I a sequence of typed models.

The pair 〈G, ⃗v〉 is coherent if

• whenever ♦Γ ∈ G, either Γ ⊆ ⋃ G or some vi satisfies ♦Γ and
• whenever □Δ ∈ G, ¬Δ ̸⊆ ⋃ G and every world in every vi satisfies □Δ.

The notion of coherence is useful because of the following:

Lemma 4.3. Let G be a set of types and⃗v a sequence of typed models.

Then, G⊕⃗v is typed model if and only if 〈G, ⃗v〉 is coherent.

From here on, our goal is to show that consistent types have typed models. Whenever possible, we will isolate reasoning that can be done within S4 to take advantage of the familiar completeness result for this logic; an example of this is the following lemma.

Lemma 4.4. If G is a finite set of types and ψ is any formula, then

Proof. Without loss of generality we can assume that all formulas are in the basic modal language, considering all polyadic occurrences of ♦Γ as propositional variables. Since S4 is complete for finite preordered models, it suffices to show that the formula is valid over this class.

Suppose that W is a finite S4 model satisfying

on some world w, so that there is v ≼ w satisfying

Now pick u ≼ v which is minimal among all worlds satisfying ψ. Since u satisfies ∨Γ∈G ∧γ∈Γ ♦γ, u satisfies ∧γ∈Γ0 ♦γ for some Γ0 ∈ G. Because u is minimal, if u′ ≼ u also satisfies ψ, then u′ ∼ u and hence u′ satisfies ∧γ∈Γ0 ♦γ.

But this shows that u satisfies ψ ∧□(ψ → ∧γ∈Γ0 ♦γ), so w satisfies ∨

as desired.

Lemma 4.5. If Θ is a modal type and

then Θ is inconsistent. 6

then

which by Lemma 4.4 implies that

But then we can apply Ind(θ) to get

which shows that Θ is inconsistent, given that ♦¬Γ is the negation 7 of □Γ.

6 We use Θ ⊢ ϕ merely as a shorthand for ⊢ ∧ Θ → ϕ.

7 Strictly speaking one must show here that ♦Γ ↔ ♦¬¬Γ is derivable, but this can be done by noting that each satisfies the other's fixpoint property.

Lemma 4.6. A saturated type Ψ is satisfiable if and only if, for all □Δ ∈ Ψ, Δ ̸⊆ Ψ and, for all ♦Γ ∈ Ψ, {♦Γ} ∪ Ψ□ is satisfiable.

Proof. For each ♦Γ ∈ Ψ let vΓ be a state satisfying ♦Γ ∧ ∧ Ψ□.

Then, by Lemma 4.3, w = {Ψ} ⊕ 〈vΓ : ♦Γ ∈ Ψ〉 is a model satisfying Ψ, as desired.

Definition 4.6. Suppose that ⃗Σ = 〈Σi〉i<I and ⃗Θ = 〈Θj 〉j<J are finite sequences of types.

A choice function on ⃗Σ is a sequence 〈σi〉i<I such that σi ∈ Σi for all i < I.

We say that ⃗Σ covers ⃗Θ if, given any choice function ⃗σ on ⃗Σ, there is j < J such that, for every θ ∈ Θj, there is i < I for which σi → θ is a tautology.

Lemma 4.7. If ⃗Σ covers Θ, then

Proof. Once again we can, without loss of generality, assume that all formulas are in the basic modal language. It suffices to show that the formula is valid over the class of finite S4 models.

Let 〈W, ≼, llbracket·rrbracket〉 be any S4 model and suppose w ∈ W satisfies

Then, for every i < I there is vi ≼ w such that vi satisfies ∨σ∈Σi σ, and hence there is some σi ∈ Σi such that vi satisfies σi. This gives us a choice function ⃗σ.

Now, because ⃗Σ covers ⃗Θ, there is j < J such that for all θ ∈ Θj there is i < I such that σi → θ is a tautology, hence vi satisfies θ. It follows that w satisfies ♦θ, and since θ ∈ Θj was arbitrary we have that w satisfies ∧θ∈Θj ♦θ, so it satisfies

as desired.

Lemma 4.8. If a task Σ is unrealizable, then it is inconsistent.

Proof. Let

For each γ ∈ Γ let

and let Cγ be the set of all formulas of the form ∧ Θ, where Θ is a consistent saturation of Σγ.

We claim that if Σ is unrealizable, then 〈Cγ : γ ∈ Γ〉 covers D; indeed, suppose otherwise.

Following the definition of cover, this means that there exist 〈Θγ : γ ∈ Γ〉 such that ∧ Θγ ∈ Cγ and for every Δ ∈ D there is δ ∈ Δ such that ∧ Θγ → δ is not a tautology for any γ, which in particular implies that δ ̸∈ Θγ.

Then, 〈Θγ : γ ∈ Γ〉 clearly realizes Σ, contradicting our assumption.

But by Lemma 4.7 we then have that

which by Lemma 4.5 implies that Σ is inconsistent.

Lemma 4.9. If a modal type Ψ is consistent, it is satisfiable.

Proof. Assume that Ψ is consistent.

We work by induction on #Ψ♦; that is, suppose that for any Θ with #Θ♦ < #Ψ♦, Θ is satisfiable if and only if it is consistent.

Let C be the set of all Γ such that ♦Γ ∈ Ψ and there is no consistent saturated type Θ with ♦Γ ∈ Θ♦ ⊊ Ψ♦ and Ψ□ ⊆ Θ.

Let D be the set of all Δ with □Δ ∈ Ψ.

First we note that, for Σ ∈ C we have

indeed, for any Γ ∈ C distinct from Σ,

is inconsistent by our induction hypothesis.

We now claim that

It suffices to check that the antecedent satisfies the fixpoint property of ♦ ⋃ C; but if γ ∈ ⋃ C, then γ ∈ Σ for some Σ ∈ C, hence by Fix

and together with 1 this implies that

which is precisely the fixpoint condition of ♦ ⋃ C.

Now, by Lemma 4.8 we have that

is realizable by some set of types G (since it cannot be inconsistent); once again, by induction on #Ψ♦ every task {♦Γ} ∪ Ψ□ with Γ ̸∈ C is satisfiable in some typed model vΓ, hence by Lemma 4.3 G ⊕ 〈vΓ : Γ ̸∈ C〉 is a typed model satisfying Ψ, which by Lemma 4.2 implies that Ψ is satisfiable.

Theorem 4.1. S4∗ is complete for interpretations on finite S4-models.

Proof. If a formula ϕ is consistent, then by Lemma 4.1, {ϕ} has a consistent saturation Φ; then, Φ♦□ is consistent, so by Lemma 4.9 it is satisfiable in some finite typed model w. By Lemma 4.3, {Φ} ⊕ {w} is a typed model for ϕ, which by Lemma 4.2 implies that ϕ is satisfiable.

From this result we immediately obtain the following:

Corollary 4.1. S4∗ has the finite model property and is decidable.

Proof. This result in fact follows from the decidability and finite model property of the μ-calculus [Kozen, 1988; Streett and Emerson, 1984], but can also be verified using Theorem 4.1.

It shows that non-valid formulas have finite countermodels, so S4∗ enjoys the finite model property. Since it is also axiomatizable, it follows that it is decidable.

5 Conclusions and future work

The work presented in [Dawar and Otto, 2009; Fern´andezDuque, 2011] has already suggested that S4∗ may be better as a basic logic for spatial reasoning than S4, given that it is more expressive and forms a more natural fragment of familiar logics without a substantial cost to syntax. However, to make this a serious proposal there are several issues which need to be taken care of.

One issue is that of a 'nice' axiomatization, which is given by the current paper. It also gives us a finite model property, which is useful since S4∗ should be regarded as a logic of topological spaces, which are usually infinite and can be rather messy.

However, axiomatizability is not enough; in future work it would be important to analyze the complexity of reasoning in S4∗ . The methods we present here could be adapted towards these goals: for example, one can track the model construction to measure the size of finite models, which a rough estimate shows not to be much larger than models satisfying S4 formulas. Indeed, we conjecture S4∗ validity to be PSPACE complete, just like S4, and believe a proof may be extracted from the techniques presented here.

Once the basic S4∗ is well-understood, our goal is to consider more complex logics containing it. In fact, the basic modal language is quite weak for reasoning about spatial structures. Because of this, many successful applications of S4 as a spatial logic use additional modal operators and greater structure.

A specific example we have in mind is Dynamic Topological Logic (DTL), introduced in [Artemov et al., 1997] and expanded in [Kremer and Mints, 2005]. These logics involve temporal and topological modalities, and can be used to model processes where some of the variables are continuous and may contain margins of error. It is our belief that enriching DTL with the tangled closure operator will provide benefits not only in terms of expressivity, but also in terms of axiomatizability: indeed, no complete axiomatization for DTL with 'henceforth' is known, and we have strong reasons to believe that such an axiomatization would be easier to establish with the polyadic modality.