Incomplete Spatial Logics

Abstract
Formalizing geographic knowledge is a lively research issue in the interdisciplinary field of Artificial Intelligence and Computational Geography. Such formalizations (Randell et al, 1992, Bennett, 1994, Pratt, 1993, Lang and Asher, 1995, Hernández, 1994, Nebel, 1994, Bennett, 1995, Jeansoulin and Mathieu, 1995) ultimately rely on "logics" of space. But what guarantee do we have that a formalization really captures the spatial notions which it sets out to? Without such a guarantee there is a danger that formalisms for spatial reasoning in computational geography might fail to capture their intended targets: that the systems might be incomplete.

We explore several "spatial" logics and investigate their credentials as logics of space. A semantical adequacy criterion for spatial logics is developed, according to which a logic is spatially adequate only if consistent theories in that logic are realizable in the standard Cartesian model of space. Various (supposedly) spatial logics are shown not to satisfy this criterion. In effect, these observations amount to incompleteness results for classes of spatial logics, because they show that consistent sets of formulae in these logics have no models of the intended sort.

Motivation
The general problem with "spatial" logics is that it is sometimes hard to know whether one has written down enough axioms to characterize the spatial notions in question - while a collection of suggested axioms may well have models; it is sometimes hard to see why we should regard these models as models of space at all.

Positional modal logics: a first inadequacy result
Von Wright (1979), employs the spatial interpretation of modal operators in order to analyse the logic of the spatial term "near". Von Wright conjectures that the "near" relation. corresponds to the modal system SwB (weak Brouwer)^l. It is quite easily seen that this logic is inadequate. Consider the following collection of formulae:

(1)

The logic SwB is characterized by serial, irreflexive, symmetric, and intransitive Kripke frames. Thus, the diagram of figure 1 is a permissible structure making the formula (1) true. Hence this formula is consistent.

Figure 1: Some convex regions and their representations over one revolution

But now consider the proposed spatial gloss on à. Under this gloss, formula (1) says that there are n locations all near to points which are near to 'here' but which, because of the conflicting propositions that are true at all points near to them, cannot be near to each other. Let us suppose that "near" means "no more than distance d away". Then, for n ³ 6 there are no possible configurations of points in the plane which can serve as an interpretation of formula (1). The reason is that, to make the sentence true in the plane, one would have to fit 6 (or more) non-overlapping closed circles of radius d around (overlapping the edge of) a closed circle of radius d - and this situation is easily shown to be geometrically impossible. In the case of embedding in R³, a larger number of spheres (in fact n ³ 12) would have to be used².

Thus, we have proved:

Theorem 1: Let the modal operator SwBo in the logic SwB have the intended geometrical interpretation "at some point no more than distance d away". Then there are consistent sentences of the logic which have no models with the intended geometrical interpretation, in either 2 or 3 dimensions.

So, just because we have an axiomatization which seems intuitively correct for some "spatial" notion, that does not mean that such a logic actually captures that notion. In order to do that, consistent sets of sentences in that logic must be realizable in R² or R³ using the intended interpretations of the spatial notions the logic is supposed to axiomatize. In putting forward the logic SwB, von Wright has not provided us with a logic of "near" at all; he has just written down three or four of its properties.

An adequacy criterion for spatial logics
Definition 1: A logic is spatial only if consistent theories in that logic are realizable in the standard Cartesian model of space.

A set of sentences of a logic is realizable in the standard Cartesian model of space if there is a configuration of objects in that space which makes all the sentences true under the intended interpretations of the spatial predicates of that logic.

RCC theory: two further inadequacy results
In fact, RCC theory (Randell et al, 1992, Bennett, 1994, Bennett, 1995, Nebel, 1994) can be shown to be inadequate in precisely the same sense that von Wright's logic of "near" is inadequate. That is, there are consistent sentences of the theory that have no model under the intended interpretation of the spatial primitives - the axioms merely list some properties of the spatial concepts they purport to characterise.

