Toward a Geometry of Common Sense: A Semantics and a Complete Axiomatization of Mereotopology

1 Introduction

Mereological and topological notions of connection, part, in­ terior and complement are central to spatial reasoning and to the Natural Language (NL) semantics of expressions concerning locations and relative positions. For example, reasoning about objects inside other objects or on them may involve complex inferences based on a semantics for the prepositions in and 011 that exploits these mereotopological notions properly [4]. Reasoning about these concepts is also present in many commonsense reasoning tasks about spatial position and navigation [13, 16] . We propose here a semantics and complete axiomatization of these notions that takes the linguistic semantics of spatial expressions to be a fundamental guide to commonsense spatial and geometrical reasoning. We do this for two reasons. First we are interested in reasoning about spatial situations from linguistically given information, in particular the spatial prepositions, movement verbs, and noun phrases referring to portions of space. In such a task we must understand exactly what sort of information spatial expressions in NL convey. Second, we are interested in how the narrative structure of discourse can convey spatial information [2] .

When examining commonsense reasoning from this lin­ guistic perspective, two observations become apparent. The first is the absence in NL of a natural way of referring to points without measure. Such points are fundamental to the mathematical conception of topological spaces, geometry, and analysis. But they are foreign to space as it is usually expressed in narrative texts, newspaper articles and texts about how to get to a certain place, which are the sort of texts with which we have been concerned. At the very least, mathematical points are not needed to express spatial rela­ tionships within NL. Furthermore, the NL expressions that

Laure Vieu

IRIT, Universite Paul Sabatier 118 route de Narbonne 31062 Toulouse cedex, France vieu @irit.fr

we do use to refer to "points," "borders," and "surfaces" do not refer in the following examples to the mathematical notions:

1. The point of this pencil is actually an irregular surface with several peaks.
2. There is a scratch in the surface of the table.

Mathematical points, unlike pencil points, can't be sur­ faces, nor can mathematical surfaces have scratches (which presuppose a depth). Even the points, surfaces and bound­ aries of our commonsense world are three dimensionally extended objects.

The other observation is that agents use spatial information contained in texts even though this information does not contain any system of universal coordinates by means of which we may spatially situate the objects talked about in the text in the way we might use a coordinate system (e.g. longitude, latitude and altitude) to situate the position of a robot. NL strongly suggests that space is a relational concept as Leibniz argued, not an "absolute" concept as Newton thought. Our conception of space is constructed from or de­ pendent upon the relative positions of objects to each other. I

This is not to say that our commonsense conception of space has nothing to do with mathematical conceptions of space. Commonsense reasoning approximates but simplifies the mathematical concepts, since the full power of mathe­ matical topology, geometry or analysis, is not needed in commonsense spatial reasoning tasks. That there should be this compatibility between mathematics and commonsense seems evident to us in that, for example, we can express mathematically precise locations in NL relative to a system of coordinates-- north, south, east, west, longitude and lati­ tude, together with numerical expressions within these di­ mensions and the dimension of altitude. We can also when needed introduce the language of analysis. Indeed, one of the accomplishments of the theory we propose below is that we make this notion of approximation between commonsense and mathematics itself formally precise. But it is clear that mathematical expressions are not always present in NL when spatially useful information is present. Thus, the use of mathematically precise notions of space is not an essential part of our conception of space.

Our aim here is to develop the foundations of a common­ sense geometry. In section 2, we present a language in which we cannot refer to points without extension and in which there are no expressions for referring to a coordinate system. We also present in section 2 a semantics for this language. In sections 3 and 4, we present a new sound and complete theory for the topological aspects of this qualitative, rela­ tional conception of space. In section 5, we develop a modal analysis of the approximation between this commonsense conception of space and the mathematical one.

I Like time which may be construted out of events only, not taking states into account [12], space may be constructed from material objects only. Indeed, immaterial portions of space such as the space beneath the table are entities dependent of objects.

2 Structures for Relational Mereotopology

Our attempt to build topology and geometry out of a domain of individuals or "bodies" instead of points is inspired by Whitehead [21], Tarski [18] and Clarke [6,7], as well as work in mereology [14]. Tarski is the only one we know who has presented an axiomatized and complete mereotopo­ logical theory besides ours, but he classified his domain of "bodies" into "spheres" and non-spheres, thus recovering topological concepts from metrical ones. Our topological theory most directly exploits Clarke's work which corrects a mistake of Whitehead's, leading to an inconsistency. ~owever, since Clarke presents (in the Russellian philosoph­ teal style) only an axiomatic calculus, we will begin by describing the formal language and the semantic structures we have found necessary for the commonsense conception of space embodied in NL.

