arxiv: 2604.23234 · v1 · submitted 2026-04-25 · 🧮 math.LO

Recognition: unknown

Polytopological Semantics for Intuitionistic Modal Logics

Juan P. Aguilera , David Fern\'andez-Duque , Leonardo Pacheco

Authors on Pith no claims yet

Pith reviewed 2026-05-08 06:43 UTC · model grok-4.3

classification 🧮 math.LO

keywords intuitionistic modal logicpolytopological semanticssoundnesscompletenessK4S4closure operatorderivative operator

0 comments

The pith

Polytopological spaces equipped with closure and derivative operators provide sound and strongly complete semantics for intuitionistic modal logics including K4 and S4 variants.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops a new semantics for intuitionistic and constructive modal logics by placing several topologies on the same set. One topology handles the intuitionistic part using closure or derivative operators, while another handles the modal operators. The authors specify regularity conditions on these topologies that make the models validate specific logics. They then establish that the logics are sound and strongly complete with respect to these models. This offers a unified topological framework for logics that combine intuitionistic and modal reasoning.

Core claim

We develop polytopological semantics for various constructive, intuitionistic, and Gödel--Dummett variations of K4 and 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.

What carries the argument

Polytopological models on a shared set where different topologies interpret the intuitionistic connectives and the modal operators separately through closure or derivative.

If this is right

The semantics are sound for each of the considered logics under the identified regularity conditions.
Strong completeness holds, so every theorem is valid in all models and every consistent theory has a model.
The approach covers constructive, intuitionistic, and Gödel-Dummett variants of K4 and S4.
Regularity conditions prevent unintended interactions between the intuitionistic and modal fragments.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

This framework may allow for the study of hybrid logics combining different nonclassical systems in a topological setting.
Potential extensions could involve applying these models to specific mathematical structures like topological spaces with additional structure.
Further work might explore algorithmic or computational aspects of validity in these polytopological models.

Load-bearing premise

Multiple topologies on one set can be chosen so that their closure or derivative interpretations capture the desired intuitionistic and modal behaviors without forcing extra logical consequences or needing excessive restrictions.

What would settle it

Finding a formula that is a theorem of one of the target logics but fails to hold in every regular polytopological model for that logic, or a non-theorem that is valid in all such models.

Figures

Figures reproduced from arXiv: 2604.23234 by David Fern\'andez-Duque, Juan P. Aguilera, Leonardo Pacheco.

**Figure 1.** Figure 1: Schematics for forward (left), backward (center), and downward (right) confluence. Solid view at source ↗

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper sets up polytopological models with multiple topologies on one set to interpret intuitionistic and modal operators together, then proves soundness and strong completeness for several variants under added regularity conditions.

read the letter

The main point is a uniform semantic framework that puts several topologies on a single carrier set and uses closure or derivative operators to handle both the intuitionistic fragment and the modal one for constructive versions of K4 and S4, including some Gödel-Dummett cases. The construction itself looks like the fresh piece; it is not just a relabeling of ordinary topological models for S4 or plain intuitionistic logic, and it pulls together scattered results into one setting. The authors spell out regularity conditions to keep the topologies from interfering and then give direct soundness and strong-completeness arguments for each target logic. That part is straightforward and avoids any obvious circularity or parameter-fitting. The proofs are claimed to be non-vacuous once the conditions are imposed, which is the sort of concrete evidence that matters here. The regularity conditions are the soft spot worth checking. They are meant to block cross-effects such as a modal closure turning an intuitionistic open set into something unintended, but it is not yet clear from the abstract whether they are also necessary or whether they exclude standard Kripke frames that the logics are supposed to generalize. If the conditions turn out to force extra commutation between the operators or shrink the class of models too much, the completeness results become narrower than they first appear. A reader working in constructive modal logic or topological semantics would get the most out of this; the uniform treatment and the explicit conditions make it worth a close look for anyone building on completeness theorems in the area. I would send it to peer review so the details of the conditions and the embedding of ordinary frames can be verified.

Referee Report

2 major / 2 minor

Summary. The paper develops polytopological semantics for various constructive, intuitionistic, and Gödel-Dummett variants of K4 and S4. In these models a single carrier set is equipped with multiple topologies; intuitionistic operators are interpreted via one topology (using closure or interior) while modal operators use another (via closure or derivative). The authors isolate regularity conditions on the topologies that ensure the spaces validate the target axioms, then prove soundness and strong completeness for each logic with respect to its corresponding class of polytopological models.

Significance. If the regularity conditions are non-vacuous and the completeness proofs hold, the work supplies a unified topological semantics that simultaneously handles the intuitionistic and modal fragments without collapsing them into a single topology. The direct semantic construction and the explicit identification of sufficient regularity conditions constitute a clear technical contribution to the literature on intuitionistic modal logic.

major comments (2)

[§4] §4 (regularity conditions): the paper must verify that the listed conditions do not force the modal closure of an intuitionistically open set to remain open (or force derivative operators to collapse), as this would impose unintended commutation between the two fragments. A concrete counter-example or invariance argument is needed to confirm the conditions are not overly restrictive.
[Theorem 5.3] Theorem 5.3 (strong completeness): the proof sketch relies on the regularity conditions blocking cross-interference, but the argument that every consistent set is satisfiable in a regular polytopological model is only outlined; the construction of the canonical model must be shown to inherit the required regularity properties.