One obvious place where things are bound to go wrong involves non-planar graphs. To make things simple suppose that the regions involved are to be understood as open sets of two- dimensional Euclidean space. Let R_i,j, (i,j = 1 to 3) be nine connected regions of the plane. We impose the following constraints on the way that R_i. may overlap each other:

1. For i = 1 to 3, the three regions R_i,1, R_i,2, and R_i,3, all contain a common (non-empty) region, T_1,i.
2. For j = 1 to 3, the three regions R_1,j, R_2,j and R_3,j all contain a common (non-empty) region, T_2,j.
3. R_i,j and R_i',j', do not overlap if i ¹ i' and j ¹ j' .

These constraints can easily be expressed by a formula in the language of RCC given the gloss on C(x, y). We establish: (i) these constraints cannot be satisfied in R²; (ii) the formula enforcing these constraints is consistent in RCC. Thus, we have a consistent formula with no model in two-dimensional Euclidean space.

Theorem 2: Let the predicate C(x,y) in the logic RCC have the intended geometrical interpretation "the closure of x has points in common with the closure of y ", where x and y are open sets of R². Then there are consistent sentences of the logic which have no models with the intended geometrical interpretation.

But what of the advertised interpretation in terms of regions of R³? It does not take too much ingenuity to show that a similar result holds there:

Theorem 3: Let the predicate C(x,y) in the logic RCC have the intended geometrical interpretation "the closure of x has points in common with the closure of y ", where x and y are open sets of R³. Then there are consistent sentences of the logic which have no models with the intended geometrical interpretation.

Proof: omitted

RCC with convexity: another inadequacy result
We have deduced (independently of the previous results) a simple result that constrains any search for a logic of convexity.

Theorem 4: Any axiomatization of conv(x) in the language of RCC which is adequatefor n-dimensional Euclidean space must be incorrect for n + 1 -dimensional Euclidean space.

Conclusion
We raise the important issue of the semantical adequacy of spatial logics for computational geography, and provide a semantical adequacy criterion for such logics. We show that the RCC theories of "space" can express consistent theories which do not have spatial models.

The above results highlight the importance of a deeper understanding of the formal semantics of spatial logics for a genuine computational formalization of geographic knowledge.

References
Bennett, B. 1994. Spatial Reasoning with Propositional Logics. In 4th International Conference on Knowledge Representation and Reasoning. Morgan Kaufmann.

Bennett, B. 1995. Modal Logics for Qualitative Spatial Reasoning. Bulletin of the IGPL, 3.

Hernández, D. 1994. Qualitative Representation of Spatial Knowledge, volume 804 of Lecture Notes in Artificial Intelligence. Springer-Verlag, Berlin.

Jeansoulin, R. and Mathieu, C. 1995. Revisable Spatial Knowledge by means of a Spatial Modal Logic. In Joint European Conference on GIS, The Hague, Netherlands.

Lang, J. and Asher, N. 1995. A Nonmonotonic Approach to Spatial Persistence Based on Distances and Boundaries. In Time, Space, and Movement, Toulouse, Groupe LRC Toulouse.

Nebel, B. 1994 Computational Properties of Qualitative Spatial Reasoning: First Results. In 19th German Conference on Artificial Intelligence, Bielefeld, Germany.

Pratt, I. 1993 Map Semantics. In Andrew Frank and Irene Campari, editors, Spatial Information Theory: a theoretical basis for GIS, volume 716 of Lecture Notes in Computer Science, pages 77 - 9 1. Springer Veriag, Berlin.

Randell, D., Cui, Z., and Cohn, A. 1992. A Spatial Logic based on Regions and Connection. In 3rd Intemational Conference on Knowledge Representation and Reasoning. Morgan Kaufmann.

von Wright, G. 1979. A Modal Logic of Place. In E. Sosa, ed. The Philosophy of Nicholas Rescher: Discussion and Replies, pages 65-73. D. Reldel, Dordrecht, Holland.

² Note: if à were interpreted as "at some location strictly less than distance d from here", the same problem would arise.