To state our relational, topological theory, we use a first order language, L RT with one non logical two place relation symbol, C, and a denumerable infinity of individual nonlogi­ cal constants (a, ao, a*, b, b., etc.) and variables (x, y, z, u, v, w, x 1, etc.). C represents intuitively the notion of connection between individuals. There are intuitively two sorts, EC (external connection), in which two objects share a boundary and 0 (overlap) in which two objects have a common part which is an object. A further kind of contact is also needed, WCont (weak contact), in which two objects are not con­ nected but are in some sense "vanishingly close" to each other. Examples of weak contact are the relation between a glass and the table on which it is standing and the relation between the glass and the wine it contains, while an example of external connection or "strong contact" is the relation between the stem of the glass and the cup of the glass. To express this notion of vanishing closeness, it is natural to suppose that each object has surrounding it a smallest neigh­ borhood. While WCont may be defined in terms of C it seems natural to us to think of its semantics using neighbor­ hood. Further, neighborhoods may be useful if we wish to impose constraints on smallest neighborhoods that we cannot state within LRT (for example, that for some fixed real number o, the neighborhood of x is within o of x). The presence of neighborhoods is also a useful feature if we wish to incor­ porate principles about how properties persist over spatial regions (see for instance [3]).

Besides these notions, NL semantics requires us to capture the more classical topological notions of openness and clo­ sure (for details see [4]). To show that the right topological notions of open and closed properties are grasped, it suffices to show that our cognitive spaces are structures built over topological spaces. The fact that our structures are based on set-theory and have points as primary entities is not in con­ tradiction with our aims. It doesn't really matter how one chooses to express the models of a theory: once completeness is proven, they are all equivalent in the sense that our language and inferential mechanisms cannot distinguish betwee~ them. Moreover, there are two clear advantages of expressmg our structures in terms of classical topological ~paces. First, _it's a practical way to compare the concepts we mtroduced With better-known ones, and second, it will give us the opportunity to show in section 5 that classical topol­ ogy may be seen as a limit ofmereotopology.

The domain of our structures is a subset of the power set of a topological space. Every subset corresponding to the space occupied by a physical object must clearly have a non­ empty interior. However, few people working on mereotopo­ logy have noticed an additional important feature of cogni­ tive space, emphasized in qualitative spatial reasoning by [10] and [8]: the subsets of a topological space correspond­ ing to physical objects are three dimensional throughout or "regular". Regularity has two defining features: for any n­ dimensional regular space, (1) every part of the objects in that space must be also n-dimensional (smooth boundaries); (2) these objects must have no "holes" of a lower dimension (full interiors). This means that subsets including a single isolated point, as well as subsets with a single interior point deleted are not in the structure. This feature has a further consequence: we must modify the union and intersection operators to ensure that they are internal composition laws on our domain of objects. To make this clear, consider this example. Suppose we have the one-dimensional space, <IR+, {any union of open intervals}>. Then, clearly any open in­ terval is "regular" but the union of (0, 1) and (1,2) has a deleted point, 1. The correct union operator of two regular subsets preserving "regurlamess" is, not ordinary u, but a new operator u*, introduced below. Similarly its dual n * replaces set intersection.

This discussion leads naturally to our definition of the models:

2.1 Definition of the models

Let T= <X, X> be a non-empty topological space (X being the set of points, X the set of open subsets of X, int and cl the interior and closure operators, open and closed the open and closed properties, and ..... the relative complement wrt X). Let RTT=<Y,f, KD> be a structure such that

1) Y is a set with the following properties

