Closure hyperdoctrines, with paths

TL;DR

This paper develops a categorical framework called closure hyperdoctrines to systematically analyze the logical properties of closure spaces, with applications to spatial reasoning in distributed systems.

Contribution

It introduces closure hyperdoctrines as a unifying abstract framework for various models of closure spaces, enabling new spatial logics and semantic characterizations.

Findings

Provides a categorical axiomatization of closure operators

Offers sound and complete semantics for spatial logics

Unifies diverse models like topological spaces, fuzzy sets, and coalgebras

Abstract

(Pre)closure spaces are a generalization of topological spaces covering also the notion of neighbourhood in discrete structures, widely used to model and reason about spatial aspects of distributed systems. In this paper we introduce an abstract theoretical framework for the systematic investigation of the logical aspects of closure spaces. To this end, we introduce the notion of closure (hyper)doctrines, i.e. doctrines endowed with inflationary operators (and subject to suitable conditions). The generality and effectiveness of this concept is witnessed by many examples arising naturally from topological spaces, fuzzy sets, algebraic structures, coalgebras, and covering at once also known cases such as Kripke frames and probabilistic frames (i.e., Markov chains). Then, we show how spatial logical constructs concerning surroundedness and reachability can be interpreted by endowing hyperdoctrines with a general notion of paths. By leveraging general categorical constructions, we provide axiomatisations and sound and complete semantics for various fragments of logics for closure operators. Therefore, closure hyperdoctrines are useful both for refining and improving the theory of existing spatial logics, but especially for the definition of new spatial logics for new applications.