Intuitionistic S4 as a logic of topological spaces
Journal of Logic and Computation, 2024
Abstract
We design and study various topological semantics for the diamond-free intuitionistic modal logic iS4, an intuitionistic analogue of S4. Ultimately we prove that ordinary topological spaces can be used as semantics, using the specialization order to interpret intuitionistic implication and the interior for the modality. Some of our soundness and completeness results are mechanised in Coq.
Recommended citation: de Groot, Jim and Shillito, Ian. (2024). "Intuitionistic S4 as a logic of topological spaces" Journal of Logic and Computation.
Download Paper