minor comments (2)

Notation for the two topologies (e.g., τ_I vs. τ_M) should be introduced once and used consistently; occasional reuse of τ for both creates ambiguity in the semantic clauses.
The abstract claims 'all the logics considered' receive strong completeness, yet the introduction lists six variants; an explicit table mapping each logic to its exact regularity conditions and completeness theorem would improve readability.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive comments on our manuscript. We address the major points below and will revise the paper to incorporate the suggested clarifications and expansions.

read point-by-point responses

Referee: [§4] §4 (regularity conditions): the paper must verify that the listed conditions do not force the modal closure of an intuitionistically open set to remain open (or force derivative operators to collapse), as this would impose unintended commutation between the two fragments. A concrete counter-example or invariance argument is needed to confirm the conditions are not overly restrictive.

Authors: We agree that it is essential to confirm the regularity conditions do not force unintended commutation or collapse between the intuitionistic and modal fragments. The current manuscript identifies the conditions to validate the target axioms but does not explicitly include a verification via counterexample or invariance argument. In the revised version we will add a subsection to §4 providing a concrete counterexample of a polytopological space satisfying the regularity conditions in which the modal closure of an intuitionistically open set is not open, together with a brief invariance argument showing the conditions remain non-vacuous under the relevant operations. revision: yes
Referee: [Theorem 5.3] Theorem 5.3 (strong completeness): the proof sketch relies on the regularity conditions blocking cross-interference, but the argument that every consistent set is satisfiable in a regular polytopological model is only outlined; the construction of the canonical model must be shown to inherit the required regularity properties.

Authors: The referee correctly observes that the proof of Theorem 5.3 outlines the canonical-model construction without fully verifying inheritance of the regularity properties. We will expand the proof in the revised manuscript to explicitly construct the canonical polytopological model from maximal consistent sets and demonstrate that the induced topologies satisfy the regularity conditions, using the consistency of the logic to ensure the required closure and derivative properties hold without cross-interference between fragments. revision: yes

Circularity Check

0 steps flagged

No circularity: direct semantic construction and standard completeness proofs

full rationale

The paper defines polytopological models by placing multiple topologies on a single carrier set and interpreting intuitionistic and modal operators via closure or derivative operators. It then states regularity conditions on these spaces and proves soundness plus strong completeness for each target logic. These steps consist of explicit model definitions followed by routine verification that the axioms hold and that every consistent set is satisfiable in some model; no equation reduces a claimed result to a fitted parameter, no prediction is obtained by renaming an input, and no load-bearing premise rests on a self-citation chain. The provided abstract and reader summary confirm the argument is self-contained against external semantic benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The work rests on the standard axiomatizations of the target logics and on basic topological notions; the main addition is the polytopological model class plus regularity conditions.

axioms (2)

standard math Standard axioms and rules of the intuitionistic, constructive, and Gödel-Dummett variants of K4 and S4.
These are the background logics whose semantics are being supplied.
domain assumption Topological spaces admit closure and derivative operators that can be used to interpret modal and intuitionistic connectives.
Invoked when defining the interpretation of the operators.

pith-pipeline@v0.9.0 · 5372 in / 1311 out tokens · 34612 ms · 2026-05-08T06:43:28.541478+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

22 extracted references · 11 canonical work pages

[1]

In Laurent Fribourg, editor:Computer Science Logic, 15th Interna- tional Workshop, CSL 2001

Natasha Alechina, Michael Mendler, Valeria de Paiva & Eike Ritter (2001):Categorical and Kripke Seman- tics for Constructive S4 Modal Logic. In Laurent Fribourg, editor:Computer Science Logic, 15th Interna- tional Workshop, CSL 2001. 10th Annual Conference of the EACSL, Paris, France, September 10-13, 2001, Proceedings,Lecture Notes in Computer Science214...

2001
[2]

Ryuta Arisaka, Anupam Das & Lutz Straßburger (2015):On Nested Sequents for Constructive Modal Logics. Log. Methods Comput. Sci.11(3). Available athttps://doi.org/10.2168/LMCS-11(3:7)2015

work page doi:10.2168/lmcs-11(3:7)2015 2015
[3]

arXiv:arXiv:2403.00201

Philippe Balbiani, Martín Diéguez, David Fernández-Duque & Brett McLean (2024):Constructive S4 modal logics with the finite birelational frame property.arXiv. arXiv:arXiv:2403.00201

work page arXiv 2024
[4]

ACM70(5), pp

Alexandru Baltag, Nick Bezhanishvili & David Fernández-Duque (2023):The Topological Mu-Calculus: Completeness and Decidability.J. ACM70(5), pp. 33:1–33:38, doi:10.1145/3623268

work page doi:10.1145/3623268 2023
[5]

469–475, doi:gmj-2015-0041

