pith. sign in

arxiv: 2601.03762 · v2 · submitted 2026-01-07 · 🧮 math.LO · cs.LO

Duality for Constructive Modal Logics: from Sahqlvist to Goldblatt-Thomason

Jim de Groot , Ian Shillito , Ranald Clouston This is my paper

Pith reviewed 2026-05-16 16:58 UTC · model grok-4.3

classification 🧮 math.LO cs.LO
keywords constructive modal logicCKcategorical dualitySahlqvist correspondenceGoldblatt-Thomason theorembirelational semanticsalgebraic semanticsmodal logic completeness
0
0 comments X

The pith

A categorical duality links algebraic and birelational semantics for the constructive modal logic CK.

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

The paper carries out a semantic study of constructive modal logic CK by establishing a categorical duality between its algebraic and birelational semantics. This duality is then employed to obtain Sahlqvist-style correspondence and completeness results for the logic. Additionally, it supports a Goldblatt-Thomason-style theorem that characterizes which classes of frames are definable by formulas of the logic. These results matter because they provide a single framework for deriving semantic properties that would otherwise require separate arguments for each type of semantics.

Core claim

We provide a categorical duality linking the algebraic and birelational semantics of the logic. We then use this to prove Sahlqvist style correspondence and completeness results, as well as a Goldblatt-Thomason style theorem on definability of classes of frames.

What carries the argument

Categorical duality between algebraic semantics and birelational semantics for CK, which transfers properties between the two and enables the correspondence and definability theorems.

If this is right

  • Sahlqvist formulas in CK correspond to first-order conditions on birelational frames.
  • Completeness theorems hold for the logic with respect to both semantics via the duality.
  • Classes of birelational frames definable by CK formulas are closed under certain operations such as disjoint unions and bounded morphic images.
  • The duality allows transferring definability results from algebraic to relational settings directly.

Where Pith is reading between the lines

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

  • The approach might generalize to other constructive modal logics, offering a template for duality-based semantic studies.
  • Checking whether specific known results for CK are recovered as direct instances of the proved theorems would test the framework's utility.
  • Similar dualities could connect to classical modal logic dualities, highlighting differences in constructive settings.

Load-bearing premise

That the categorical duality provides a faithful and complete link between the algebraic and birelational semantics without additional restrictions for this constructive modal logic.

What would settle it

Finding a CK formula that is valid on all birelational frames but not on the corresponding algebra, or vice versa, would falsify the duality's faithfulness.

read the original abstract

We carry out a semantic study of the constructive modal logic CK. We provide a categorical duality linking the algebraic and birelational semantics of the logic. We then use this to prove Sahlqvist style correspondence and completeness results, as well as a Goldblatt-Thomason style theorem on definability of classes of frames.

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.

Referee Report

0 major / 3 minor

Summary. The paper claims to establish a categorical duality linking the algebraic (modal Heyting algebras) and birelational semantics of the constructive modal logic CK. It then uses this duality to prove Sahlqvist-style correspondence and completeness results, as well as a Goldblatt-Thomason-style theorem on definability of classes of frames.

Significance. If the duality holds, the work supplies a clean categorical transfer mechanism for validity and definability properties in constructive modal logic. This extends classical Sahlqvist and Goldblatt-Thomason techniques to the constructive setting without hidden classical assumptions, which is a non-trivial and useful contribution to the semantic study of CK.

minor comments (3)
  1. [Title] The title contains a typographical error: 'Sahqlvist' should be 'Sahlqvist'.
  2. [Abstract] The abstract is extremely terse and gives no hint of the duality construction or the main transfer arguments; expanding it by one or two sentences would improve readability without altering the paper's length.
  3. [Section 2] In the birelational semantics section, the notation for the two accessibility relations is introduced without an immediate concrete example; adding a small diagram or frame example would clarify the constructive features.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive evaluation of our manuscript and the recommendation for minor revision. We appreciate the recognition that the categorical duality provides a clean transfer mechanism for validity and definability results in constructive modal logic without hidden classical assumptions.

Circularity Check

0 steps flagged

No significant circularity identified

full rationale

The paper constructs a new categorical duality linking algebraic (modal Heyting algebras) and birelational semantics for CK as its primary contribution, then applies this equivalence to transfer validity and definability properties for Sahlqvist correspondence, completeness, and a Goldblatt-Thomason-style theorem. No load-bearing step reduces by definition or self-citation to its own inputs; the duality is presented as an independent equivalence of categories whose properties are established directly rather than presupposed, and the subsequent results follow from standard categorical transfer without circular reduction to fitted parameters or prior self-referential theorems.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard background axioms of modal logic and category theory with no free parameters or new entities introduced in the abstract description.

