CS代考计算机代写 flex AI chain Reasoning About Space: The Modal Way
Reasoning About Space: The Modal Way
MARCO AIELLO, Department of Information and Communication Technologies, University of Trento, Via Sommarive 14, 38050 Trento, Italy. E-mail aiellom@ieee.org
JOHAN VAN BENTHEM, Institute for Logic, Language and Computation, University of Amsterdam, Plantage Muidergracht 24, 1018 TV Amsterdam, The Netherlands.
E-mail: johan@science.uva.nl
GURAM BEZHANISHVILI, Department of Mathematical Sciences, New Mexico State University, Las Cruces, NM 88003-0001, USA.
E-mail: gbezhani@nmsu.edu
Abstract
We investigate the topological interpretation of modal logic in modern terms, using a new notion of bisimulation. We look at modal logics with interesting topological content, presenting, among others, a new proof of McKinsey and Tarski’s theorem on completeness of S4 with respect to the real line, and a completeness proof for the logic of finite unions of convex sets of reals. We conclude with a broader picture of extended modal languages of space, for which the main logical questions are still wide open.
Keywords: Spatial reasoning, modal logic, topological interpretation, topo-bisimulation, serial set.
1 Introduction and purpose
The topological interpretation is one of the oldest semantics for modal languages. Reading the modal box as the interior operator, one can show that the modal logic S4 is complete with respect to arbitrary topological spaces. But there are classical results with much more mathe- matical content, such as McKinsey and Tarski’s beautiful theorem that S4 is also the complete logic of the reals, and indeed of any metric separable space without isolated points [20]. In the 1970s, Albert Dragalin started a programme of investigating modal logics of geometrical structures in Euclidean spaces, as reported in [26] containing Shehtman’s results on logics of domains of the real plane (similar results were obtained independently by Goldblatt [17]). At the same time, Esakia started the study of modal diamonds interpreted as the topological derivative operator, resulting in an axiomatization of the base logic (later published in [15]), as well as that of scattered spaces [14]; in the late 1980s, Shehtman gave a similar axioma- tization of Euclidean spaces [27] solving a problem posed in [20]. Also, much of the work on modal ‘neighbourhood semantics’ has a topological flavour, though the spatial aspect was never prominent. Overall, it seems fair to say that the topological interpretation has always remained something of a side-show in modal logic and intuitionistic logic, often tucked away in notes and appendices.
The 1990s marked extensive research in spatial logics from the AI point of view. An extension of Allen’s approach to qualitative reasoning for time intervals [3] to spatial regions
J. Logic Computat., Vol. 13 No. 6, c Oxford University Press 2003; all rights reserved
Page 889
Journal of Logic and Computation
890 Reasoning About Space: The Modal Way
[23] has been the seed for a number of modal studies of space in AI. The spatial version of the interval calculus, named the region connection calculus RCC, is a first-order theory with a topological predicate of connection. Since RCC is undecidable, Bennett [6] proposed a study of tractable fragments through an encoding into a multi-dimensional modal logic interpreted in topological spaces. Subsequently, Renz and Nebel have shown this encoding to be NP- complete [25]. Combinations of the modal encoding of RCC with various temporal theories have been proposed, from a computational viewpoint, in [32, 33]. Lemon and Pratt [19] provide an appealing analysis of spatial models and the design of complete logics for them.
The purpose of this paper is to establish a programme of the modal analysis of space – showing how one can get more generality, as well as some new questions. In particular, this paper contains (a) a modern analysis of the modal language as a topological formalism in terms of ‘topo-bisimulation’ (continuing [1]), (b) a new proof of McKinsey and Tarski’s Theorem (inspired by [21]), (c) an analysis of special topological logics on the reals, pointing towards a landscape of spatial logics above S4, and finally (d) an extension to richer modal languages of space, and their increased expressive power.
2 Modal language and topological semantics
2.1 Language and axioms
Let us first set the scene where we will operate. The basic language of propositional modal logic is composed of
a countable set of propositional variables,
Boolean connectives ,
modal operators .
The standard axiomatization of our central logic S4 is
(K)
(4) (T)
Modus Ponens and Necessitation are the only rules of inference:
For a closer fit to topological reasoning, however, it is better to work with an equivalent axiomatization of S4:
(N) (R) (T) (4)
Modus Ponens and Monotonicity are the only rules of inference:
Page 890
Journal of Logic and Computation
Reasoning About Space: The Modal Way 891
As we shall see in a moment, these principles are valid in all topological spaces when we let formulas range over sets of points, with the Booleans as the obvious set operations, modal box as interior and dually, modal diamond as closure. On top of this base set, further modal axioms can be used to express more special topological properties. For example, an additional ‘axiom’ would say that each set is open, meaning that the spaces satisfying it have the discrete topology.
2.2 Topological completeness
The first semantic completeness proof for S4 did not use the by now dominant Kripke models, which go back to Kanger, Hintikka, and Kripke in the 1950s. It was actually an earlier spatial completeness argument of [20], in terms of the following notions. Recall that a topological space is a pair , where is a nonempty set and is a collection of subsets of satisfying the following three conditions:
;
if ,then ;
if ,then .
Let and denote the interior and closure operators of , respectively. It is well known (cf. [13]) that these satisfy the following clauses for all :
.
, and a topological space can also be defined in terms of an interior operator or a closure operator satisfying the above four clauses.
Moreover, there is a duality McKinsey and Tarski defined a valuation
,
,
,
,
,
,
.
of formulas of into by putting
In definitions and arguments in this paper, we will often economize, and leave out the clauses for disjunction, implication and modal diamond, as these are automatic from the others. Now, call a triple a topological model. A formula is said to be true in such a model if , and we say that is topologically valid if it is true in every topological model. Referring to the second axiomatization of S4, which highlights the interior operator, one easily sees its soundness:
If then is topologically valid
Page 891
Journal of Logic and Computation
892 Reasoning About Space: The Modal Way
McKinsey and Tarski’s pioneering achievement [20] was a proof of completeness (for a new proof, see Section 3 below):
If is topologically valid, then
Hence, for a modal logician, the topological semantics is adequate for S4, or the other side of the same coin, for a topologist, S4 axiomatizes the algebra of the interior operator completely.
2.3 The semantics amplified
In the rest of the paper we use a modern format for modal semantics. Given a topological model , we define when a formula is true at a point by induction on the length of :
iff ;
iffnot ;
iff and ;
iff and ;
and hence, also
iff .
This semantics for the modal language looks different from the usual one, where models have a binary accessibility relation between points, and if is true in all relational successors of . Nevertheless, there are strong analogies. All basic notions of Kripke models make sense for the topological semantics, too. Here are two typical examples that we shall need further on.
The topological semantics is local in that the truth value of a formula at a point only depends on what happens inside the open neighbourhoods of that point. More precisely, consider any topological model with a point inside, which lies in some open set . Now define the obvious restriction of to a topological model by taking for the new universe,lettingtheopensetsbealltheoldopensetsinside ,andputting . It is easy to show by induction on formulas that
iff .
Thus, to determine truth values for modal formulas at a point on the real line we only need to know how the model behaves in arbitrarily small open neighbourhoods around . Or conversely, we can change the model at a distance from a point , without affecting the original truth values.
Our second illustration concerns the proper semantic invariance for our modal language. The connection between and is a special case of a more general model relation investigated at length in [1], including versions in terms of Ehrenfeu ̈cht–Fraisse ́ games.
DEFINITION 2.1 (Topo-bisimulation)
Suppose that two topological models and are given. A topo-bisimulation isanonemptyrelation suchthatif then
Page 892
Journal of Logic and Computation
(base):
(forth condition):
(back condition):
Reasoning About Space: The Modal Way 893 iff forany ;
if then
;
if then
As an example, the identity relation on is a topo-bisimulation between the above mod- els and . This also shows that the preceding definition does not require totality: some points need not have links at all. But much rougher ‘contractions’ and ‘twists’ are also possible. For example, a continuous and open map between topological spaces gives rise to a topo-bisimulation. We recall that a map between two topological spaces and is called continuous if for every ; is called open if forevery .
FACT 2.2
Let be a continuous and open map between two topological spaces and .
1.Suppose isavaluationon . Defineavaluation on bysetting for any . Then is a topo-bisimulation between the topologi- calmodels and .
2.Suppose isavaluationon suchthat iff forany and with .Defineavaluation on bysetting for any . Then is a topo-bisimulation between the topological models and .
As follows from the above, topo-bisimulation is a coarse notion of similarity between topological spaces, much less fine-grained than homeomorphism or homotopy. But it is just right for the expressive power of the modal language.
FACT 2.3
If is a topo-bisimulation between two models , such that , then , satisfy the same modal formulas.
The statement of true versions of converse results is a much more delicate matter (cf. [8] and [11]). Here we give just one simple illustration.
FACT 2.4
If two worlds and satisfy the same modal formulas in two finite models and , then there exists a topo-bisimulation between these models which connects with .
2.4 Topological spaces and Kripke models
We briefly describe the well-known connection between topological and Kripke semantics for modal logic. The latter is a particular case of the former. To see this, we recall that an S4-frame (henceforth ‘frame’, for short) is a pair , where is a nonempty set and is a quasi-order (transitive and reflexive) on . Call a set upward closed if and imply .
FACT 2.5
Every frame gives rise to a topological space , where is the set of all upward closed subsets of .
Page 893
Journal of Logic and Computation
894 Reasoning About Space: The Modal Way
It is easy to check that
for any family
spaces, in which every point has a least neighbourhood. In frames, the least neighbourhood of a point is evidently , which is usually denoted by .
Conversely, every topological space naturally induces a quasi-order defined by putting iff . This is called the specialization order in the topological literature. Again it is easy to check that is transitive and reflexive, and that every open set of is – upward closed. Moreover, is anti-symmetric iff satisfies the separation axiom (that is, any two different points are separated by an open set). Hence, is a partial order iff is a -space.
Now it is easy to check that and . Moreover, the following four con- ditions are equivalent: (i) , (ii) every -upward closed set belongs to , (iii) every point of has a least neighbourhood in , (iv) is an Alexandroff space.
The upshot of all this is a one-to-one correspondence between quasi-ordered sets and Alexandroff spaces, and between partially ordered sets and Alexandroff -spaces. Since every finite topological space is an Alexandroff space, this immediately gives a one-to-one correspondence between finite quasi-ordered sets and finite topological spaces, and finite partially ordered sets and finite -spaces. It is straightforward to see that this also implies a one-to-one correspondence between order-preserving maps and continuous maps, as well as between -morphisms and continuous and open maps.
3 General completeness
The preceding section shows that standard modal models are a particular case of a more general topological semantics. Hence, the known completeness of S4 plus the topological soundness of its axioms immediately give us general topological completeness. Even so, we now give a direct model-theoretic proof of this result. It is closely related to the stan- dard modal Henkin construction, and is much like completeness proofs for neighbourhood semantics (see [12]), but with some nice topological twists.
3.1 The main argument
Soundness is immediate, and so we move directly to completeness. Call a set of formulas of (S4–)consistent if for no finite set we have that . A consistent set of formulas is called maximally consistent if there is no consistent set of formulas properly containing . It is well-known that is maximally consistent iff, for any formula of , either or , but not both. Now we define a topological space out of maximally consistent sets of formulas.
DEFINITION 3.1 (Canonical topological space)
The canonical topological space is the pair , where:
is the set of all maximally consistent sets ;
is a topology on
. Indeed,
is a rather special topology on
;
, we have . Such spaces are called Alexandroff
is the set generated by arbitrary unions of the following basic sets
is . In other words, basic sets are
Let us first check that is indeed a topological space.
def
.
any formula
the families of the form:
, where
Page 894
Journal of Logic and Computation
LEMMA 3.2
forms a basis for the topology.
PROOF. We only need to show the following two properties:
Forany andany ,thereis ;
suchthat
Forany ,thereis
suchthat .
Now(N)impliesthat
. Hence,
the first item is satisfied.
, and so
forany
. Hence,
item is satisfied. As for the first item, thanks to (R), one can easily check that
Reasoning About Space: The Modal Way 895
,andsothesecond
is closed under finite intersections, whence,
Next we define the canonical topological model. DEFINITION 3.3 (Canonical topological model)
The canonical topological model is the pair , where: is the canonical topological space;
.
The valuation equates truth of a propositional variable at a maximally consistent set with its membership in that set. We now show this harmony between the two viewpoints lifts to all formulas.
LEMMA 3.4 (Truth lemma) For all modal formulas ,
iff
PROOF. Induction on the complexity of . The base case follows from the definition above. The case of the Booleans follows from the following well-known identities for maximally consistent sets:
.
The interesting case is that of the modal operator . We do the two relevant implications separately, starting with the easy one.
;
‘From membership to truth.’ Suppose . By definition, is a basic set, hence
. Therefore, there exists an open neighbour-
open. Moreover, thanks to axiom (T),
for all
hood
.Thus .
, for any
, and by the induction hypothesis,
of
such that
‘From truth to membership.’ Suppose
such that
and
. Therefore,
for all
. This implies that the logic S4 can prove the
. By the induction hypothesis,
implication . (If not, there would be some maximally consistent set containing both
and .) But then we can prove the implication , and hence, using the S4
transitivity axiom, . It follows that , and so the world
belongs to
. Then there exists a basic set
.
Page 895
Journal of Logic and Computation
896 Reasoning About Space: The Modal Way
Now we can clinch the proof of our main result. THEOREM 3.5 (Completeness)
For any set of formulas ,
then
PROOF. Suppose that . Then is consistent, and by the Lindenbaum Lemma it can be extended to a maximally consistent set . By the Truth Lemma, , whence , and we have constructed the required counter-model.
3.2 Topological comments
Let us now look at some topological aspects of this construction. In proving the box case of the Truth Lemma, we did not use the standard modal argument, which crucially invokes the distribution axiom of the minimal modal logic. Normally, one shows that, if a formula does not belong to a maximally consistent set , then there exists some maximally consistent successor set of containing . This is not necessary in the topological version at this stage. We only needed the reflexivity and transitivity axioms, plus the Lindenbaum Lemma on maximally consistent extensions. The modal distribution axiom still plays a crucial role, but that was at the earlier stage of verifying that we had really defined a topology. This different perspective provides an additional proof-theoretic explanation why S4 is the weakest axiom system complete for the topological semantics. Moreover, the divergence with the ‘standard’ argument explodes the prejudice that one single ‘well-known’ interpretation for a language must be the only natural one.
Comparing our construction given above with the standard modal Henkin model for S4, the basic sets of our topology are -upward closed. Hence, every open is -upward closed, and is weaker than the topology corresponding to . In particular, our canonical topological space is not an Alexandroff space.
if
Here are some further topological aspects of the above construction. First, it is worthwhile
, yieldingaspacewhichwedenoteby . Itiswellknownthat ishomeo- morphic to the Cantor space, and so, up to homeomorphism, is compact, metric,
to compare Stone’s famous construction which uses the alternative basis
any formula
-dimensional, and dense-in-itself. The basis of our topology, however, was the subfamily
any formula
. Now every subtopology of one that is compact and dense-in-itself is also compact and dense-in-itself. Therefore, we get these same properties for our canonical topological space. But we can be more precise than this.
FACT 3.6
The canonical topology is actually the intersection of Kripke and Stone topologies.
In other words,
. Indeed, since
and
, obviously
. Conversely, since every basic set
of Stone’s topology is
-upward .
closed iff
As an immediate consequence of the above observations we obtain:
for some
, we have
, and so
COROLLARY 3.7
S4 is the logic of the class of all topological spaces which are compact and dense-in-itself.
Still, the canonical topological space is neither -dimensional nor metric (it is not even a -space). So, is not homeomorphic to the Cantor space. In Section 4 we show how to get completeness of S4 with respect to the Cantor space by a different route.
Page 896
Journal of Logic and Computation
Reasoning About Space: The Modal Way 897
3.3 Finite spaces suffice
We conclude Section 3 with an observation that is important for later arguments. The whole construction in the completeness proof would also work if we restricted attention to the finite language consisting of the initial formula and all its subformulas. All definitions go through for this restricted setting, and our arguments never needed to go beyond it. This means that we only get finitely many maximally consistent sets, and so nonprovable formulas can be refuted on finite models, whose size is effectively computable from the formula itself. (Note however that the obtained finite model is not necessarily dense-in-itself.)
COROLLARY 3.8
S4 has the effective finite model property with respect to the class of topological spaces.
Incidentally, this also shows that validity in S4 is decidable, but we forego such complexity issues in this paper.
The resulting models have some interesting topological extras. Consider any finite frame . Wedefinesomeauxiliarynotions. Forany let . Callaset aclusterifitisoftheform forsome : thecluster generatedby . issimpleif ,andproperotherwise. Anelement of iscalledminimalif implies forany . Acluster isminimalifthereexists aminimal suchthat . Next,call rootedifthereis suchthat for any : is then a root of . This need not be unique: any point from , the initial cluster of , will do.
Evidently, a finite Kripke frame is rooted iff it has only one minimal cluster. Topo- logically, this property is related to the notion of connectedness. We recall that a topological space is connected if its universe cannot be written as a union of two disjoint open sets. is well-connected if implies or , for any . Obvi- ously well-connectedness is a stronger notion than connectedness. It corresponds to being rooted. For this observe that, dually, well-connectedness can be stated as follows:
For any two closed subsets and of , implies or . LEMMA 3.9
A finite Kripke frame is rooted iff the corresponding topological space is well-connected.
PROOF. Suppose is a rooted Kripke frame with a root , and is the corre- sponding topological space. Let and be closed sets of such that . It is easy to see that a set is topologically closed iff it is downward closed in the ordering, that is and imply , for any . Now if both and are nonempty, then belongs to both of them, which is a contradiction. Hence, one of them should be empty, and so is well-connected.
Conversely, suppose is not rooted. Then there are at least two different minimal clusters and in . Since and are minimal clusters, they are downward closed, and hence closed in . Moreover, since they are different, . Thus, is not well-connected.
This allows us to improve on Corollary 3.8. THEOREM 3.10
S4 is the logic of finite well-connected topological spaces.
Page 897
Journal of Logic and Computation
898 Reasoning About Space: The Modal Way
PROOF. It suffices to observe the following. If a modal formula has a counter-example on a finite Kripke model, it fails at some point there. But then by standard modal locality it also fails in the submodel generated by that point and its relational successors, which is rooted and hence transforms into a well-connected topological space.
Again, there is a downside to such an upgraded completeness result. What it also means is that the basic modal language cannot define such a nice topological property as well- connectedness.
4 Completeness in real spaces
As early as 1944, McKinsey and Tarski [20] proved the following beautiful result, which is an expansion of a completeness theorem by Tarski [29] for intuitionistic propositional logic from 1938.
THEOREM 4.1 (McKinsey–Tarski)
S4 is the logic of any metric separable dense-in-itself space.
Most importantly, this theorem implies completeness of S4 with respect to the real line , as well as with respect to the Cantor space . The original algebraic proof in [20] was very complex, the later more topological version in [24] is not much more accessible. Re- cently, Mints [21] replaced these by a much more perspicuous model-theoretic construction, extending earlier ideas of Beth and Kripke to get faster completeness of S4 with respect to the Cantor space. We generalize its model-theoretic structure, using the topo-bisimulations of Section 2, and also provide a modification for completeness on the reals.
4.1 Cantorization
Our starting point is an arbitrary modal formula which is not provable in S4. We have already seen that such a nontheorem can be refuted on a finite rooted Kripke model. Now we show how to transform the latter into a topological counterexample on the Cantor space .
We think of the Cantor space as the countable topological product , where is a two-element set with the discrete topology. Then the basic opens for the topology on C are , where all but finitely many coincide with . To picture the Cantor space, we think of the full infinite binary tree ; starting at the root, one associates to every left-son of a node and to every right-son (see Figure 1).
We call a countable sequence of nodes of an infinite path of if is therootof andeach isanodeonthethlevelof . Ifthesequenceisfinite,thenwecall it a finite path of . We think of points of the Cantor space as infinite paths of . Therefore, if denotes the set of all infinite paths of , then is in a one-to-one correspondence with C.TotransferthetopologicalstructureofCto,forafinitepath of let
aninitialsegmentof
It is routine to observe that the sets correspond to basic opens of C. Thus, if we define
topology on by introducing
a finite path of
as a basis, the following obvious fact holds true.
Page 898
Journal of Logic and Computation
Reasoning About Space: The Modal Way 899
01010101
0101
. Now we define a map
from branches to worlds by putting
01
FIGURE 1.
FACT 4.2
is homeomorphic to .
NowforanyfiniterootedKripkemodel ,welabel bytheworldsof recursively as follows.
DEFINITION 4.3
For any node the -comb is the infinite leftward branch starting at plus all one-step rightward successors of its nodes in (see Figure 2).
For let denotesomeenumerationof .
(1) We label the root of by a root of .
(2) We always repeat the same world as a label upwards to the left (see Figure 3).
(3) If is labelled by , then we label the right nodes of the -comb as follows:
and repeated modulo (see Figure 4).
Suppose .If isgoinginfinitelytotheleft,thatis isoftheform , then by our labelling there exists such that labels every node of starting from some node on. In this case we say that stabilizes . Otherwise, as node labels increase along the ordering of the model , there exists a ’highest’ cluster of such that every node of is labelled by an element of starting from some node on. In this case we say that
keeps cycling in
stabilizes
arbitrarily chosen representative of
if
if keeps cycling in , where is some
Page 899
Journal of Logic and Computation
900 Reasoning About Space: The Modal Way
LEMMA 4.4
For any finite path end of .
t
FIGURE 2. -comb
w w
w w
w w
FIGURE 3. World repetition on the left
of we have , where is the label occurring at the
PROOF. Since every branch carries label , the definition of implies that . Conversely, if , then by the above cyclic rule of labelling suc- cessors along a comb, there is a finite path extending whose end is labelled by . The infinite path is then mapped to .
LEMMA 4.5
isacontinuousandopenmapfrom onto .
PROOF. (a) is onto. This follows immediately from the labelling of the -comb, where is the root of .
(b) preserves opens. By Lemma 4.4 basic opens of are mapped onto the basic opens of the Alexandroff topology on . It follows that preserves arbitrary opens.
Page 900
Journal of Logic and Computation
Reasoning About Space: The Modal Way 901
w w
w
w 1
w n(w)
w w
w
w 3
w 2
w 1
(c) let
FIGURE 4. First -comb labelling
reflects opens. It suffices to look at basic opens of the form . Now, for
a finite path of whose end is labelled by
Obviously
Lemma 4.4 that Conversely,suppose that carrieslabel .
. Hence,itissufficienttoshowthat . First,itfollowsfrom
,i.e. . Let beafinitepathof such
.
PROOF. Suppose S4 . Then by Theorem 3.10 there is a finite rooted Kripke model refuting . By Fact 4.2 and Corollary 4.6 there exists a valuation on the Cantor space such that is topo-bisimilar to . Hence, is refuted on .
4.2 Counterexamples on the reals
In the previous section we described how to transform counterexamples on a finite rooted Kripke model into counterexamples on the Cantor space . In this section we show how to transfer counterexamples from to the open interval of real numbers. As a result, we obtain a new proof of completeness of S4 with respect to the real line . Our strategy is similar to that of Section 4.1. First we establish a one-to-one correspondence between
. Therefore,
andtheendof islabelledby . Then ,andso
Now we define a valuation on by putting . COROLLARY 4.6
is a total topo-bisimulation between and . PROOF. Apply Lemma 4.5 and Fact 2.2.
THEOREM 4.7
S4 is complete with respect to the Cantor space.
Page 901
Journal of Logic and Computation
902 Reasoning About Space: The Modal Way
and a suitable set of infinite paths of the full infinite binary tree . Then we transfer the topology from to . Finally, we label nodes of by worlds of in a way which allows us to define a valuation on such that is topo-bisimilar to . This labelling is a bit more complicated than the previous one, but it shows the freedom one has on the tree within the ‘back and forth’ constraints of a modal simulation. It will readily follow that S4 is complete with respect to , and hence with respect to .
We note that there exist three different types of infinite paths of : (1) is going infinitely totheleftif ;(2) isgoinginfinitelytotherightif ; finally, (3) is infinitely zigzagging if it is neither going infinitely to the left nor infinitely to the right. Let denote the set of infinite paths of that are either going infinitely to the left or are infinitely zigzagging. We also let . Then there is a one-to-one correspondence between and . To see this recall the dyadic representation
ofanumberfrom . Let . Toconstructaninfinitepath of
representing observe that either
inthelattercaseput . Assume . Theneither or . Inthe former case put and in the latter case put . Continuing this process, we will get an infinite path of representing .
or . In the former case put and
Note that there are two ways for the dyadic representation of a number , where
and ;eitheras oras .Therefore, if we throw away together with all infinite paths of going infinitely to the right, we obtain a one-to-one correspondence between and the remaining infinite paths of . Hence, there exists a bijection, say , between and . In order to transfer the topological structure of to , we need the following lemma.
LEMMA 4.8 Thefamily
.
PROOF. Suppose
formsabasisforthetopologyon
. For an arbitrarily small , select so that .
Let bethelargestintegerforwhich . Then . From
itfollowsthat . Since ,wehavethat
. Also
and implythat .Therefore,thereexist
suchthat .Thus, ,
and so there exists a member of containing and contained in . This implies
that forms a basis for the topology on .
For andso
twocasesarepossible: (1)If iseven,then forsome ,
;and(2)if isodd,then forsome ,andso
. Therefore, we can think of as the union of two kinds of sets and
. It follows from the proof of Lemma 4.8 that if
does not have the form , then there
exist such that . So the only reason we need elements
of is to find small neighbourhoods around the points of the form .
Now we take the set of -images of elements of as a basis for the topology on . Then it should be clear that is homeomorphic to . To understand better what the -imageofanelementof is,forafinitepath of ,let
aninitialsegmentof
Page 902
Journal of Logic and Computation
and
Reasoning About Space: The Modal Way 903
We observe that if represents , then represents , and
so represents . Therefore, elements of are represented as s, where is
a finite path of . To represent elements of we need the following definition.
DEFINITION 4.9 (1) We call
back-to-back nodes if is the end of the finite path and
is the end of the finite path
times
. In a picture, they sit on top of the following
sn= s
s1
times
W-formation in (see Figure 5).
t = tn
t2
s2
t1
FIGURE 5. W-formation
(2) We call back-to-back nodes at least -deep if .
Let .If represents ,where endsin,then
. Thus, elements of are represented as , where and ending in back-to-back nodes . So if we define topology on
afinitepathof
represents , where ends in and are back-to-back nodes. Therefore,
represents are finite paths of by taking the sets
and
and finite paths of ending in back-to-back nodes as a basis, the following obvious fact holds:
FACT 4.10
is homeomorphic to .
NowforanyfiniterootedKripkemodel worlds of recursively as follows. For of .
,welabelthenodesof by let denote some enumeration
Page 903
Journal of Logic and Computation
904 Reasoning About Space: The Modal Way
(1) We label the root of by a root of .
(2) We always repeat the same world as a label upwards on the left.
(3) If is labelled by , then we label the right nodes of the -comb as follows:
andrepeatedmodulo (seeFigure6).
w w
w w
w w
w w
w w
w w
w i
w
w i−1
w 1
w
w n(w)
ww
w i+1
w
w i
FIGURE 6. Second -comb labelling
Clause (3) involves repetition of the initial label in between successors of . The point of this trick will become clear below. Also note that we left the exact starting point for the successor labelling along the teeth of the -comb unspecified. To make the choice of , we look at the node preceding , if any. Given our inductive procedure, we only need to consider the case where is a right-successor of , as labels were merely repeated going leftward. Suppose that is labelled by . Then two cases are possible:
Case 1: is a strong successor of in . Then we just put .
Case2: Thetwoworldlabelsarethesame: . Then,if istherootof ,again put . Otherwise, by our labelling procedure, the situation is as in Figure 7. That is, the node is a left-successor of some node labelled with , and the latter’s right-successor is labelled by some successor . In this case, put .
Now we prove a crucial property of this construction. LEMMA 4.11
If labels and labels , where are at least -deep back-to-back nodes of , then .
Page 904
Journal of Logic and Computation
w =u i
w
Reasoning About Space: The Modal Way 905
label
and
label asinFigure5. Then , ,and and
v= w
u
FIGURE 7. Case 2
PROOF.Let
are on the teeth of the same comb. So by our labelling procedure only the preceding two cases are possible.
Case1: .Then because and sincewealwaystook -successors going up any branch.
Case2: isastrongsuccessorof . Thenbytherepetitionruleforlabels, , and ’s first rightward successor, which in the worst case is since the back-to-back nodes are at least -deep, is labelled by the above rule. So again .
The rest of the proof is similar to the proof for the Cantor space, but with some additional
w
verifications. First, we define
by putting:
if stabilizes
Thus, is the restriction of the earlier
if keeps cycling in to .
LEMMA 4.12
For any finite path of we have , where is the label of the end of .
PROOF. The argument is like before. Since , it is obvious that . Alsosinceeverypath carrieslabel ,wehave . Toseethethird inclusion let . By our labelling we find recurring repetitions of label on the teeth of the -comb. Let be on the teeth of the -comb labelled by , and let be a finite path of with the end . Then is an initial segment of , whence . By the definitionof wehave .So .
LEMMA 4.13
isacontinuousandopenmapfrom onto .
PROOF. (a) is onto. This follows immediately from the labelling of the -comb, where is the root of .
(b) preserves opens. It suffices to consider basic opens in the new topology, which are of the form and , where the ends of and are back-to-back nodes. By Lemma
Page 905
Journal of Logic and Computation
906 Reasoning About Space: The Modal Way
4.12 the sets and are mapped to unions of open sets of the form , which are open in the Alexandroff topology on .
(c) reflects opens. Again it suffices to look at basic opens in . Let be any world in
. We let
finite paths of whose ends are at least -deep
a finite path of whose end is labelled by
and
back-to-back nodes with respective labels such that
It is sufficient to show that . First, consider the inclusion from righttoleft. Lemmas4.11and4.12implythat . In particular,forthecaseof wenotethat because . Therefore, . Fortheinclusionfromleft to right, suppose that , i.e. . Now either is infinitely zigzagging or is going infinitely to the left.
Case 1: is infinitely zigzagging. Then it is in some open set with carrying label andtheendof labelledbysome . Therefore, .
Case 2: is of the form . Then lies in an open set , where the ends of and are back-to-back nodes. As the open neighbourhoods can be chosen arbitrarily small, we can assume that the back-to-back end nodes of are at least -deep. Let labeltheendof and labeltheendof . ByLemma4.11wehave . Also, since carries label , . Therefore, .
In either case we have , thus the equality.
Finally, similar to the Cantor space argument, we define a valuation on by copying the valuation of the model using the inverse of . By a reasoning exactly like before, we get:
COROLLARY 4.14
is a total topo-bisimulation between and .
This gives our main result. THEOREM 4.15
1. S4 is complete with respect to .
2. S4 is complete with respect to the real line .
PROOF. (1) Suppose S4 . Then by Theorem 3.10 there is a finite rooted Kripke model refuting . By Corollary 4.14, is topo-bisimilar to . Hence, is refuting . Now since is homeomorphic to , is refuted on .
(2) Suppose S4 . Then by (1) there exists a valuation on refuting . Now since is homeomorphic to , is refuted on .
This provides an alternative proof of McKinsey and Tarski’s original theorem. The method seems quite flexible, as we can vary tree labelling very widely, while keeping a topo-
Page 906
Journal of Logic and Computation
Reasoning About Space: The Modal Way 907
bisimulation with the initial Kripke model. Another attraction is the immediate geometri- cal character of the procedure. Inductive tree labelling with recurring world labels is a bit like imposing fractal structure on a representation of the space.
Finally, we note that a minor further step establishes the following version of the complete- ness result.
COROLLARY 4.16
There exists a single valuation on falsifying all the nontheorems of S4.
PROOF. Enumerate all the nontheorems of S4. This can be done since the language of S4 is countable. Let this enumeration be . Since the interval is home- omorphic to , from Theorem 4.15 it follows that there exists a valuation on
such that
of .) Forany let
each is an open submodel of , where the ‘identity embedding’ is a topo-bisimulation. Hence, the truth values of modal formulas do not change moving from each to . Therefore, isstillfalsifiedonthewhole foreach. Thus, we have constructed a single valuation on falsifying all the nontheorems of S4.
This corollary also shows that, though very different from the standard canonical Kripke model of S4, shares some of its universal properties.
4.3 Logical nonfiniteness on the reals
Recall that two formulas and are said to be S4-equivalent if . It is well known that there exist infinitely many formulas in one variable which are not S4-equivalent. Consider the following list of formulas:
We can easily construct a Kripke model in which all have different interpretations. Let ,where denotesthesetofallnaturalnumbers, iff ,and iff iseven. Thenonecanreadilycheckthat istrueatallevenpoints . Hence, every has a different interpretation on . It implies that the are not S4- equivalent. Now we will give a topological flavour to this result by showing that interpreting a propositional variable as a certain subset of allows us to construct infinitely many S4- nonequivalent formulas of one variable. Corollary 4.16 already told us such a uniform choice must exist, but the proof does not construct explicitly. The following argument does, and thereby also highlights the topological content of our modal completeness theorem in a more concrete fashion.
We use and instead of the standard notations and for the interior and closure operators of a topological space. This modal notation shows its basic use in topology because it allows us to write topological formulas in a much more perspicuous fashion.
To proceed further we need to recall the definition of Hausdorff’s residue of a given set. Suppose a topological space and are given. is called theHausdorffresidueof .Let and .
is said to be of rank , written , if is the least natural number such that ; is said to be of finite rank if there exists a natural such that is of rank ; is said to be of infinite rank if it is not of finite rank.
falsifies
. (Note that we need not know anything about the shape
bethevaluationof on. Notethat
Page 907
Journal of Logic and Computation
908 Reasoning About Space: The Modal Way
is said to be of rank if , but ; is said to be of finite rank if there exists a natural such that is of rank ; is said to be of infinite rank if it is not of finite rank.
Obviously is of rank iff the rank of every element of is strictly less than , and there is at least one element of of rank ; is of finite rank iff there is a natural such that the rank of every element of is strictly less than ; and is of infinite rank iff there is no finite bound on the ranks of elements of .
It is obvious that if we interpret as a subset of , then will be interpreted as . So, in order to show that different are S4-nonequivalent, it is sufficient to show that there is suchthat .
PROPOSITION 4.17
Thereexistsasubset of suchthat .
PROOF. We will construct inductively. Fix a natural number .
Step 1: Consider a sequence from converging to , and put
where
. Note that
,
is a sequence from
,
,
. So,thepointsof ofrank are
rank , and .
, and
,forarbitrary and , istheonlypointof of
where is a sequence from converging to . Note that
,and
,
converging to
,
,and .
So, is the only point of
Step 2: Consider a sequence
of rank , and .
from converging to
, and put
Page 908
Journal of Logic and Computation
Reasoning About Space: The Modal Way 909 Step n: Consider a sequence from converg-
ing to , and put
where is a sequence from
. Also let
converging to
Thennotethat
,
,
,and
,
,
.
So, the points of of rank are
the points of of rank are
,
and so on; finally, is the only point of of rank , and .
Nowlet beconstructedin , in , in ,andsoon. Weput
Then it is obvious that and , for any natural . So,
,and containspointsofeveryfiniterank.
REMARK 4.18
It is worth noting that the constructed above does not contain elements of infinite rank. However, a little adjustment of the above construction will allow us to construct a subset of with an element of infinite rank. Actually, it is possible to construct a subset of containing elements of rank , for any ordinal .
Returning to our list of formulas, with as the just constructed , the interpretation of every in will be different. In the next section we show that if we restrict ourselves to only ‘good’ subsets of , then the situation will be drastically changed.
Page 909
Journal of Logic and Computation
910 Reasoning About Space: The Modal Way
5 Axiomatizing special kinds of regions
As we saw in the previous section, by interpreting propositional variables as certain subsets of the real line , we can refute every nontheorem of S4 on . Certainly not all subsets of are required for refuting the nontheorems of S4. In this section, we will analyse the complexity of the subsets of required for refuting the nontheorems of S4. Similarly to Section 4.5, we prefer to use and to denote the interior and closure operators of a topological space. For consistency we also use and to denote the set-theoretical intersection, union, and complement.
5.1 Serial sets on the real line
To start with, consider subsets of with the simplest intuitive structure. Call convex if all points lying in between any two points of belong to . In other words, is convex if and imply .Everyconvexsubsetof hasoneofthefollowing forms:
DEFINITION 5.1 Call a subset of serial subsets of
serial if it is a finite union of convex subsets of . Denote the set of all by . So,
isaserialsubsetof
Obviously the constructed in Proposition 4.17 is not serial, and actually this was abso-
lutely crucial in showing that had points of any finite rank. Indeed, we have the following: LEMMA 5.2
forany .
PROOF. First, foranyconvexsubset of. For,if isconvex,then
consists of at most two points,
, and
.Hence, .
,
Now let
of , and actually we can assume that all are disjoint. But then and so .
be a serial subset of
. Then
, where every
is a convex subset
It follows that if we interpret as a serial subset of , then all from the previous section define sets equal to each other.
Callavaluation ofourlanguage tosubsetsof serialif forany . Since isclosedwithrespectto and,wehavethat foranyserial valuation . Call a formula -true if it is true in under a serial valuation. Call -valid if is -trueforanyserialvaluationon. Let is -valid.
FACT 5.3
is a normal modal logic over S4.
Obviously all from the previous section are -equivalent. So, it is natural to expect that there are only finitely many formulas in one variable which are -nonequivalent, and indeed that is a much stronger logic than S4.
Page 910
Journal of Logic and Computation
Reasoning About Space: The Modal Way 911 As a first step in this direction, we show that the Grzegorczyk axiom
belongs to . LEMMA 5.4
Grz is -valid.
PROOF.Grzis -validiff forany . Suppose .Since isfinite, .Hence ,whichclearlycontains . So, .
As a next step, we show that the axioms , and
, bounding the depth and the width of a Kripke frame to , are -valid.
LEMMA 5.5
and are -valid.
PROOF. Notethat is -validiff forany , andthat
is-validiff
Toshowthat forany ,suppose .Then isa limit point of not belonging to . Since is serial, there is such that either and ,or and . Inbothcasesitisobviousthat . So,
.
Toshowthat forany ,
suppose .Then and .Hence, thereexist suchthat and ,whichmeansthat .So, .
The following is an immediate consequence of our observations. COROLLARY 5.6
.
In order to prove the converse, and hence complete our axiomatization of the logic of serial subsets of , observe that is actually the complete modal logic of the following ‘-fork’ Kripke frame , where and (seeFigure8).
forany .
FIGURE 8. The -fork frame
Page 911
Journal of Logic and Computation
912 Reasoning About Space: The Modal Way
Indeed, it is well known that Grz is valid on a Kripke frame iff it is a Noetherian partial order, that is valid on a partially ordered Kripke frame iff its depth is bounded by , and that is valid on a partially ordered Kripke frame of a depth iff its width is bounded by . Now, denoting the logic of by , we have the following:
THEOREM 5.7
.
PROOF. Denote by . Obviously, . Hence, . Conversely, since Grz is a theorem of , every -frame is a Noethe- rian partial order. Since is a theorem of , every -frame is of depth . Therefore, has the f.m.p., and thus is complete with respect to finite rooted partially ordered Kripke frames of depth . Since is a theorem of , it is obvious that the width of finite rooted -frames is also . But then it is routine to check that every such rooted frame is a -morphic image of . Hence, , and so .
As a final move, we show that is a continuous and open serial image of , meaning thatthereisacontinuousandopenmap suchthat foranysubset of.
Recall that consists of the upward closed subsets of , which obviously are , ,
,
, and
. Fix any
anddefine byputting
for
for
for
Then it is routine to check that
, ,and . So, iscontinuous. Moreover, for any open subset of , if , then ; and if , then , which is always open. Hence, is open. Furthermore, from the definition of it follows that the -inverse image of any subset of is a serial subset of . So, is a continuous and open serial image of .
As a trivial consequence of this observation, we obtain that for every valuation on there is a serial valuation on such that is topo-bisimilar to . Hence, every nontheorem of is a nontheorem of , and we have the following:
COROLLARY 5.8
.
Combining Corollaries 5.6 and 5.8 and Theorem 5.7, we obtain: THEOREM 5.9
.
5.2 Formulas in one variable over serial sets
This section provides some more concrete information about definability of serial sets. As is the logic of the finite ‘2-fork’ frame, for every natural number , there are only finitely many -nonequivalent formulas built from the variables . In this section, we show that there are exactly -nonequivalent formulas in one variable, and describe them all.
, ,
Page 912
Journal of Logic and Computation
Reasoning About Space: The Modal Way 913
THEOREM 5.10
Every formula in one variable is -equivalent to a disjunction of the following six formu-
las: ,
,
,
,
, and .
Hence, there are exactly -nonequivalent formulas in one variable.
PROOF. In line with our interest in tying up ‘modal’ and ‘topological’ ways of thinking, we will give two different proofs of this result. One proceeds by constructing the -universal Kripke model of , which is a standard technique in modal logic; the other is purely topological, using some obvious observations on serial subsets of .
First Proof. Since is the logic of the ‘-fork’ frame, we can easily construct the - universal Kripke model of , where iff is even (see Figure 9). Now one can readily check that each point of corresponds to one of the six formulas in the condition of the theorem. Hence, every formula in one variable is -equivalent to a disjunction of the above six formulas. Since there are exactly different subsets of , we obtain that there are exactly -nonequivalent formulas in one variable.
FIGURE9. Second Proof. Observe that there exists a serial subset of
such that
.Forexample,
let ,andtake . Thenonecanreadilycheckthat
,
, ,
,
,and
.
Hence, we can always interpret as a serial subset of such that all the six formulas of the theorem correspond to different serial subsets of .
Page 913
Journal of Logic and Computation
914 Reasoning About Space: The Modal Way
Now, let us prove that every subset of obtained by repeatedly applying to a serial set is equal to a finite (including the empty) union of the following serial subsets:
,
,
,
,
,and .
Forthisfirstobservethat if ,andthat . So,thesesix
serial subsets of are mutually disjoint and jointly exhaustive. Next observe that ,where aredifferentfromeachother. Finally observe that , , and .
Hence, every subset of obtained by repeatedly applying to is a finite (including the empty) union of .
Now suppose is obtained by repeatedly applying to . We prove by induction on the complexity of that is equal to a finite (including the empty) union of .
Basecase. Since (and ) is obvious.
),thebasecase(thatiswhen
.
Then
using the distributivity law we obtain that . Since for different
and , ,whichistheemptyunionof s,wefinallyobtainthat isafinite unionof .
Intersection.Suppose , and ,where . Similarlytotheabovecase,usingthedistributivitylaw we obtain that is a finite union of .
Interior.Suppose and ,where .Since saremutuallydisjoint, . Nowsince isclosedwith respect to , we obtain that is a finite union of .
Hence, every subset of obtained by repeatedly applying to a serial set is equal to a finite (including the empty) union of . Since there are exactly different subsets obtained as a union of , we obtain that there are exactly different subsets of obtained by repeatedly applying to a serial set . This directly implies that there are exactly -nonequivalent formulas in one variable.
The same technique can also be used to prove the normal form theorem over for every formula with more than one propositional variable.
5.3 Countable unions of convex sets on the real line
Let us now be a bit more systematic. By Theorem 4.15, S4 is the complete logic of , and hence sets of reals suffice as values in refuting nontheorems. But how complex must these sets be? In first-order logic, for example, we know that completeness requires
Complement. Suppose and
, where
. Since every
is equal to
,
Page 914
Journal of Logic and Computation
Reasoning About Space: The Modal Way 915
atomic predicates over the integers which are at least . With only simpler predicates in the arithmetic hierarchy, the logic gets richer. In a topological space like , it seems reasonable to look at the Borel Hierarchy . How high up do we have to go for our S4-counterexamples? One could analyse our construction in Section 4.3 to have an upper bound. But here we will state some more direct information.
Consider the set of all open subsets of . Let denote the Boolean closure of . Since contains all open subsets of , it is obvious that is closed with respect to . Obviously is properly contained in . It is natural to ask whether the elements of are enough for refuting all the nontheorems of S4. The answer is negative, the modal logic is still richer.
FACT 5.11
[10] The complete logic of is Grz.
Hence, we need to seek something bigger than . Let denote the set of count- able unions of convex subsets of . Since every open subset of is a countable union of open intervals, it is obvious that . Let denote the Boolean closure of .Since ,wealsohave .Itfollowsthat is also closed with respect to . Moreover, is properly contained in , since the set Q of rationals belongs to but does not belong to .
THEOREM 5.12
[10] S4 is the complete logic of .
So, the Boolean combinations of countable unions of convex subsets of are all we need for refuting the nontheorems of S4. Since every countable union of convex subsets of belongs to the Borel hierarchy over the opens of , a very low level of the Borel hierarchy suffices for refuting nontheorems of S4. So, itself is more than sufficient for refuting nontheorems of S4.
Summarizing, we constructed five Boolean algebras of subsets of forming a chain under inclusion: ,where istheBooleanalgebra of all serial subsets of , is the Boolean closure of the set of all open subsets of , is the Boolean closure of the set of all countable unions of convex subsets of , is the Boolean algebra of all Borel subsets of over , and is the power set of . All of these Boolean algebras are closed with respect to . The modal logic of the last three algebras is S4, that of the second one is Grz, and the modal logic of the first is the logic of the ‘-fork’ Kripke frame.
5.4 Generalization to R
We conclude this section by sketching the generalization of our results on the serial subsets of to sufficiently well-behaved ‘chequered subsets’ of a Euclidean space .
A set is convex if all points lying in between any two points of
It is said to be serial if is a finite union of convex subsets of . Denote the set of all serial subsets of by . The main difference between and is that, unlike , is not closed with respect to the set-theoretical complement. For instance, a full circle is obviously a convex subset of . However, its complement is not serial.
One natural way of overcoming this difficulty is to work with a smaller family of chequered subsets of , which also has a reasonable claim of being ‘the -dimensional generalization of one-dimensional serial sets’.
belong to .
Page 915
Journal of Logic and Computation
916 Reasoning About Space: The Modal Way
Aset issaidtobeahyper-rectangularconvexif ,whereall the are convex subsets of [7]. It is easy to see that every hyper-rectangular convex is a convex set in the usual sense, but not vice versa. For example, in the real plane a circle is obviously convex, but it is not a rectangular convex.
A set is said to be -chequered if it is a finite union of hyper-rectangular convex subsets of . Denote the set of all -chequered subsets of by . Obviously .
Notethatunlike , doesformaBooleanalgebra.Moreover, for any . Hence, interpreting propositional variables as -chequered subsets of , every formula of our language will also be interpreted as a -chequered subset of .
This approach leads to a logic, which we sketch here. We call a valuation of to subsets of -chequeredif forany . Since isclosedwithrespect to and,wehavethat forany-chequeredinterpretation . Wecalla formula -true if it is true in under a -chequered valuation. We call -valid if is - trueforany-chequeredvaluationon . Let is-valid. Denoteby the -times Cartesian product of the ‘2-fork’ frame on itself. Let denote the logic of . A complete characterization of is given by the following:
THEOREM 5.13 .
PROOF. See [9].
In particular, the logic of chequered subsets of the real plane coincides with the logic . An illustration of is given in Figure 10. For interesting alternative approaches for the plane consult [22, 4].
FIGURE 10.
Page 916
Journal of Logic and Computation
Reasoning About Space: The Modal Way 917
6 A general picture
6.1 The deductive landscape
The logics that we have studied in this paper fit into a more general environment. Typical for modal logic is its lattice of deductive systems such as K, S4, S5 or GL. These form a large family describing different classes of Kripke frames, with often very different motivations (cf., for instance, [18, 34]). Among the uncountably many modal logics, a small number is distinguished for one of two reasons. Logics like S4 or S5 were originally proposed as syntactic proof theories for notions of modality, and then turned out to be semantically com- plete with respect to natural frame classes, such as quasi-orders for S4. Other modal logics, however, were discovered as the complete theories of important frames, such as the natural numbers with their standard ordering. What about a similar landscape of modal logics for the topological interpretation?
Some well-known modal logics extending S4 indeed correspond to natural classes of topo- logical spaces. For example, it is easy to see that the ‘identity logic’ with the axiom axiomatizes the complete logic of all discrete spaces. And it also defines them semantically through the usual notion of frame correspondence, which can be lifted to the topological se- mantics in a straightforward manner. But already S5 corresponds to a less standard condition, namely that every point has an open neighbourhood all of whose points have in all their open neighbourhoods. (Alternatively, this says that every open set is closed.) Also, even rich topological spaces do not seem to validate very spectacular modal logics, witness the fact that has just S4 for its modal theory. We did find stronger logics with ‘general frames’ though, i.e. frames with a designated interior algebra of subsets, such as with the serial sets.
A related question is what becomes of the known general results on completeness and correspondence for modal logic in the topological setting. There appear to be some obstacles here. For example, the substitution method for Sahlqvist correspondence (cf. [11]) has only a limited range. It does work for axioms like the above , where it automatically generates the corresponding first-order condition
i.e. discreteness. Likewise, it works for the S5 axiom , where it produces the above-mentioned
The method also works for antecedents of the form , but things stop with antecedents like or . The reason is that, in the topological semantics, one modality expresses a two-quantifier combination
such that
so that syntactic complexity builds up more rapidly than in standard modal logic, where each modality is one quantifier over relational successors of the current world. General correspon- dence or completeness results for topological modal logics therefore seem harder to obtain, and we may need different syntactic notions for them (see [16] for recent results in this di- rection).
Page 917
Journal of Logic and Computation
918 Reasoning About Space: The Modal Way
6.2 The expressive landscape
In any case, the basic modal language seems too poor to express many properties of topo- logical interest. A good example is connectedness, which cannot be modally defined. To see this, suppose there was a modal formula defining connected topological spaces in the sense of frame correspondence. Now consider the nonconnected discrete -element space with the universe . The formula must fail here under some valuation , say at point . Now consider the one-point model copying ’s valuation. The link between just the worlds in the two models is a topo-bisimulation, as it is easy to see. But then, by modal invariance, would also fail in the connected one-point model: a contradiction.
Connectedness does have a definition in a modal language extended with a universal modality expressing that holds in all worlds of the model, and a dual existential modal- ity expressing that holds in at least one world. This allows us to express connectedness in the following way [28, 1]:
This is one instance of a general trend in modal logic toward moderate expressive exten- sions of the base language. The language is a natural candidate, as it can formulate ‘global facts’ about topological spaces such as inclusion of one region into another. Many of our earlier techniques apply such as frame correspondence, bisimulation and related model constructions. (Cf. [1] for back-up to this section.) The general logic of this new language is known [6]. It is the system S4S5, being S4 for , S5 for , plus the ’bridge axiom’ . Moreover, according to [28], we have a natural extension of the McKinsey and Tarski theorem: the modal theory of , and indeed of any metric separable dense- in-itself space, is exactly S4S5 plus the given connectedness axiom. Thus, the concerns of this paper reproduce for richer modal languages, expressing more topological behaviour.
Indeed, modal languages can also have much stronger topological modalities, such as the following ‘Until’ operator generalizing two well-known notions from temporal logic:
has an open neighbourhood all of whose interior points satisfy while all its boundary points satisfy .
And even further extensions are needed to deal with modal separation axioms, such as a space being Hausdorff, which requires even stronger ‘modalities’ definable in the monadic second- order language over topological spaces. One can then see the art of the field in choosing ‘good fragments’ out of this total language, admitting a good balance between expressive power and complexity.
Finally, the same modal methodology also extends to other similarity types. In particular, one can introduce geometrical structure. For example, the affine geometry of betweenness suggests a ‘convexity modality’ :
lies in between two points that satisfy .
This brings out differences between the spaces , as but no higher-dimensional sat- isfies the principle . (A more extensive study of various modal languages for affine, projective, and metric geometries is made in [5, 31, 2].)
Thus, there is a lot of modal logic of space in between Tarski’s work on the propositional language of topology [29, 20] and his work on the full first-order language of elementary geometry [30]. We see our work and much of the related literature we have cited as the beginnings of a systematic way of filling this gap.
Page 918
Journal of Logic and Computation
Reasoning About Space: The Modal Way 919
Acknowledgements
We thank Yde Venema, Maarten Marx, and Nick Bezhanishvili of University of Amsterdam, Mai Gehrke and Patrick J. Morandi of New Mexico State University, and Mamuka Jibladze and Dimitri Pataraia of the Georgian Academy of Sciences for discussions. We also thank Ting Zhang of Stanford University for pointing out a flaw in the original proof of Lemma 4.13, as well as the referees for their comments which changed the original version of the paper.
References
[1] M. Aiello and J. van Benthem. Logical patterns in space. In Words, Proofs, and Diagrams, D. Barker-Plummer, D. Beaver, J. van Benthem, and P. Scotto di Luzio, eds, pp. 5–25. CSLI, Stanford, 2002.
[2] M. Aiello and J. van Benthem. A modal walk through space. Journal of Applied Non-classical Logics, 12, 319-363, 2002.
[3] J. Allen. Maintaining knowledge about temporal intervals. Communications of the ACM, 26, 832–843, 1983.
[4] P. Balbiani, J. Condotta, and L. Farin ̃as del Cerro. A model for reasoning about bidimensional temporal rela- tions. In Proceedings of the International Conference on Principles of Knowledge Representation and Reason-
ing (KR’98), A. G. Cohn, L. Schubert, and S. Shapiro, eds, pp. 124–130. Morgan Kaufmann, 1998.
[5] Ph. Balbiani, L. Farin ̃as del Cerro, T. Tinchev, and D. Vakarelov. Modal logics for incidence geometries.
Journal of Logic and Computation, 7, 59–78, 1997.
[6] B. Bennett. Modal logics for qualitative spatial reasoning. Bulletin of the IGPL, 3, 1–22, 1995.
[7] J. van Benthem. The Logic of Time, volume 156 of Synthese Library. Reidel, Dordrecht, 1983. [Revised and
expanded, Kluwer, 1991].
[8] J. van Benthem. Exploring Logical Dynamics, volume 156. CSLI Publications, Stanford — Cambridge Uni-
versity Press, 1996.
[9] J. van Benthem, G. Bezhanishvili, and M. Gehrke. Euclidean hierarchy in modal logic. Studia Logica, 2003.
To appear. Also available as Technical Report PP-2002-07, University of Amsterdam.
[10] G. Bezhanishvili and M. Gehrke. A new proof of completeness of S4 with respect to the real line. Technical
Report PP-2002-06, University of Amsterdam, 2002.
[11] P. Blackburn, M. de Rijke, and Y. Venema. Modal Logic. Cambridge University Press, 2001.
[12] B.F. Chellas. Modal Logic: An Introduction. Cambridge University Press, 1980.
[13] R. Engelking. General Topology. Heldermann Verlag, 1989.
[14] L. L. Esakia. Diagonal constructions, Lo ̈b’s formula and Cantor’s scattered spaces. In Studies in Logic and
Semantics, pp. 128–143. Metsniereba, 1981. In Russian.
[15] L. L. Esakia. Weak transitivity-restitution. In Study in Logic, Volume 8, pp. 244–254. Nauka, 2001. In Russian.
[16] D. Gabelaia. Modal Definability in Topology. Master’s thesis, ILLC, University of Amsterdam, 2001.
[17] R. Goldblatt. Diodorean modality in Minkowski space-time. Studia Logica, 39, 219–236, 1980.
[18] M. Kracht, M. de Rijke, H. Wansing, and M. Zakharyaschev, eds. Advances in Modal Logic, volume 1. CSLI
Publications, 1998.
[19] O. Lemon and I. Pratt. On the incompleteness of modal logics of space: advancing complete modal logics of
place. In Advances in Modal Logics ’96, M. Kracht, M. de Rijke, H. Wansing. and M. Zakharyaschev, eds.
CSLI and FoLLi, Stanford, 1996.
[20] J. McKinsey and A. Tarski. The algebra of topology. Annals of Mathematics, 45, 141–191, 1944.
[21] G. Mints. A completeness proof for propositional S4 in Cantor Space. In Logic at work: Essays dedicated to
the memory of Helena Rasiowa, E. Orlowska, ed. Physica-Verlag, Heidelberg, 1998.
[22] I. Pratt and D. Schoop. Expressivity in polygonal, plane mereotpology. Journal of Symbolic Logic, 65, 822–
838, 2000.
[23] D. Randell, Z. Cui, and A. G. Cohn. A spatial logic based on regions and connection. In Proceedings of
International Conference on Principles of Knowledge Representation and Reasoning (KR’92), pp. 165–176.
San Mateo, 1992.
[24] H. Rasiowa and R. Sikorski. The Mathematics of Metamatematics. Panstwowe Wydawnictwo Naukowe, 1963.
Page 919
Journal of Logic and Computation
920 Reasoning About Space: The Modal Way
[25] J. Renz and B. Nebel. On the complexity of qualitative spatial reasoning: a maximal tractable fragment of the region connection calculus. Artificial Intelligence, 108, 69–123, 1999.
[26] V. Shehtman. Modal logics of domains on the real plane. Studia Logica, 42, 63–80, 1983.
[27] V. Shehtman. Derived sets in Euclidean spaces and modal logic. Technical Report X-1990-05, University of
Amsterdam, 1990.
[28] V. Shehtman. ‘Everywhere’ and ‘Here’. Journal of Applied Non-classical Logics, 9, 369–379, 1999.
[29] A. Tarski. Der Aussagenkalku ̈l und die Topologie. Fund. Math., 31, 103–134, 1938.
[30] A. Tarski. What is elementary geometry? In The Axiomatic Method, with Special Reference to Geometry ad
Physics, L. Henkin and P. Suppes and A. Tarski, eds, pp. 16–29. North-Holland, 1959.
[31] Y. Venema. Points, lines and diamonds: a two-sorted modal logic for projective planes. Journal of Logic and
Computation, 9, 601–621, 1999.
[32] F. Wolter and M. Zakharayaschev. Spatio-temporal representation and reasoning based on RCC-8. In Proceed-
ings of the International Conference on Principles of Knowledge Representation and Reasoning (KR2000),
A. G. Cohn, F. Giunchiglia, and B. Selman, eds, pp. 3–14, 2000.
[33] F. Wolter and M. Zakharyaschev. Qualitative spatio-temporal representation and reasoning: a computational
perspective. In Exploring Artifitial Intelligence in the New Millenium. Morgan Kaufmann, 2002.
[34] M. Zakharyaschev, K. Segerberg, M. de Rijke, and H. Wansing, eds. Advances in Modal Logic, volume 2.
CSLI Publications, 2000.
Received 25 October 2001
Page 920
Journal of Logic and Computation
