On Binding in the Spatial Logics for Closure Spaces.

We present two different extensions of the spatial logic for closure spaces (SLCS), and its spatio-temporal variant ( $$\tau $$ SLCS), with spatial quantification operators. The first concerns the existential quantification on individual points of a space. The second concerns the quantification on sets of points. The latter amounts to a form of quantification over atomic propositions, thus without the full power of second order logic. The spatial quantification operators are useful for reasoning about the existence of particular spatial objects in a space, their spatial relation with respect to other spatial objects, and, in the spatio-temporal setting, to reason about the dynamic evolution of such spatial objects in time and space, including reasoning about newly introduced items. In this preliminary study we illustrate the expressiveness of the operators by means of several small, but representative, examples.