pith. sign in

arxiv: 2606.31884 · v1 · pith:OJGK56DJnew · submitted 2026-06-30 · 💻 cs.LO

Intuitionistic Justification Logic, Semantically

Sonia Marin (University of Birmingham) , Paaras Padhiar (University of Birmingham) , Ian Shillito (University of Birmingham) This is my paper

Pith reviewed 2026-07-01 02:36 UTC · model grok-4.3

classification 💻 cs.LO
keywords intuitionistic justification logicrealisation theoremmodular modelssatisfier termsintuitionistic modal logicsoundness and completenesssemantics
0
0 comments X

The pith

Modular models enable a semantic realisation theorem for intuitionistic justification logic with satisfiers.

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

The paper supplies semantics for an intuitionistic justification logic in which diamonds are replaced by explicit satisfier terms equipped with their own operations. It defines basic modular models that extend standard possible-world semantics for intuitionistic propositional logic, then strengthens them with Kripke-style accessibility to recover compatibility with modal logic. Using the stronger models the authors prove soundness and completeness and, crucially, a realisation theorem that converts theorems of the corresponding intuitionistic modal logic into terms of the justification logic. A reader would care because the result supplies the first semantic route from the modal side to explicit proofs in the intuitionistic setting, where only a syntactic proof existed before.

Core claim

Modular models interpret intuitionistic justification logic with satisfiers so that every theorem of the corresponding intuitionistic modal logic is realized by a term; the models are sound and complete, and the realisation is obtained directly from the semantic construction rather than from a syntactic translation.

What carries the argument

Modular models, which extend possible-world semantics for intuitionistic propositional logic by adding Kripke-style machinery that interprets satisfier terms and their interaction with implication and diamond while preserving modal behaviour.

If this is right

  • Basic modular models give soundness and completeness for the justification logic alone.
  • The stronger modular models additionally recover a realisation theorem to the modal logic.
  • Every theorem of the intuitionistic modal logic therefore possesses an explicit realizing term.
  • The semantic construction supplies an alternative to the existing syntactic realisation proof.

Where Pith is reading between the lines

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

  • The same modular construction might be adapted to produce countermodels that witness non-realizability.
  • Decision procedures for the justification logic could be read off from the finite-model property of the modular frames.
  • The approach opens a route to comparing computational complexity of the justification and modal systems directly through their common semantics.

Load-bearing premise

The modular models correctly encode how satisfier terms combine with intuitionistic implication and diamond while keeping the intended modal behaviour intact.

What would settle it

A concrete counter-example would be a formula valid in the target intuitionistic modal logic whose every candidate realizing term fails to satisfy the modular-model semantics at some world.

Figures

Figures reproduced from arXiv: 2606.31884 by Ian Shillito (University of Birmingham), Paaras Padhiar (University of Birmingham), Sonia Marin (University of Birmingham).

Figure 1
Figure 1. Figure 1: Intuitionistic justification axioms and rule [PITH_FULL_IMAGE:figures/full_fig_p004_1.png] view at source ↗
read the original abstract

Justification logics are explicit versions of modal logic. In the classical setting, this means boxes are refined with explicit proof terms and interact with each other through proof operations. This exercise was extended to intuitionistic modal logic with native diamonds. In this setting, diamonds are refined to satisfier terms and come equipped with additional operations. Justification logic enjoys a connection to its corresponding modal logic through a realisation theorem. In the classical setting, this is achieved through either proof-theoretic or semantic methodology. So far, intuitionistic justification logic with satisfiers has only been presented syntactically with a proof-theoretic realisation theorem. We present two classes of semantics for intuitionistic justification logic with soundness and completeness results: basic modular models, which extend possible world semantics for intuitionistic propositional logic; modular models which contain Kripke-style machinery to promote "backwards compatibility" to modal logic. Using modular models, we present a realisation theorem to establish a connection between intuitionistic justification logic and its corresponding intuitionistic modal logic.

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