Guram Bezhanishvili, Nick Bezhanishvili, Joel Lucero-Bryan & Jan van Mill (2015):S4.3and hereditarily extremally disconnected spaces.Georgian Mathematical Journal22(4), pp. 469–475, doi:gmj-2015-0041

2015
[6]

325–355, doi:10.1007/s11225-005-4648-6

Guram Bezhanishvili, Leo Esakia & David Gabelaia (2005):Some Results on Modal Axiomatization and Definability for Topological Spaces.Studia Logica81(3), pp. 325–355, doi:10.1007/s11225-005-4648-6

work page doi:10.1007/s11225-005-4648-6 2005
[7]

Davoren (2007):Topological Semantics and Bisimulations for Intuitionistic Modal Logics and Their Classical Companion Logics

Jennifer M. Davoren (2007):Topological Semantics and Bisimulations for Intuitionistic Modal Logics and Their Classical Companion Logics. In Sergei N. Artëmov & Anil Nerode, editors:Logical Foundations of Computer Science, International Symposium, LFCS 2007, New Y ork, NY , USA, June 4-7, 2007, Proceed- ings,Lecture Notes in Computer Science4514, Springer,...

work page doi:10.1007/978-3-540-72734-7_12 2007
[8]

Model enumeration of two-variable logic with quadratic delay complexity

Jim De Groot, Ian Shillito & Ranald Clouston (2025):Semantical Analysis of Intuitionistic Modal Logics between CK and IK. In:2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pp. 169–182, doi:10.1109/LICS65433.2025.00020

work page doi:10.1109/lics65433.2025.00020 2025
[9]

Methods Comput

David Fernández-Duque (2018):The intuitionistic temporal logic of dynamical systems.Log. Methods Comput. Sci.14(3), doi:10.23638/LMCS-14(3:3)2018

work page doi:10.23638/lmcs-14(3:3)2018 2018
[10]

Santiago Fernández, D

S. Santiago Fernández, D. Fernández-Duque & J.J. Joosten (2026):The Complexity of the Constructive Master Modality. Submitted

2026
[11]

Gisèle Fischer Servi (1977):On modal logic with an intuitionistic base.Studia Logica36(3), pp. 141–149

1977
[12]

Gisèle Fischer Servi (1984):Axiomatizations for some intuitionistic modal logics.Rend. Sem. Mat. Univers. Politecn. Torino42(3), pp. 179–194

1984
[13]

[BBMP24] M

Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales & Lutz Straßburger (2023):Intuition- istic S4 is decidable. In:38th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2023, Boston, MA, USA, June 26-29, 2023, IEEE, pp. 1–13, doi:10.1109/LICS56636.2023.10175684

work page doi:10.1109/lics56636.2023.10175684 2023
[14]

Logic Comput

Jim de Groot & Ian Shillito (2025):IntuitionisticiS4as a logic of topological spaces.J. Logic Comput. 35(7), pp. Paper No. exae030, 25, doi:10.1093/logcom/exae030

work page doi:10.1093/logcom/exae030 2025
[15]

McKinsey & A

J.C.C. McKinsey & A. Tarski (1944):The algebra of topology.Annals of Mathematics2, pp. 141–191

1944
[16]

367–395, doi:10.1007/S11225-020-09910-5

Ricardo Oscar Rodríguez & Amanda Vidal (2021):Axiomatization of Crisp Gödel Modal Logic.Stud Logica 109(2), pp. 367–395, doi:10.1007/S11225-020-09910-5

work page doi:10.1007/s11225-020-09910-5 2021
[17]

Simpson (1994):The proof theory and semantics of intuitionistic modal logic

A. Simpson (1994):The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh, UK

1994
[18]

271–301, doi:10.1016/0168-0072(90)90059-B

Duminda Wijesekera (1990):Constructive modal logics I.Annals of Pure and Applied Logic50(3), pp. 271–301, doi:10.1016/0168-0072(90)90059-B

work page doi:10.1016/0168-0072(90)90059-b 1990
[19]

Tomasz Witczak (2019):Topological and Multi-Topological Frames in the Context of Intuitionistic Modal Logic.Bulletin of the Section of Logic48(3), pp. 187–205. Available athttp://eudml.org/doc/295593. Appendix A Strong completeness In this Appendix, we sketch the proof of strong completeness forCK4,IK4,K4I,GK4,GK4 c,CS4,IS4, S4I,GS4,GS4 c with respect to ...

2019
[20]

IfFS∈Λ, thenM Λ c is backward confluent
[21]

IfRV∈Λ, thenM Λ c is downward confluent
[22]

Proof.We consider the first item explicitly; the others are similar

IfGD∈Λ, thenM Λ c is locally linear. Proof.We consider the first item explicitly; the others are similar. Recall that FS is(♢ϕ→□ψ)→ □(ϕ→ψ). Suppose thatΦ⊏ c Ψ≼cΨ′. Letϒ=Φ∪ {♢χ:χ∈Ψ ′}. We argue thatϒis consistent, and so can be extended to a theoryΦ ′ ∈W c. If so, notice that clearly we have(Φ ′)♢ ∩Ψ ′ =∅, and moreover (Φ′)□ ⊆Ψ ′ follows from the fact that...