Modal Logics of Metrics and Topology
by
FRANK WOLTER
Department of Computer Science, University of Liverpool, UK

In 1944, McKinsey and Tarski proved that S4 is the logic of topological interior and closure of any metric separable dense-in-itself space. Thus, the logicof topological interior and closure over arbitrary metric spaces coincides with the logic of the real line, the real plane, and any metric separable dense-in-itself space,it is finitely axiomatizable, and PSpace-complete. Because of this result, S4 hasbecome a logic of prime importance in Qualitative Spatial Reasoning in AI. And in Logic this result has triggered the investigation of a number of variants and extensions of S4 for reasoning about qualitative aspects of metric spaces.

In parallel (but without much interaction) to this line of research, Philosophical Logicand AI have suggested and investigated a variety of logics --- such as conditional logics, certain nonmonotonic logics, and logics of comparative similarity --- which are naturally interpreted in metric (or distance) spaces and which contain a binary operator for comparing distances between points in a distance space.

In the talk, I will discuss a uniform framework covering large parts of these two lines of research, thus enabling a comparison of the logics involved and a systematic investigation of their expressive power and complexity. This framework is obtained by decomposing the underlying modal operators into two-sorted first-order quantifier patterns. Within this framework, two classes of languages are investigated in detail: (1) A natural fragment of the resulting two-sorted first-order logic can be captured bythree binary modal operators each of which compares distances in a certain way. Due to its greater expressive power, this language turns out to behave quite differentfrom Tarski's S4: the logic of all metric spaces is finitely axiomatizable and ExpTime-complete, but the logic of the real line (and various other important metric spaces) is not recursively enumerable. This result is proved by an encoding of Diophantine equations. (2) Another natural fragment is obtained by considering languages with limited quantification but constants for rational numbers. In this case, the logic of arbitrary metric spaces is again finitely axiomatizable and ExpTime-complete. The logic of the real line is different from this logic but still finitely axiomatizable and even PSpace-complete. In fact, this logic turns out to be closely related to well-known metric temporal logics.

The talk is based on joint work with D. Tishkowsky, M. Sheremet and M. Zakharyaschev.

Date received: May 30, 2007