Taming the `elsewhere': On expressivity of topological languages

TL;DR

This paper investigates the expressive power of topological modal logic, demonstrating that the Cantor derivative can define properties beyond those expressible by closure and elsewhere operators, through a new morphism theory.

Contribution

It proves that the Cantor derivative alone is strictly more expressive than closure and elsewhere combined, introducing a novel morphism framework for this logic.

Findings

Cantor derivative can define properties not expressible with closure and elsewhere

Development of a new morphism theory preserving formulas with the elsewhere operator

Affirmative answer to the open question by Kudinov and Shehtman

Abstract

In topological modal logic, it is well known that the Cantor derivative is more expressive than the topological closure, and the `elsewhere,' or `difference,' operator is more expressive than the `somewhere' operator. In 2014, Kudinov and Shehtman asked whether the combination of closure and elsewhere becomes strictly more expressive when adding the Cantor derivative. In this paper we give an affirmative answer: in fact, the Cantor derivative alone can define properties of topological spaces not expressible with closure and elsewhere. To prove this, we develop a novel theory of morphisms which preserve formulas with the elsewhere operator.