What question did this study set out to answer?

The research focuses on proving the soundness and completeness of intuitionistic modal logic iS4 using topological semantics.

February 26, 2026Open Access

Intuitionistic S4 as a logic of topological spaces

Key Points

The research focuses on proving the soundness and completeness of intuitionistic modal logic iS4 using topological semantics.
Developed various topological semantics for iS4.
Interpreted intuitionistic implication through specialization order in topological spaces.
Utilized interior for the modality in semantics.
Mechanized results in Coq.
Established that ordinary topological spaces serve as semantics for iS4.
Proven soundness results for intuitionistic modal logic within these semantics.

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.

Intuitionistic S4 as a logic of topological spaces

Key Points

Abstract

Cite This Study

Also Consider

Also Consider