axioms (1)
  • domain assumption Standard semantics and axioms for constructive modal logic CK
    The paper assumes the usual definition and properties of CK as background for the duality construction.

pith-pipeline@v0.9.0 · 5346 in / 1172 out tokens · 38182 ms · 2026-05-16T16:58:15.738219+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

52 extracted references · 52 canonical work pages

  1. [1]

    Artemov and T

    S. Artemov and T. Protopopescu. Intuitionistic epistemic logic.The Review of Symbolic Logic, 9(2):266––298, 2016. doi:10.1017/S1755020315000374

    work page doi:10.1017/s1755020315000374 2016

  2. [2]

    Balbiani, H

    P. Balbiani, H. Gao, C ¸ . Gencer, and N. Olivetti. A natural intuitionistic modal logic: Axiomatization and bi-nested calculus. InProceedings CSL 2024, pages 1–21, 2024. doi:10.4230/LIPIcs.CSL.2024.13

    work page doi:10.4230/lipics.csl.2024.13 2024

  3. [3]

    Bellin, V

    G. Bellin, V. de Paiva, and E. Ritter. Extended Curry-Howard correspondence for a basic constructive modal logic. InMethods for Modalities 2 (M4M-2), 2001

    work page 2001

  4. [4]

    J. F. A. K. van Benthem. A note on modal formulae and relational properties.The Journal of Symbolic Logic, 40(1): 55–58, 1975. URLhttp://www.jstor.org/stable/2272270

    work page arXiv 1975

  5. [5]

    J. F. A. K. van Benthem. Modal frame classes revisited.Fundamenta Informaticae, 18:307–317, 1993. doi:10.3233/FI- 1993-182-416

    work page doi:10.3233/fi- 1993

  6. [6]

    Birkhoff

    G. Birkhoff. On the structure of abstract algebras.Mathematical Proceedings of the Cambridge Philosophical Society, 31:433–454, 1935. doi:10.1017/S0305004100013463

    work page doi:10.1017/s0305004100013463 1935

  7. [7]

    Blackburn, M

    P. Blackburn, M. de Rijke, and Y. Venema.Modal Logic. Cambridge University Press, Cambridge, 2001. doi:10.1017/CBO9781107050884

    work page doi:10.1017/cbo9781107050884 2001

  8. [8]

    Boˇ zi´ c and K

    M. Boˇ zi´ c and K. Doˇ sen. Models for normal intuitionistic modal logics.Studia Logica, 43:217–245, 1984. doi:10.1007/BF02429840

    work page doi:10.1007/bf02429840 1984

  9. [9]

    Celani and R

    S. Celani and R. Jansana. A closer look at some subintuitionistic logics.Notre Dame Journal of Formal Logic, 42(4): 225–255, 2001. doi:10.1305/ndjfl/1063372244

    work page doi:10.1305/ndjfl/1063372244 2001

  10. [10]

    S. A. Celani and R. Jansana. Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic.Logic Journal of the IGPL, 7:683–715, 1999. doi:10.1093/jigpal/7.6.683. 26

    work page doi:10.1093/jigpal/7.6.683 1999

  11. [11]

    Chagrov and M

    A. Chagrov and M. Zakharyaschev.Modal Logic. Oxford University Press, Oxford, 1997

    work page 1997

  12. [12]

    Das and S

    A. Das and S. Marin. On intuitionistic diamonds (and lack thereof). In R. Ramanayake and J. Urban, editors, Proceedings TABLEAUX 2023, pages 283–301, 2023. doi:10.1007/978-3-031-43513-3 16

    work page doi:10.1007/978-3-031-43513-3 2023

  13. [13]

    K. Doˇ sen. Duality between modal algebras and neighbourhood frames.Studia Logica, 48:219–234, 1989. doi:10.1007/BF02770513

    work page doi:10.1007/bf02770513 1989

  14. [14]

    L. L. Esakia. Topological Kripke models.Soviet Mathematics Doklady, 15:147–151, 1974

    work page 1974

  15. [15]

    L. L. Esakia.Heyting Algebras. Trends in Logic. Springer, Springer, 2019. doi:10.1007/978-3-030-12096-2. Translated by A. Evseev

    work page doi:10.1007/978-3-030-12096-2 2019

  16. [16]

    Fischer Servi

    G. Fischer Servi. Axiomatizations for some intuitionistic modal logics.Rendiconti del Seminario Matematico – Politecnico di Torino, 42:179–194, 1984

    work page 1984

  17. [17]

    Fornasiere and T

    D. Fornasiere and T. Moraschini. Intuitionistic Sahlqvist theory for deductive systems.The Journal of Symbolic Logic, pages 1–59, 2023. doi:10.1017/jsl.2023.7

    work page doi:10.1017/jsl.2023.7 2023

  18. [18]

    Gehrke and J

    M. Gehrke and J. Harding. Bounded Lattice Expansions.Journal of Algebra, 238:345–371, 2001

    work page 2001

  19. [19]

    Gehrke, H

    M. Gehrke, H. Nagahashi, and Y. Venema. A Sahlqvist theorem for distributive modal logic.Annals of Pure and Applied Logic, 131(1):65–102, 2005. ISSN 0168-0072. doi:https://doi.org/10.1016/j.apal.2004.04.007. URLhttps: //www.sciencedirect.com/science/article/pii/S0168007204000880

    work page doi:10.1016/j.apal.2004.04.007 2005

  20. [20]

    R. I. Goldblatt. Metamathematics of modal logic I.Reports on Mathematical Logic, 6:41–78, 1976

    work page 1976

  21. [21]

    R. I. Goldblatt. Metamathematics of modal logic II.Reports on Mathematical Logic, 6:21–52, 1976

    work page 1976

  22. [22]

    R. I. Goldblatt. Axiomatic classes of intuitionistic models.Journal of Universal Computer Science, 11(12):1945–1962, 2005

    work page 1945

  23. [23]

    R. I. Goldblatt and S. K. Thomason. Axiomatic classes in propositional modal logic. In J. Crossley, editor,Algebra and Logic, pages 163–173, Berlin, Heidelberg, 1974. Springer. doi:10.1007/BFb0062855

    work page doi:10.1007/bfb0062855 1974

  24. [24]

    Grefe.Fischer Servi’s intuitionistic modal logic and its extensions

    C. Grefe.Fischer Servi’s intuitionistic modal logic and its extensions. PhD thesis, Freie Universit¨ at Berlin, 1999

    work page 1999

  25. [25]

    de Groot

    J. de Groot. Positive monotone modal logic.Studia Logica, 109:829–857, 2021. doi:10.1007/s11225-020-09928-9

    work page doi:10.1007/s11225-020-09928-9 2021

  26. [26]

    de Groot.Dualities in Modal Logic

    J. de Groot.Dualities in Modal Logic. PhD thesis, The Australian National University, 2022

    work page 2022

  27. [27]

    de Groot

    J. de Groot. Goldblatt-Thomason theorems for modal intuitionistic logics. In D. Fern´ andez-Duque, A. Palmigiano, and S. Pinchinat, editors,Proc. AiML 2022, pages 467–490, 2022

    work page 2022

  28. [28]

    de Groot and D

    J. de Groot and D. Pattinson. Monotone subintuitionistic logic: Duality and transfer results.Notre Dame Journal of Formal Logic, 63(2):213–242, 2022. doi:10.1215/00294527-2022-0014

    work page doi:10.1215/00294527-2022-0014 2022

  29. [29]

    The yoneda embedding in simplicial type theory

    J. de Groot, I. Shillito, and R. Clouston. Semantical Analysis of Intuitionistic Modal Logics between CK and IK. In2025 40th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), pages 169–182, 2025. doi:10.1109/LICS65433.2025.00020

    work page doi:10.1109/lics65433.2025.00020 2025

  30. [30]

    H. H. Hansen. Monotonic modal logics. Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam, 2003. illc-MoL:2003-24

    work page 2003

  31. [31]

    H. H. Hansen and C. Kupke. A coalgebraic perspective on monotone modal logic.Electronic Notes in Theoretical Computer Science, 106:121–143, 2004. doi:10.1016/j.entcs.2004.02.028

    work page doi:10.1016/j.entcs.2004.02.028 2004

  32. [32]

    K. Kojima. Relational and neighborhood semantics for intuitionistic modal logic.Reports on Mathematical Logic, 47: 87–113, 2012

    work page 2012

  33. [33]

    Bourbaki, Lie Groups and Lie Algebras, Chapters 4–6, Elements of Mathematics, Springer-Verlag, Berlin, 2002

    A. Kurz and J. Rosick´ y. The Goldblatt-Thomason theorem for coalgebras. In T. Mossakowski, U. Montanari, and M. Haveraaen, editors,Proc. CALCO 2007, pages 342–355, Berlin, Heidelberg, 2007. Springer. doi:10.1007/978-3-540- 73859-6 23

    work page doi:10.1007/978-3-540- 2007

  34. [34]

    J. C. C. McKinsey and A. Tarski. The algebra of topology.Annals of Mathematics, 45:141–191, 1944. doi:10.2307/1969080

    work page doi:10.2307/1969080 1944

  35. [35]

    Mendler and V

    M. Mendler and V. de Paiva. Constructive CK for contexts. InProceedings CRR 2005, 2005

    work page 2005

  36. [36]

    Moraschini

    T. Moraschini. A Gentle Introduction to the Leibniz Hierarchy. In J. Malinowski and R. Palczewski, editors,Janusz Czelakowski on Logical Consequence, volume 27 ofOutstanding Contributions to Logic, pages 123–201. Springer, Cham, 2024

    work page 2024

  37. [37]

    L. Pacheco. Epistemic possibility in Artemov and Protopopescu’s intuitionistic epistemic logic.New frontiers of proof and computation, 2293:66–71, 2024. URLhttp://hdl.handle.net/2433/295429

    work page 2024

  38. [38]

    Palmigiano

    A. Palmigiano. Dualities for some intuitionistic modal logics. InDick de Jongh’s Liber Amicorum. ILLC Publications, Amsterdam, 2004

    work page 2004

  39. [39]

    A. M. Pitts. Evaluation logic. In G. Birtwistle, editor,Proceedings of the IVth Higher Order Workshop 1990, Berlin, Heidelberg, 1991. Springer

    work page 1990

  40. [40]

    H. A. Priestley. Representation of distributive lattices by means of ordered Stone spaces.Bulletin of the London Mathematical Society, 2(2):186–190, 1970. doi:10.1112/blms/2.2.186

    work page doi:10.1112/blms/2.2.186 1970

  41. [41]

    P. H. Rodenburg.Intuitionistic Correspondence Theory. PhD thesis, University of Amsterdam, 1986

    work page 1986

  42. [42]

    Sahlqvist

    H. Sahlqvist. Completeness and correspondence in the first and second order semantics for modal logic. In S. Kanger, editor,Proceedings of the Third Scandinavian Logic Symposium, volume 82, pages 110–143, 1975. doi:10.1016/S0049- 237X(08)70728-6

    work page doi:10.1016/s0049- 1975

  43. [43]

    Sambin and V

    G. Sambin and V. Vaccaro. A new proof of Sahlqvist’s theorem on modal definability and completeness.The Journal of Symbolic Logic, 54(3):992–999, 1989. doi:10.2307/2274758

    work page doi:10.2307/2274758 1989

  44. [44]

    Sano and M

    K. Sano and M. Ma. Goldblatt-Thomason-style theorems for graded modal language. InProc. AiML 2010, pages 330–349, England, 2010. College Publications

    work page 2010

  45. [45]

    Sano and J

    K. Sano and J. Virtema. Characterising modal definability of team-based logics via the universal modality.Annals of Pure and Applied Logic, 170:1100–1127, 2019. doi:10.1016/j.apal.2019.04.009. 27

    work page doi:10.1016/j.apal.2019.04.009 2019

  46. [46]

    M. H. Stone. The theory of representations for Boolean algebras.Transactions of the American Mathematical Society, 40:37–111, 1936. doi:10.2307/1989664

    work page doi:10.2307/1989664 1936

  47. [47]

    B. Teheux. Modal definability based on Lukasiewicz validity relations.Studia Logica, 104:343–363, 2016

    work page 2016

  48. [48]

    D’Agostini, A Multidimensional unfolding method based on Bayes’ theorem, Nucl

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

    work page doi:10.1016/0168- 1990

  49. [49]

    Wijesekera and A

    D. Wijesekera and A. Nerode. Tableaux for constructive concurrent dynamic logic.Annals of Pure and Applied Logic, 135(1-3):1–72, 2005. doi:10.1016/j.apal.2004.12.001

    work page doi:10.1016/j.apal.2004.12.001 2005

  50. [50]

    Williamson

    T. Williamson. On intuitionistic modal epistemic logic.Journal of Philosophy, 21(1):63–89, 1992

    work page 1992

  51. [51]

    Wolter and M

    F. Wolter and M. Zakharyaschev. The relation between intuitionistic and classical modal logics.Algebra and Logic, 36(2):73–92, 1997. doi:10.1007/BF02672476

    work page doi:10.1007/bf02672476 1997

  52. [52]

    Wolter and M

    F. Wolter and M. Zakharyaschev. Intuitionistic modal logic. In A. Cantini, E. Casari, and P. Minari, editors,Logic and Foundations of Mathematics: Selected Contributed Papers of the Tenth International Congress of Logic, Methodology and Philosophy of Science, pages 227–238, Dordrecht, 1999. Springer Netherlands. 28

    work page 1999