2 major / 2 minor

Summary. The paper develops two classes of Kripke-style semantics for intuitionistic justification logic with satisfiers: basic modular models extending IPL possible-world semantics, and modular models incorporating additional machinery for modal compatibility. It asserts soundness and completeness results for both classes and, using the modular models, proves a realisation theorem establishing a semantic connection between the justification logic and the corresponding intuitionistic modal logic.

Significance. If the soundness, completeness, and realisation results hold, the work supplies the first semantic realisation theorem for intuitionistic justification logic with satisfiers, complementing the existing proof-theoretic version and extending the classical justification-logic paradigm to the intuitionistic setting with native diamonds. The modular construction, defined independently of the target modal logic, is a clear strength.

major comments (2)
  1. [Abstract / modular-models section] Abstract and the section on modular models: the central claim that the modular models correctly encode the interaction of satisfier terms with intuitionistic implication and the diamond operations (while preserving intended modal behaviour) is load-bearing for the realisation theorem, yet no verification steps, counter-model constructions, or key lemmas are supplied to confirm this encoding.
  2. [Soundness and completeness section] The section asserting soundness and completeness: these results are stated without proof sketches, outline of the induction, or indication of how the backwards-compatibility conditions are used, which directly affects the reliability of the subsequent realisation theorem.
minor comments (2)
  1. Notation for satisfier terms and their operations could be introduced with an explicit comparison table to the classical justification-logic operations to aid readability.
  2. [Abstract] The abstract would benefit from a one-sentence statement of the main technical device (the modular compatibility relation) that enables the realisation theorem.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful review and for identifying points where the presentation of our semantic results can be strengthened. We address each major comment below and will incorporate the suggested clarifications in the revised manuscript.

read point-by-point responses

  1. Referee: [Abstract / modular-models section] Abstract and the section on modular models: the central claim that the modular models correctly encode the interaction of satisfier terms with intuitionistic implication and the diamond operations (while preserving intended modal behaviour) is load-bearing for the realisation theorem, yet no verification steps, counter-model constructions, or key lemmas are supplied to confirm this encoding.

    Authors: We agree that the manuscript would benefit from explicit verification of the encoding properties. In the revision we will add a dedicated subsection to the modular-models section containing two key lemmas: one establishing that the satisfier-term operations respect the intuitionistic implication clauses under the modular accessibility relation, and another confirming that the diamond-interaction axioms are preserved while maintaining backwards compatibility. We will also include a short discussion of a representative counter-model that would arise if the compatibility conditions were omitted, thereby making the load-bearing claim more transparent for the subsequent realisation theorem. revision: yes

  2. Referee: [Soundness and completeness section] The section asserting soundness and completeness: these results are stated without proof sketches, outline of the induction, or indication of how the backwards-compatibility conditions are used, which directly affects the reliability of the subsequent realisation theorem.

    Authors: The observation is correct; the current text states the theorems without proof outlines. We will expand the soundness-and-completeness section with high-level proof sketches. For soundness we will outline the induction on formula complexity, highlighting the cases that rely on the backwards-compatibility conditions to handle the diamond and satisfier clauses. For completeness we will sketch the canonical-model construction and indicate where the same conditions ensure the truth lemma. These additions will directly support the reliability of the realisation theorem proved from the modular models. revision: yes

Circularity Check

0 steps flagged

No circularity; semantics and realisation theorem defined independently of target modal logic.

full rationale

The paper introduces basic modular models as an extension of IPL possible-world semantics and extended modular models incorporating Kripke-style machinery for modal compatibility. Soundness and completeness are established directly for these models, after which the realisation theorem is derived as a consequence linking IJL satisfiers to IML. No equations, definitions, or self-citations reduce the theorem or models to a fitted parameter, self-referential construction, or prior result by the same authors; the construction remains self-contained against external benchmarks with no load-bearing self-citation chains.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work rests on standard axioms of intuitionistic propositional logic and the definition of satisfier-term operations; no free parameters or new postulated entities are introduced in the abstract.