• (i) Y C p(X) and X e Y
• (ii) 'Vxe Y (int(x)e Y & int(x};a!:¢ & int(x)=int(cl(x))) (full interiors)
• (iii) "1/xe Y (cl(x)e Y & cl(x)=cl(int(x))) (smooth boundaries)
• (iv) "1/xe Y (int(-x) :t¢ ... -x e Y)
• (v) "1/xe Y "1/ye Y (int(xny) ~ ... xn*y e Y)
• (vi) "1/xe Y 'Vye Y x u*y e Y 2
• where xn*y = xnyncl(int(xny)) and xu*y =xuyuint(cl(xuy)
• (vii) 3xe Y 3ye Y (xny~ & int(xny}=¢)
• (viii) 3xe Y 3ye Y (xny=¢ & "1/ze Y ((open(z) & xCz) -+yncl(z~))
• f is a function over Y (f: Y ... Y) such that: x C f(x) & open(f(x)) & (cl(f(x))ny:t¢ ... xncl(f(y)~) & ((open(x) & yCx) ... f(y)Cx)

2Note that xn*y!: xny, xuy!: xu*y, xn*x=x, xu*x=x

f(x) is called the (smallest) neighborhood of x, a straightfor­ ward extension of the topological notion of neighborhood of a point. It is important to note that X cannot be dense (in the sense that (open(x) & open(y) & xC:y & x:;ty) -+ 3z (open(z) & z:;tx & z:;ty & xC:z & zC:y)), because the notion of a mini ­ mal open set is vacuous then, since the intersection of any set of open sets may not be an open set.

3) [Dis a function assigning individual terms a denotation in Y. The interpretation of C will be given below. (We assume the usual extension of the interpretation of constants [D to an interpretation of terms [lg, where g is an assignment of ob­ jects in the domain to the variables occurring free in the term.)

Of all these constraints only conditions (vii) and (viii) above have not yet been motivated. They are needed to ensure that our structure is nontrivial in the sense that it does have instances of weak contact and external connection.

2.2 Semantics for L

RTr ~gC(x,y) iff[xDgn [yDg:;t¢ RTr ~g WCont(x,y) iff not RTr~g C(x,y) and f([xD g) n [y D g :;t¢ R1' = { RT T: Tis a non-empty topological space}. Validity in every RTr model is written~ RT

2.3 Axiomatization

Our axiomatization extends and corrects that of [6]. Classical mereology [14], as well as [6], contains a fusion operator for summing up any collection of individuals into a new indi­ vidual. This general fusion operator is in fact unnecessary. In addition, removing Clarke's axiom stating the existence of the fusion of any collection of individuals is a simple way of making the theory first-order, and gives a response to a criti­ cism often given of mereology, that it is neither cognitively nor ontologically acceptable to assume the existence of indi­ viduals having as parts any collection of individuals. This change is visible in axioms (A4-S). The next change is in the definition of connectedness (DlO). Clarke's definition makes it impossible to have connected spaces as soon as it is split into two externally connected parts, since the sum of two in­ teriors equals the entire sface and thus is not connected according to his definition . Finally, we added WCont, and axioms that ensure that the theory is not trivially verified in any topology (because, e.g., there is no external connection).

TheoryRTo (Al) C(x,x) (A2) C(x,y)-+ C(y,x) (A3) (C(z,x) - C(z,y)) -+ x=y (Dl) P(x,y) -def T:/z (C(z,x)-+ C{z,y)) (D2) PP(x,y) -def P(x,y) & ...,P(y,x) (D3) O(x,y) -def 3z (P(z,x) & P(z,y)) (D4) EC(x,y) -def C(x,y) & --, O(x,y) (D5) TP(x,y) -def P(x,y) & 3z (EC(z,x) & EC(z,y)) (D6) NTP(x,y) -def P(x,y) & --.3z (EC(z,x) & EC(z,y)) (A4) 3x T:/u C(u,x) (A4) and (A3) entail the existence of a unique universe a*. (A5) T:/x T:/y 3z T:/u (C(u,z)- (C{u,x) v C{u,y))) (AS) and (A3) entail the existence of a unique sum of x and y, x+y for every x andy.

3we owe this observation to Carola Eschenbach.

• (A6) T:/x T:/y (O{x,y) -+ 3z T:/u (C(u,z) - 3v (P(v,x) & P{v,y) & C(v,u))))

(A6) and (A3) entail the existence of a unique nonempty intersection, x ·y for every x andy such that O(x,y).

(A7) T:/x (3y --,C(y,x) --+ 3z T:/u (C(u,z)- 3v (--,C{v,x) & C(v,u)))) (A7) and (A3) entail the existence of a unique complement of x in a*, -x, for every x:;ta*. (AS) T:/x 3y T:/u (C(u,y)- 3v (NTP(v,x) & C(v,u))) (AS) and (A3) entail the existence of a unique interior, ix, for every x. (D7) ex =def -i( -x) Since the complement is involved in this definition, c(x) exists only if x:;ta*. We make the c operator a function by adding axiom (A9): (A9) c(a*)=a* (DS) OP(x) .. defX=ix (D9) CL(x) .. def x=cx (AlO) (OP(x) & OP(y) & O(x,y))--+ OP(xey) (DlO) Con(x) -der--.3y 3z (x=y+z & --,C(cy,cz)) (Dll) WCont(x,y) -def --,C(x,y) & T:/z ((P(x,z) & OP(z)) --+ C(cz,y)) (All) 3x 3y EC(x,y) (A12) 3x 3y WCont(x,y) (A13) T:/x 3y (P(x,y) & OP(y) & T:/z (P(x,z) & OP(z)) -+ P{y,z))) (A13) and (A3) entail the existence of a unique neighbor­ hood nx for each x; if x is open, nx=x. Fact 3 shows that neighborhoods and WCont interact in the right way. Fact 1: i) --x=x; ii) icx=ix; iii) cix = ex. [20] Fact2: WCont(x,y)-+ WCont(y,x) [20] Fact 3: (--,C(x,y) & C(x,c(ny)))- WCont(x,y) Proof: -+ : By (A13), T:/z ((P(x,z) & OP(z)) -+ P(nx,z)). Since P(nx,z) -+ P(c(nx),cz), (C(c(nx),y) & P(nx,z)) -+ C(cz,y); so --,C(x,y) & T:/z ((P{x,z) & OP(z)) -+ C(cz,y)).

+-; Directly from (Dll) since by (A13), P(x,nx) & OP(nx)

3 The Soundness Proof

When added to the axioms and rules for first order logic, the set of axioms we have set up for relational mereotopology (RTo) form the basis of a proof relation ~RTo. A proof in RTo is as usual a finite sequence of sentences of L, each one of which is either an axiom or derivable from the other lines using Modus Ponens or Universal Generalization. We now provide a class of models for RT 0 to show that it is sound. Clarke did not do this, nor have any of the people following his work done this. This has led researchers, including Clarke, to miss certain important features of the theory--e.g., the models are not just the power sets of topological spaces with the subsets having an empty interior removed, and the difficulty of defining points within this theory (attempted in [7], but proved in [20] to be incorrect).

The question arises as to whether the constraints we have imposed on Y and hence on RTr, though intuitively moti­ vated, are consistent. It will suffice to show that, under the hypotheses that Y:;t~ and Y:;t{X} (needed to satisfy the con­ straints corresponding to {All) and (Al2)):

Fact 4: Let X andY be as defined above for RTrand suppose that Y:;t~ and Y:;t{X}; then, the elements asserted to exist in Yin clauses (i) and (iv)-(vi) verify the constraints on their interiors and closures imposed by clauses (ii) and (iii).

The proof though long is not hard. Our conclusion is that indeed the constraints are satisfiable by a substructure of a classical topological space.

Theorem 5: ~RTo<p-+ ~ RT<i>

The proof is by induction on the complexity of a proof in RT0 · We look here only at the basis case to show for an arbitrary model RTT=<Y,f, [D> that RTT~ (Al) to (Al3).

That a structure RTr verifies (Al) and (A2) is trivial. That RTT verifies (A4) follows immediately from the fact that Xe Y. To show (A3), it suffices to show that 'Vxe Y 'Vye Y ('Vze Y (z nx:;e~ .... z ny:;e~) .... xey). If y=X, xey is always true; if y:;eX, suppose 'Vze Y (znx:;e~ .... zny~) and -,xey, we have y:;eX .... --ye Y and -,xey .... xn--y:;e~ then by hypothesis, y n--y~. which is impossible. 4 D

More complex are (A5 - AS). Let's first consider (A5): to show RTT ~ 'Vx 'Vy 3z 'Vu (C(u, z) - (C(u,x) v C(u,y))) where z = x+y, we show that [x+yDg =ffxD gU*[yDg for some arbitrary assignment g. This amounts to showing: 'Vxe Y 'Vye Y 'Vue Y (un(xu*y)~- (unx~ v uny~))

+- : Since (unx:;e~ v uny:;e~) - un(xuy):;e~ and xuy e xu*y, un(xu*y~

-. :By definition, xu*y = (xuy)uint(cl(xuy)). So un (xu*y)~ .... un(xuy)~ v u nint(cl(xuy))~. Ifu n(xvy):;e ~;then the conclusion follows trivially. If unint(cl(xvy)~. then cl(u)=cl(int(u)) since ue Y, and so cl(int(u))n int(cl(xuy)):;e~. and cl(a)nint(b):;e~ .... anint(b):;e~. So int(u) nint(cl(xuy)):;e~. Then, int(u)nd(xuy):;e~. and so int(u)n (d (x)ucl(y)):;e~. or equivalently int(u)rcl(x):;e~ v int(u)n cl(y~. So unx~ v uny~.D

Now let's consider the proof for (A6): R TT ~ 'Vx 'Vy (O(x,y) .... 3z 'Vu (C(u,z)- 3v (P(v,x) & P(v,y) & C(v,u)))) where z = x·y. As with (A5), we will show that [x·yDg = [xDgn*[yDg. and this amounts to showing:

(*) 'Vxe Y 'Vye Y (3ze Y (zex & zey) .... 'Vue Y (un(xn*y)~- 3veY (vex & vey & vnu~))).

To show (*) we note the following fact of our models (which follows from the fact that xn*y e xny and that xn*y e Y, if int(xny):;e~): 'Vxe Y 'Vye Y (3ze Y (zex & zey) - int(xny):;e~). So to prove(*), assume zex & zey. By the fact above int(xny):;e~. So now we must show: un(xn*y):;e~- 3veY (vex & vey & vnu~).

-: Take v=xn*y

... : By hypothesis vexny. So cl(int(v)) e cl(int(xny)); cl(v)=cl(int(v)) since ve Y; so v e cl(int(xn y)); so, v e (xny) n cl(int(xny)). So v e xn*y. Since vnu:;e~ by hypothesis, un(xn*y~ .D

The proofs that RTT~ (A7) and RTT~ (AS) are similar to the proof of (A6). These proofs establish that the interpreta­ tion of the operators i and - are the operators int and ""'.

Proof for (A9): Since the interpretation of the operators i and- are the operators int and--, the definition in RTo of the operator c for all variables not equal to a* and the topolog!­ cal theorem: cl(x)=--int(--x) yield that [cxD g for g(x) :;eX IS cl(g(x)). The interpretation of c as cl can be extended to all ofY, so that RTT~ c(a*)=a*.D

Proof for (AlO): RTT ~ (OP(x) & OP(y) & O(x,y)) ..... OP(x·y). It suffices to show 'VxeY 'VyeY [(open(x) &

4since VxeY VyeY (xCy- VzeY (znx:;t:jll-+ zny:;t:lll)), we have RTT ~ P(x,y) iff [xD c [yD. an intuitive consequence.

open(y) & 3ze Y (zex & zey)) ..... open(xn*y)]. Assume (open(x) & open(y) & 3ze Y (zex & zey)); in view of the fact used to verify (A6) about the existence of xn*y, int(xny):;e~ . But since(open(x) & open(y)) ..... open(xny~ then int(xn y) = xny and since xn yecl(x ny), xn*y=xnyncl(xny)=xny.D

That RTT verifies (All) and (Al2) comes directly from conditions (vii) and (viii) on Y, and that RTT verifies (Al3) follows easily from the definition of the function f.D

4 Completeness

Since our axioms for our mereotopology are all 1st order, completeness ofRT0 amounts to showing completeness for a particular 1st order theory. This means that we need to show that if <p is not a theorem then we can construct a counter model of the appropriate sort. We do this by means of the usual Henkin method, in which three lemmas are crucial:

Lindenbaum Lemma: Every RT o consistent set of sentences can be extended to a maximal consistent set.

Saturation or Witness Lemma: Every RT o consistent set of sentences I. can be extended to a saturated set I.' in the ex­ tension ofL, L(ao, a~o ... ),such that I.'~ 3x A ..... A(a./x), for every formula with one free variable A and a. is a witness forx.

Henkin Lemma: Every RT o maximal consistent saturated set I. yields an MT o model M r such that M r ~ <p iff <p e I..

The first two lemmas have a standard proof. But for the proof of the Henkin Lemma, we must spell out in detail the construction of M r .

We assume that every consistent RTo set can be extended to a maximal, RT 0 consistent saturated set. Given a maximal RT 0-consistent, saturated set I. , we have a collectio.n of con­ stants occurring in I., I.e, that will form the basis of our mereotopology; equivalence classes of these constants repre­ sent our objects. But since we must model C by non-empty intersection, we must in the model Mr. constructed from I., represent these objects by sets of points. We will in fact define points by means of our basic objects, by appealing to an ultrafilter-like construction. It is similar to that used e.g., by [12] to construct temporal instants from temporally ex­ tended intervals and states. Clarke [7] also suggests that the ultrafilter construction can be used to reconstruct points, but he uses just one construction adapted from Russell and Wiener that actually makes the system inconsistent as soon as there is one external connection [20]. We use two sorts of ultrafilter constructions, one for interior points (IP) and one for boundary points (BP).

We are now in a position to construct the model M l:· We associate with each equivalence class of constants [c.] ={ ci : I. ~RT0ci =c.} for each c. in I. c. the set of P?ints n[~J = { ~: (IP(a) v BP(a)) & [c.] e a}. The domam m Mr. VMr· IS

such that D ~.f:E = { n [c.) : Cn E L c}, [E ~t is an interpretation function of constants in I:c such that [c.E~t = n[c 1 , and f9.(E is a function from D~f:E to D ~t such that f Mr(.d[c.J)= il[c,J where I:~ RTocm=n(c.). We set Mr = <DMr· fMr· ffEMr>.

Lemma 6: (Henkin Lemma) M r ~ <p iff <p e I:. The proof by induction that M r ~ <p iff <p e I: is standard except for the base clause. Our axioms concern only one primitive predicate C and so we need only to check atomic formulas of the form C(x,y). What we need to show is:

C(a, b)e.L iff M r ~ C(a, b)

... :Assume that C(a,b)e.L. Then O(a,b)e.L v EC(a,b) e I: by (D3). By the "ultrafilter" constructions, this assures either that an interior point c e [aE () [bE or a boundary point c e [aE () [bE. In either case we have [aE () [bE ,;: ¢. So we have Mr~C(a,b).

+-:Now assume M r ~ C(a,b). So [aE ()[bE,;:¢ in Mr. But the common points must all either be boundary points or at least some must be interior points. By the "ultrafilter" construction then we conclude EC(a,b)e.L or O(a,b)e.L. By (D3) and (D4) then, C(a,b)el:.D

The final step in proving completeness is that we need to show that M r is a model in KI'. To show this we must show that every one of the conditions on models in RTis fulfilled. To this end, we must embed the open elements of the do­ main of M r in a classical topological space. We have already the set of points that forms the space; it is just U{il[c.J: c.e.Lc} =der.Lu. Now we must find an embedding of {Q[c.J: c. e Lc & I:~ OP(c.)} in some set of open sets in cf.J{Lu). to form the topology. We will simply take {Q[c.J: c.e.Lc & I:~ OP(c.)} U {¢} U {UX: X .S {il[c.J: c.e.Lc& I:~ OP(c.)}} =def lU to be the relevant set. <Lu, I:u> is a structure in which: (i) ¢ e I:u; (ii) x, y e lU--x n y e I:u; (iii) X .S I:u -- UX e lU; (iv) I:u e .Lu. Thus, <Lu. I:u> is a non-empty topological space (I:u is assured to be non-empty because of (All), (Al2) and the "ultrafilter" construction of points). Further, fact 7 now follows immediately from our axioms and definitions.

Fact 7: There is an embedding of D Mr (the identity function on D Mr) into <Lu. I:u> such that:

(i) [a*EM!~u; (ii) [x+yEg=[xEgM!u*[yEgM!;

(iii) [x~M!= [xE~n*[yEgM!; (iv) [-xEgM!=-·hEgM!; (v) [ixEg =int([xEg ); (vi) [cxEg9.l!=cl([x'Eg9.ll:)

We can now verify that all the conditions of RT hold of M r relative to the embedding of the previous lemma.

LemmaS:

• (i) D Mr ~ cf.J(Lu) & I:ue DMr;

(ii) 'Vxe D Mr (int(x)e D Mr & int(x),;;¢ & int(x)=int(cl(x)));

(iii) 'Vxe D Mr (cl(x)e D Mr & cl(x)=cl(int(x)));

• (iv) 'Vxe DMr (int(~x),;;¢ -+ ~xeD Mr~
• (v) 'Vxe D Mr 'Vye D Mr (int(x ny}*¢ -- x n*ye D Mr~
• (vi) 'Vxe DMr 'Vye D Mr xu*ye DMr;

(vii) 3xe DMr 3ye D Mr (x ny*f~S & int(x ny)=¢);

(viii) 3xeDMr 3yeDMr (xny=¢ & 'VzeDMr ((open(z) & x~z)-- yncl(z),;;¢));

• (ix) 'Vxe D Mr (f(x)e DMr & x ~ f(x) & open(f(x)) & (cl(f(x))ny,;;¢ -- xncl(f(y)),;;¢) & ((open(u) & x~u) f(x)~u))

The proof of (i) follows directly from the definition of DMr and (A4), (v), (vi), (vii) and (viii) follow directly from the axioms (A6, AS, All and Al2) ofRT0 respectively.

To show (ii), we note that by (A7), for each ae.Lc, iaeic so [iaEeDMr; and by (Al) C(ia,ia)e.L. So by the "ultrafilter" construction and Fact 7, there is a point in [iaE, i.e., [iaE = int([aE)*fiS.O ·

We now show that ia= icae I:, so that int([aE)=int(cl([aE)) holds of all objects D Mr· insofar as they are elements of ~u. :Eu> and where int and clare the topological operators in <l:u, .Lu>. By axiom (A3) this amounts to showing that C(b,ia)-C(b,ica). But C(b,ia)-O(b,a) and C(b,ica)-O(b,ca) by (A8), (D6) and (D3). So we need to show that O(b,a)­ O(b,ca). To this end we note: ~RToP(b,ca)-P(ib,a).

Now to the proof of O(b,a) .... O(b,ca):

... : O(b,a)-+ 3z (P(z,b) & P(z,a)) (D3) and P(a,ca) by (Dl), (D7), (A7), (A8) and (A9). By the transitivity ofP, O(b,a) ... 3z (P(z,b) & P(z,ca)) and so O(b, ca).

+-; O(b,ca) -+ 3z (P(z,b) & P(iz,a)) by (D3) and the fact we noted above. Since P(id,d) (proof from (A8) and (Dl)) and the transitivity of P, O(b,ca) -- 3z (P(iz,b) & P(iz,a)). So O(b,ca) -- 3z' (P(z',b) & P(z',a)) and so O(b,ca) -+ 0: b,a).D

To prove (iii), we see that by (A8) and (A9), 'Vaeic, cae.Lc so [caE eD Mr· Let's now show that cx=cixe.L, so that by Fact 7, cl([xE) = cl(int([d)) in M !· If a=a*, then since ca*=a* by (A9) and ia*=a* (since ~RT0'Vx NTP(x,a*)), cl(x) = cl(int(x))) in M !·If a,;:a*, ca=cia .... -i(-a)=-i(-ia) by (D7). Since --a=a, ca=cia .... i( -a)=i( -i( --a)), then ca=cia - i(-a)=i(c(-a)), but i(-a)=i(c(-a)) is true by the previous result exploiting again the correspondence in Fact 7.0

To show (iv), we note that by (A7), 'Vae.Lc (a,;;a* ... -ae.Lc), so if[al!;t.Lu then ~[aE eDMr· But 'VaeD ~t (a;tiu .... int(~ax),;;¢) since int(~a),;;¢ .... cl(a),;;I:u and cl(a),;;Iu­ ~u (cf lemma in the proof of RTT ~ (A7)); so if int(~[aE)*fiS then ~[aE e DMr·

Finally, to show (ix), we note that by (A13) 'Vaeic nae I:c so [naE e D Mr and [aD ~ [naE & open([naE) & 'Vbe Ic ((open([bE) & [aE~[bE) -+ [naE~[bE)). It suffices now to show that 'Vbe I:c (cl([naE)n[bE,;;¢ -+ [aEncl([nbE),;;¢). We have -.C(x,y) -+ (C(x,c(ny)) .... C(c(nx),y))e :E, directly from Fact 3 and Fact 2, and C(x,y) -+ (C(x,c(ny) & C(c(nx),y))ei: since P(x,cnx) and P(y,cny) are trivial facts in RT0.0

From the Lindenbaum, Witness and Henkin lemmas, the desired result now follows:

Theorem 9: Every RT o consistent set of sentences has a model in the class RT; or equivalently, ~RT<i>- ~RT~.

S Extension : Microscopization

In this section, we explore one refinement of commonsense mereotopology. RTo meets our requirements for a topology exemplifying a relational conception of space without math­ ematical points. For many reasoning tasks and for the semantics of NL expressions this information is sufficient (See e.g. [4] for details). When, for instance, a cup is on top of a table, the proper semantics for the relation between the cup and the table is weak contact. However, looking much closer we may see that there are objects or a space between the cup and the table. As we refine the granularity of our space (that is, as we consider smaller and smaller size objects), we eliminate weak contact relations. Note that this revision never happens for an external connection, for we cannot find any object between the stem and the cup of the glass, or between one's hand and one's wrist.

This sort of refinement is also present in changes of granu­ larity signified by the use of certain modals in NL. Consider again, for example, the sentences (1) and (2) above in which there is arguably a shift in granularity--passing, e.g., from the description of an object as a point to one where it is de­ scribed as a surface. Superficially, these descriptions are in­ consistent5, so we suppose that there is some sort of shift from one model or world to another. We call this sort of shift of granularity microscopization. We can suppose that this process of refinement of granularity continues to a "limit" as follows. We suppose that we can find parts of each object in the space. Next, we suppose we could find parts of those parts, and so on forming a sequence of objects decreasing in size. These sequences of objects are, mathematically speak­ ing Cauchy sequences; and if we suppose that the limits of these sequences exist, then we will have constructed dense spaces of points by partitioning the original objects of our commonsense conception of space based on middle-sized objects.

The use of modal adverbs like actually (in sentence (1) above) suggests that we should model this process of reflec­ tion modally, each world will reflect an increasingly fine­ grained view of what the parts of objects are. At the end, we pass from the notion of a physical part to a mathematical part. We can axiomatize the idea that there are worlds of commonsense mereotopology and there are refined worlds with traditional, mathematical conceptions of topology.

The modal extension for LRT that we envision will include a modal operator [m]. To the usual clauses for a first order language, we add: if <pis a formula of L RT· then [m]<p is also a formula. A modal RTo model is a quintuple, <W, D, R, c, [D>, where W is a nonempty set (of worlds), D a function from W into a discrete, "pseudotopological" structure of the sort outlined in the semantics for LRT in section 1 above; R a transitive and asymmetric alternativeness relation in W; can injective counterpart function from D(w) into D(w') for each w and w' such that wRw' such that if anb :1:- ¢ in w then for all w' such that wRw' c(a)nc(b) :1:- ¢in w'; and [Dan assign­ ment to each nonlogical constant of an appropriate intension (function from worlds to extensions).

The domain of each accessible world is strictly larger than its R-predecessors (it is this that allows us to capture the asymmetry of R), reflecting the refinement of the granularity size of objects. We further suppose that for each object a in wand wRw', w' contains additional objects that are parts of a (or strictly speaking the counterpart of a). The collections of points in one world need not be the same collection in an­ other, but an object (collection of points in one world) will always have a counterpart in each accessible world. Finally, we suppose a limit to the R chains in which every object is the sum of points without interiors. This falsifies certain ax­ ioms of RT 0 at the limit worlds--namely the axiom that every object has a nonempty interior. These limit worlds are classica! topologies of the sort we used to build the models for RTo. We insist that every world other than a limit world is in effect a model in KI', and the limit worlds verify all except (Al), (A8), (All), (Al2) and (A13). We will call the class of all modal models MRT. Because MK1' is a modal semantics with variable domains, we must change the notion of truth and validity. Following standard techniques (see [11]) we will say that a formula <pis either verified (1) falsified (0) or undefined at a world. An atomic formula <p is undefined at w if it contains a constant that denotes an object ~ D(w) or a variable whose assignment is not in D(w). The recursive satisfaction definition follows the strong Kleene semantics. We say that <pis MRT valid iff in every MK1' model M and every world w in M if <p is defined at w in M, then <p is true at win M.

5The "points" referred to here are in effect extended objects, i.e. they have nothing to do with the abstract points in the models, but they are subject to constraints that are incompatible with those constraints that define surfaces (see [4] for the definitions of NL notions of point, border and surface objects in RT o).

Axiomatization: In addition to the axioms (A2-7) and (A9l 0) of RT o, we now have the axioms below for MRT o (modal RTo). We define LIMIT as:

LIMIT -def 3wV'u (P(w, u) & -, C(w, u) & (u :1:- w - C(u,

u))) & V'xV'y (C(y, x) - O*(y, x)) & -,(A12) & -,(Al3)

This formula describes these limit worlds; it asserts the existence of ¢ which is unique by extensionality. Below we will refer to this element as Null and its existence if only in limit worlds prompts us to add a new notion of overlap (0*). Of interest are the axioms (B 1), (B2), and (B7)-(B 10) and Nee*. (B2) says that once two objects are connected they are always connected under microscopization. (B8) captures the process of microscopization, while (B9) says that a micro­ scopization of the current world always exists or else the current world is already a limit world. (B7) asserts that such limit worlds exist. (B 10) asserts that the whole space is con­ nected, while (B 1) and (Nee*) say that the normal axioms of RT o hold except at limit worlds.

(B1) ((AI) & (A8) & (All) & (Al2) & (A13)) v LIMIT

• (B2) V'xV'y(C(x,y) - [m]C(x,y))
• (B3) [m]<p - [m][m]<p

(B4) [m]V'x<p - V'x[m]<p

(B5) 3x[m]V'y P(y, x)

• (B6) <p-'JI- [m](<p++'JI)
• (B7) [m]-,[m]-,LIMIT

(B8) [m]V'x[m]3y, y' ((P(y, x) & P(y', x) & -,O(y, y'))

(B9) ([m]<p - -,[m]-,<p) v LIMIT

(BlO) Con(a*)

(D3') O*(x,y) -def 3z (z :1:- Null & P(z,x) & P(z,y))

Nee*: For all instances of the axioms of FOL with identity, (A2-7), (A9-10), (Bl-10) <p, ~MRTo [m]<p

6 Related Work

Qualitative spatial reasoning has in the past focussed more on reasoning about orientations than on topology. A number of authors have defined topological relations from orienta­ tiona) primitives, extending Allen's interval calculus [1] to 3 dimensions (for instance [15]), but it is easily shown that mereotopological concepts such as overlap or external con­ nection can be correctly grasped in this case only for a quite limited domain of parallelepedic objects [20].

Others such as [8] use a domain of points and all the po­ wer of classical topology (and Euclidean geometry), on the grounds that it was the only sound theory modelling these concepts. Our work shows that an alternative based on a naive conception of space as it is expressed in NL can be developed rigorously at least as far as the topology is concerned. Furthermore, the full topology of IR3 is a higher order concept and we have proposed a first-order and axiomatizable alternative.

As far as we know, the only other mereotopological ap­ proach in qualitative reasoning apart from ours has been ta­ ken by the AI group in Leeds, the last version of their theory being presented in [16]. While also based on Clarke's propo­ sal, they remove the topological definitions of interior and closure. They also change the complement definition so that it is equivalent to the two following axioms Vx 3y Vu (C(u,y) - -,NTPP(u,x)) and P(x,y) - Vu 3v (C(u,v) & (C(x,v) -+ NTPP(v,y))). As shown in [16], these imply that there can be no atoms, and that it is now impossible to assert the existence of interiors--otherwise the theory is inconsis­ tent. This last feature is one of the motivations for the change in the theory, since for them, differentiating between an individual, its closure and its interior has no cognitive support. On our point of view, it is on the contrary cogniti­ vely important to be able to view material objects as closed individuals and their complements as open ones, so that their interpretations don't share any point. Indeed, we don't want the air around the glass to have a "glass boundary" belonging to it, that is why in RTo, the glass and the air are in weak contact. But in [16], an object and its complement are exter­ nally connected, and so in that theory the unintuitive conse­ quence about glass boundaries seems to follow unless one does a lot of fiddling with the way we refer to objects in NL. We have two strong motivations for wanting topological operators in our theory, one being the possibility of defining strong contact and weak contact, the other being that we think it ontologically important to be able to recover classical topology as a "limit" model, which we do in the process of microscopization. Note that the authors of [16] don't provide any soundness or completeness proofs for their theory.

Recently, in formal ontology there has been much work done on the ontological relation between mereological con­ cepts and topological ones. [19] provides a nice description and a classification of this work. One active trend in this field is to show that mereology alone supports topology, at the cost of having domains containing both extended indivi­ duals and boundaries [9, 5, 17]. It seems to us important to guarantee the ontological homogeneity of the domain, in or­ der to avoid the need to classify a priori the spatial entities we will represent in the theory, which even if metaphysically justifiable does not seem to us relevant to spatial reasoning tasks in AI. Besides, we have already stressed the fact that no linguistically described entity corresponds to an infinitely thin mathematical object, so that considering boundaries as constructs more abstract than extended individuals, as we do, is cogni tively grounded. In addition, we note that none of these authors provide a soundness or completness proofs to support their intuitions about the kind of models their theories are supposed to have.