Dynamic contact algebras and quantifier-free logics for space and time

P. Dimitrov ; D. Vakarelov

Sibirskie èlektronnye matematičeskie izvestiâ, Tome 15 (2018), pp. 1103-1144

Résumé

The paper is in the field of Region Based Theory of Space (RBTS), sometimes called mereotopology. RBTS is a kind of point-free theory of space based on the notion of region. Its origin goes back to some ideas of Whitehead, De Laguna and Tarski to build the theory of space without the use of the notion of point. Contact algebras present an algebraic formulation of RBTS and in fact give axiomatizations of the Boolean algebras of regular closed sets of some classes of topological spaces with an additional relation of contact. Dynamic contact algebras (DCA), are generalizations of contact algebras studying regions changing in time and present formal explications of Whitehead's ideas of integrated point-free theory of space and time. In the present paper we propose several new types of dynamic contact algebras and quantifier-free logics based on them. The logics are finitary, based on Modus Ponens and some nonstandard inference rules which replace the non-universal axioms of the corresponding DCA. In fact these logics can be considered as axiomatizations of the universal fragment of the first-order theory of the corresponding DCA. They can be treated as kinds of non-standard temporal logics for spatial regions changing in time. The difference with standard temporal logic is that we do not use temporal operators but temporal predicates. We present also snapshot semantics and Kripke style relational semantics for some of these logics, based on relational models for the corresponding DCA. The relational semantics helps to use some techniques adapted from modal logic to study some metalogical properties of the studied systems.

Détail

Keywords: region-based theory of space and time, contact algebra, dynamic contact algebra, representation theorem, quantifier-free first-order theory, rule-elimination theorem, non-standard temporal logic.