axioms (1)
  • standard math Intuitionistic propositional logic axioms and rules
    Invoked as the base for extending possible-world semantics (abstract).

pith-pipeline@v0.9.1-grok · 5711 in / 1049 out tokens · 32724 ms · 2026-07-01T02:36:14.997894+00:00 · methodology

discussion (0)

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

Reference graph

Works this paper leans on

39 extracted references · 23 canonical work pages

  1. [1]

    Artemov (1995): Operational modal logic

    Sergei N. Artemov (1995): Operational modal logic . Technical Report MSI 95-29, Cornell University. Available at https://sartemov.ws.gc.cuny.edu/files/2014/01/download-3.pdf

    1995

  2. [2]

    Artemov (2001): Explicit provability and constructive semantics

    Sergei N. Artemov (2001): Explicit provability and constructive semantics. Bulletin of Symbolic Logic 7(1), pp. 1–36, doi:10.2307/2687821

    work page doi:10.2307/2687821 2001

  3. [3]

    Artemov (2002): Unified Semantics for Modality and λ-terms via Proof Polynomials

    Sergei N. Artemov (2002): Unified Semantics for Modality and λ-terms via Proof Polynomials. In Kees Ver- meulen & Ann Copestake, editors: Algebras, Diagrams and Decisions in Language, Logic and Computation - Lecture Notes, Centre for the Study of Language & Information, Stanford University, pp. 89–119

    2002

  4. [4]

    Sergei N. Artemov (2011): Why Do We Need Justification Logic? In Johan van Benthem, Amitabha Gupta & Eric Pacuit, editors: Games, Norms and Reasons, Synthese Library 353, Springer Netherlands, Dordrecht, pp. 23–38, doi:10.1007/978-94-007-0714-6 2

    work page doi:10.1007/978-94-007-0714-6 2011

  5. [5]

    Artemov (2012): The Ontology of Justifications in the Logical Setting

    Sergei N. Artemov (2012): The Ontology of Justifications in the Logical Setting. Studia Logica 100(1-2), pp. 17–30, doi:10.1007/s11225-012-9387-x

    work page doi:10.1007/s11225-012-9387-x 2012

  6. [6]

    Artemov, Melvin Fitting & Thomas Studer (2024): Justification Logic

    Sergei N. Artemov, Melvin Fitting & Thomas Studer (2024): Justification Logic. In Edward N. Zalta, ed- itor: The Stanford Encyclopedia of Philosophy , Metaphysics Research Lab, Stanford University, p. online. Available at https://plato.stanford.edu/archives/fall2024/entries/logic-justification

    2024

  7. [7]

    Artemov & Rosalie Iemhoff (2007): The basic intuitionistic logic of proofs

    Sergei N. Artemov & Rosalie Iemhoff (2007): The basic intuitionistic logic of proofs. Journal of Symbolic Logic 72(2), pp. 439–451, doi:10.2178/jsl/1185803617

    work page doi:10.2178/jsl/1185803617 2007

  8. [8]

    Artemov, E

    Sergei N. Artemov, E. Kazakhov & D. Shapiro (1999): On logic of knowledge with justifications. Technical Report CFIS 99-12, Cornell University

    1999

  9. [9]

    In: Proceedings for Methods for Modalities 2, Amsterdam, Netherlands, p

    Gianluigi Bellin, Valeria de Paiva & Eike Ritter (2001): Extended Curry-Howard Correspondence for a Basic Constructive Modal Logic. In: Proceedings for Methods for Modalities 2, Amsterdam, Netherlands, p. unpaginated

    2001

  10. [10]

    In Hans de Nivelle, editor: Automated Reasoning with Analytic Tableaux and Related Methods , Lecture Notes in Computer Science 9323, Springer, Wroclaw, Poland, pp

    Annemarie Borg & Roman Kuznets (2015): Realization Theorems for Justification Logics: Full Modularity. In Hans de Nivelle, editor: Automated Reasoning with Analytic Tableaux and Related Methods , Lecture Notes in Computer Science 9323, Springer, Wroclaw, Poland, pp. 221–236, doi:10.1007/978-3-319-24312- 2 16

    work page doi:10.1007/978-3-319-24312- 2015

  11. [11]

    In: Language, Logic, and Computation , Lecture Notes in Computer Science 7758, Springer Berlin Heidel- berg, Berlin, Heidelberg, pp

    Samuel Bucheli, Roman Kuznets & Thomas Studer (2011): Decidability for Justification Logics Revisited. In: Language, Logic, and Computation , Lecture Notes in Computer Science 7758, Springer Berlin Heidel- berg, Berlin, Heidelberg, pp. 166–181, doi:10.1007/978-3-642-36976-6 12

    work page doi:10.1007/978-3-642-36976-6 2011

  12. [12]

    Available at https://prooftheory.blog/2025/10/03/ diamond-free-parts-of-intuitionistic-modal-logics/

    Anupam Das, Jim de Groot & Ian Shillito (2025): Diamond-free parts of intu- itionistic modal logics . Available at https://prooftheory.blog/2025/10/03/ diamond-free-parts-of-intuitionistic-modal-logics/ . Post on The Proof Theory Blog, accessed: 13/02/2026

    2025

  13. [13]

    Anupam Das & Sonia Marin (2023): On Intuitionistic Diamonds (and Lack Thereof) . In Revantha Ra- manayake & Josef Urban, editors: Automated Reasoning with Analytic Tableaux and Related Methods, Lec- ture Notes in Computer Science 14278, Springer Nature Switzerland, Prague, Czech Republic, pp. 283–301, doi:10.1007/978-3-031-43513-3 16

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

  14. [14]

    Journal of Logic and Computation 21(4), pp

    Evgenij Dashkov (2011): Arithmetical Completeness of the Intuitionistic Logic of Proofs . Journal of Logic and Computation 21(4), pp. 665–682, doi:10.1093/logcom/exp041

    work page doi:10.1093/logcom/exp041 2011

  15. [15]

    Studia Logica 36(3), pp

    Gis `ele Fischer Servi (1977): On Modal Logic with an Intuitionistic Base. Studia Logica 36(3), pp. 141–149. S. Marin, P. Padhiar & I. Shillito 621

    1977

  16. [16]

    Gis `ele Fischer Servi (1980):Semantics for a class of intuitionistic modal calculi. In Maria Luisa Dalla Chiara, editor: Italian Studies in the Philosophy of Science , Boston Studies in the Philosophy and History of Sci- ence 47, Springer Netherlands, Dordrecht, pp. 59–72, doi:10.1007/978-94-009-8937-5 5

    work page doi:10.1007/978-94-009-8937-5 1980

  17. [17]

    Rendiconti del Seminario Matematico Universit`a e Politecnico di Torino 42(3), pp

    Gis `ele Fischer Servi (1984): Axiomatizations for some intuitionistic modal logics. Rendiconti del Seminario Matematico Universit`a e Politecnico di Torino 42(3), pp. 179–194

    1984

  18. [18]

    Annals of Pure and Applied Logic132(1), pp

    Melvin Fitting (2005): The logic of proofs, semantically. Annals of Pure and Applied Logic132(1), pp. 1–25, doi:10.1016/j.apal.2004.04.009

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

  19. [19]

    In Johan van Ben- them, Amitabha Gupta & Eric Pacuit, editors: Games, Norms and Reasons, Synthese Library 353, Springer, Dordrecht, pp

    Melvin Fitting (2011): The Realization Theorem for S5: A Simple, Constructive Proof . In Johan van Ben- them, Amitabha Gupta & Eric Pacuit, editors: Games, Norms and Reasons, Synthese Library 353, Springer, Dordrecht, pp. 61–76

    2011

  20. [20]

    Annals of Pure and Applied Logic 167(8), pp

    Melvin Fitting (2016): Modal logics, justification logics, and realization. Annals of Pure and Applied Logic 167(8), pp. 615–648, doi:10.1016/j.apal.2016.03.005

    work page doi:10.1016/j.apal.2016.03.005 2016

  21. [21]

    Annals of Pure and Applied Logic 163(9), pp

    Remo Goetschi & Roman Kuznets (2012): Realization for justification logics via nested sequents: Modularity through embedding . Annals of Pure and Applied Logic 163(9), pp. 1271–1298, doi:10.1016/j.apal.2012.02.002

    work page doi:10.1016/j.apal.2012.02.002 2012

  22. [22]

    de Groot, I

    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

  23. [23]

    849–867, doi:10.1007/s11229-011-9905-9

    Raul Hakli & Sara Negri (2012): Does the deduction theorem fail for modal logic? Synthese 187(3), pp. 849–867, doi:10.1007/s11229-011-9905-9

    work page doi:10.1007/s11229-011-9905-9 2012

  24. [24]

    Notre Dame Journal of Formal Logic 60(3), doi:10.1215/00294527-2019-0008

    Brian Hill & Francesca Poggiolesi (2019): An Analytic Calculus for the Intuitionistic Logic of Proofs. Notre Dame Journal of Formal Logic 60(3), doi:10.1215/00294527-2019-0008

    work page doi:10.1215/00294527-2019-0008 2019

  25. [25]

    In Peter G

    Roman Kuznets (2000): On the Complexity of Explicit Modal Logics. In Peter G. Clote & Helmut Schwicht- enberg, editors: Computer Science Logic, Lecture Notes in Computer Science 1862, Springer Berlin Heidel- berg, Fischbachau, Germany, pp. 371–383, doi:10.1007/3-540-44622-2 25

    work page doi:10.1007/3-540-44622-2 2000

  26. [26]

    Journal of Applied Logics — IfCoLog Journal of Logics and their Applications 8(8), pp

    Roman Kuznets, Sonia Marin & Lutz Straßburger (2021): Justification Logic for Constructive Modal Logic. Journal of Applied Logics — IfCoLog Journal of Logics and their Applications 8(8), pp. 2313–2332

    2021

  27. [27]

    In Thomas Bolan- der, Torben Bra¨uner, Silvio Ghilardi & Lawrence Moss, editors: Advances in Modal Logic, 9, College Pub- lications, Copenhagen, Denmark, pp

    Roman Kuznets & Thomas Studer (2012): Justifications, Ontology, and Conservativity. In Thomas Bolan- der, Torben Bra¨uner, Silvio Ghilardi & Lawrence Moss, editors: Advances in Modal Logic, 9, College Pub- lications, Copenhagen, Denmark, pp. 437–458. Available at http://www.aiml.net/volumes/volume9/ Kuznets-Studer.pdf

    2012

  28. [28]

    Studies in Logic 80, College Publications

    Roman Kuznets & Thomas Studer (2019): Logics of Proofs and Justifications. Studies in Logic 80, College Publications

    2019

  29. [29]

    Sonia Marin & Paaras Padhiar (2025): Justification Logic for Intuitionistic Modal Logic . In Gian Luca Pozzato & Tarmo Uustalu, editors: Automated Reasoning with Analytic Tableaux and Related Methods , Lecture Notes in Computer Science 15980, Springer Nature Switzerland, Reykjavik, Iceland, pp. 393–413, doi:10.1007/978-3-032-06085-3 21

    work page doi:10.1007/978-3-032-06085-3 2025

  30. [30]

    IFCoLog Journal of Logic and its Applications 3(5), pp

    Michel Marti & Thomas Studer (2016): Intuitionistic Modal Logic Made Explicit. IFCoLog Journal of Logic and its Applications 3(5), pp. 877–901

    2016

  31. [31]

    In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe & Thomas Studer, edi- tors: Advances in Modal Logic , 12, College Publications, Bern, Switzerland, pp

    Michel Marti & Thomas Studer (2018): The Internalized Disjunction Property for Intuitionistic Justifi- cation Logic . In Guram Bezhanishvili, Giovanna D’Agostino, George Metcalfe & Thomas Studer, edi- tors: Advances in Modal Logic , 12, College Publications, Bern, Switzerland, pp. 511–529. Available at https://www.aiml.net/volumes/volume12/Marti-Studer.pdf

    2018

  32. [32]

    In Sergei Adian & Anil Nerode, editors: Logical Foundations of Computer Science , Lecture Notes in Computer Science 1234, Springer Berlin Heidelberg, Yaroslavl, Russia, pp

    Alexey Mkrtychev (1997): Models for the Logic of Proofs. In Sergei Adian & Anil Nerode, editors: Logical Foundations of Computer Science , Lecture Notes in Computer Science 1234, Springer Berlin Heidelberg, Yaroslavl, Russia, pp. 266–275, doi:10.1007/3-540-63045-7 27. 622 Intuitionistic Justification Logic, Semantically

    work page doi:10.1007/3-540-63045-7 1997

  33. [33]

    Logic Journal of the IGPL31(3), pp

    Nicholas Pischke (2023): On intermediate justification logics. Logic Journal of the IGPL31(3), pp. 534–573, doi:10.1093/jigpal/jzac049

    work page doi:10.1093/jigpal/jzac049 2023

  34. [34]

    In Joseph Y

    Gordon Plotkin & Colin Stirling (1986): A framework for Intuitionistic Modal Logics: Extended Abstract . In Joseph Y . Halpern, editor: Proceedings of the 1986 Conference on Theoretical Aspects of Reasoning about Knowledge, TARK ’86, Morgan Kaufmann Publishers Inc., Monterey, California, United States, pp. 399–406

    1986

  35. [35]

    In Dima Grigoriev, John Harrison & Edward A

    Natalia Rubtsova (2006): Evidence Reconstruction of Epistemic Modal Logic S5. In Dima Grigoriev, John Harrison & Edward A. Hirsch, editors: Computer Science – Theory and Applications , Lecture Notes in Computer Science 3967, Springer Berlin Heidelberg, St. Petersburg, Russia, pp. 313–321, doi:10.1007/11753728 32

    work page doi:10.1007/11753728 2006

  36. [36]

    Simpson (1994): The Proof Theory and Semantics of Intuitionistic Modal Logic

    Alex K. Simpson (1994): The Proof Theory and Semantics of Intuitionistic Modal Logic . Ph.D. thesis, University of Edinburgh. Available at http://hdl.handle.net/1842/407

    1994

  37. [37]

    A. S. Troelstra & H. Schwichtenberg (2000): Basic Proof Theory, 2nd edition. Cambridge Tracts in Theo- retical Computer Science 43, Cambridge University Press, doi:10.1017/CBO9781139168717

    work page doi:10.1017/cbo9781139168717 2000

  38. [38]

    Nachiappan Valliappan (2026): Lax Modal Lambda Calculi. In Stefano Guerrini & Barbara K ¨onig, editors: 34th EACSL Annual Conference on Computer Science Logic (CSL 2026), Leibniz International Proceedings in Informatics (LIPIcs) 363, Schloss Dagstuhl – Leibniz-Zentrum f ¨ur Informatik, Dagstuhl, Germany, pp. 46:1–46:20, doi:10.4230/LIPIcs.CSL.2026.46

    work page doi:10.4230/lipics.csl.2026.46 2026

  39. [39]

    Wijesekera (1990): Constructive Modal Logics I

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

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