Modal logic of planar polygons

TL;DR

This paper investigates the modal logic of polygons in the Euclidean plane, establishing its axiomatization, completeness, computational complexity, and certain logical properties.

Contribution

It introduces a finite axiomatization and completeness result for the modal logic of planar polygons, and analyzes its computational and logical properties.

Findings

Logic is finitely axiomatizable

Completeness with respect to crown frames

Validity problem is PSPACE-complete

Abstract

We study the modal logic of the closure algebra $P_2$, generated by the set of all polygons in the Euclidean plane $\mathbb{R}^2$. We show that this logic is finitely axiomatizable, is complete with respect to the class of frames we call "crown" frames, is not first order definable, does not have the Craig interpolation property, and its validity problem is PSPACE-complete.