Compared to temporal logics, modal logics of space have received very little attention. I can see two reasons for this. First, temporal logic has its roots in the semantics of natural language; here, the notion of tense naturally leads to an extension of classical logics with temporal modal operators. In most familiar languages spatial concepts seem to play a less pervasive role, notwithstanding the many expressions that could be interpreted as spatial modalities. Also, the development of temporal logic has been boosted by concerns from computer science, in the context of program specification and verification. Here temporal properties are of greater interest than spatial ones.
A second reason is perhaps that it is more evident which ontologies to employ when formalizing the notion of time; apart from some notable exceptions, the standard temporal structure consists of a set of time points together with some kind of ordering of these points. When devising a formal model of space we seem to be faced with a far greater choice. Even if we decide to restrict ourselves to points as spatial objects, there are a great number of interesting relations to consider, such as nearness, collinearity, betweenness or equidistance. But also, the restriction to points as the sole entities of the mathematical model is more debatable than in the temporal case. For, space is inhabited by various kinds of things, such as lines, spheres, planes, poyhedra, etc.
Nevertheless, in recent years the interest seems to be growing in the use of modal logics for qualitative reasoning about spatial relations between objects. This increased interest stems from intended applications in the areas of Knowledge Representation and the theory of Geographical Information Systems. It is not our intention here to survey the variety of these recently developed modal logics of space — the reader is referred to Lemon or Lemon & Pratt. In any case, it is clear that as yet, no consensus has been reached as to what the modal logic of space would be.
The aim of this paper is to take a class of very simple structures, a very simple modal language to talk about it, and to give a detailed account of the arising modal logic. In this way we hope to arrive at one sort of basic spatial logic, in the same way that S5 and K are basic modal logics, or K t a basic temporal one.
Now projective planes are probably the simplest spatial structures around (in our account we have based ourselves on the treatment in Heyting but the facts on projective geometries used here can be found in any textbook on geometry). There seem to be two kinds of approaches to projective planes: they are either formalized as what we call collinearity frames, that is, structures consisting of points related by a ternary collinearity relation satisfying certain properties; or as two-sorted structures consisting of points and lines related by a binary incidence relation.
We take the second approach here since it seems to be the simplest. Also, since more complex spatial ontologies may be inhabited by various creatures, it seems quite natural for spatial logicians to get acquainted with many-sorted modal logics. In fact, we want to make a case for sorted modal logics as description languages for spatial structures. In the next section, we define a projective plane to be a two-sorted structure F = (P,L,I) with P and L being two disjoint sets, of points and lines, respectively; and I ? P × L an incidence relation satisfying some simple conditions. It naturally follows that our corresponding modal language MLG is two-sorted as well: we will distinguish point formulas and line formulas. The language then will have two diamonds with respectively the incidence relation and its converse as accessibility relation. These diamonds thus turn respectively line formulas into point formulas, and vice versa. Apart from some obvious adaptations, this sortedness can be incorporated in the general framework of modal logic quite smoothly.
The main results of the paper are the following. Theorem 4.2 is a completeness result: in Definition 4.1 we provide a strongly sound and complete axiom system for the two-sorted modal logic of projective planes. Theorem 5.1 states that it is decidable whether a given MLG -formula is satisfiable in a projective plane. Finally, Theorem 6.1 is a complexity result; we prove that the satisfaction problem for the class of projective planes is nexptime complete.
There are a few papers in the literature that are closely related to this approach. I got interested in the subject through a paper Balbiani et alii, which also takes two-sorted geometrical structures as a basis. The main difference is that Balbiani cum suis wish to stay within the framework of one-sorted modal logic. Their approach is to turn two-sorted structures into multi-dimensional one-sorted structures; the ‘possible worlds’ in their modal structures are so-called ‘tips’, that is, pairs consisting of a point and a line. The price they have to pay for this is a relatively involved axiomatization and an (as yet) open decidability problem. A modal logic of one-sorted projective geometries (of arbitrary but fixed finite dimension) is developed in Stebletsova. Here the earlier mentioned collinearity frames are the basic ontologies. Stebletsova’s prime aim is to find axiomatizations for classes of socalled Lyndon algebras; these are relation algebras arising as the complex algebras of structures induced by the collinearity frames. Third, when preparing the final version of this manuscript, I learned that independently, Ph. Balbiani has obtained some of the results reported on in this paper. The reader may find his account in Balbiani.
Finally, there are some obvious directions for further research that we hope to report on in the future. For instance, in this paper we only consider the binary relation of incidence, but it would be interesting to consider modal logics of richer geometrical structures; immediate candidates are the relations of parallelism, orthogonality and betweenness. Another road would lead to a study of the modal logic of projective geometries of higher dimensions; here we might stick to a two-sorted modal logic of points and lines, but in a fixed finite dimension, say n, it seems more natural to consider n-sorted modal logics.
Overview In the next section we formally introduce the syntax and semantics of our modal language MLG. Section 3 is about quasi-planes; these are two-sorted structures that look like projective planes but are a bit easier to work with; they play an important technical role in this paper. In section 4 we define a Hilbert style axiom system AXP, and we state and prove this system to be strongly sound and complete with respect to the class PP of projective planes. The short section after that concerns the decidability of MLG with respect to the class PP. Section 6 is about complexity issues: we show that the problem whether an MLG -formula is satisfiable in a projective plane, is nexptime-complete. Finally, in the last section we sketch some directions for further research. Acknowledgements I am indebted to V. Stebletsova for discussions on the modal logic of geometries (and for the L ATEX-code producing the picture of Pappus’ Theorem), and to M. Marx for help in proving the complexity result.
Download
PDF Ebook Points, lines and diamonds: a two-sorted modal logic for projective planes
