Polytopological Semantics for Intuitionistic Modal Logics

TL;DR

This paper introduces polytopological semantics for intuitionistic modal logics, interpreting operators through topologies with closure or derivative operators, and proves soundness and completeness for these models.

Contribution

It develops a novel polytopological framework for constructive and G"odel--Dummett intuitionistic modal logics, establishing their soundness and strong completeness.

Findings

Models validate various intuitionistic modal logics.

Regularity conditions ensure the spaces validate the logics.

All considered logics are sound and strongly complete with respect to the semantics.

Abstract

We develop polytopological semantics for various constructive, intuitionistic, and G\"odel--Dummett variations of $\mathsf{K4}$ and $\mathsf{S4}$. In our models, intuitionistic and modal operators are interpreted via various topologies over a single set, equipped with either the closure or derivative operators. We identify regularity conditions to ensure that spaces validate each of our target logics and prove that all the logics considered are sound and strongly complete with respect to their respective semantics.