Pith. sign in

REVIEW 1 major objections 6 minor 31 references

The Complexity of the Constructive Master Modality

T0 review · 1 major / 6 minor · reviewed 2026-08-02 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read The constructive master-modality logics CK* and WK* are EXPTIME-complete, with exponential-size finite models, and their diamond-free fragment settles an open conjecture; the same translations put CS4 and WS4 validity in EXPTIME.

desk verdict Solid, careful complexity paper for constructive master modalities; the internal proofs check out under spot-checking, but the ExpTime lower bound rests on an unproven folklore claim about the single-program PDL fragment K* that the authors should pin down before I'd call the headline result fully settled. read the letter →

arxiv 2603.05131 v2 pith:E54Y36X6 submitted 2026-03-05 cs.LO math.LO

Sofía Santiago-Fernández , David Fernández-Duque , Joost J. Joosten This is my paper · ORCID
classification cs.LOmath.LO MSC 03B4503B7068Q1568Q17
keywords constructivemodallogicmastermodalitypropositionaldynamicPDLEXPTIME-completenessfinitemodelpropertyGödel–TarskitranslationCS4
topics P versus NP
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

This paper introduces two constructive modal logics, CK* and WK*, that add 'master' modalities □* and ♢* to the basic constructive modal logic CK and its infallible variant WK. The central claim is that validity for both logics is EXPTIME-complete — exactly the complexity of classical propositional dynamic logic — and that every satisfiable formula has a finite model of at most exponential size. The proof works by constructing exact translations in both directions: a translation from WK* into PDL yields the upper bound, and a translation of the classical single-program fragment K* into the diamond-free fragment CK*_box yields the lower bound. A stated consequence is that the diamond-free fragment is EXPTIME-complete, resolving an open conjecture, and that the constructive S4 logics CS4 and WS4 become decidable in EXPTIME.

What carries the argument

The load-bearing mechanism is a family of four exact translations that preserve validity and satisfiability in both directions. The central transfer is τ: WK* → PDL, which replaces each constructive modality by a PDL program — □* ↦ [(i*;m)*], ♢* ↦ [i*]⟨m*⟩ — so that WK*-validity is literally a fragment of PDL-validity. The reverse transfer ι: K* → CK*_box relativizes to an 'excluded middle for all subformulas' hypothesis, which forces the classical reading of negation inside the intuitionistic logic. Around these, ω maps CK* into WK* by encoding ⊥ as a boxed conjunction, and κ embeds CS4 and WS4 as the *-only fragment. Each translation is polynomial (or linear for τ), which is what makes the

What would settle it

Locate a full proof that validity in K* (PDL with one atomic program and no program operations beyond a and a*) is EXPTIME-hard, or exhibit a PSPACE decision procedure for K*; either would settle the load-bearing assumption that the cited EXPTIME-hardness transfers.

Watch

Extended reading notes

Core claim

On its own terms, the paper establishes that the semantically defined logics CK* and WK* — which interpret □* via the reflexive-transitive closure of the composed relation (≼;R) and ♢* as a constructive 'eventually' — are EXPTIME-complete and have the exponential-size model property. The upper bound follows from a validity-preserving translation τ into classical PDL, where □* becomes [(i*;m)*] and ♢* becomes [i*]⟨m*⟩. The lower bound comes from a converse translation ι that relativizes a classical K*-formula to the hypothesis that every subformula satisfies excluded middle, embedding K* into the diamond-free fragment CK*_box. As the paper notes, this settles the conjecture for the diamond-fr

Load-bearing premise

The lower-bound chain rests on the folklore assertion that the fragment of PDL with a single atomic program and only the programs a and a* is already EXPTIME-hard; if that assertion is unsupported or false, the EXPTIME-completeness results collapse to mere EXPTIME upper bounds.

Editorial extensions

If this is right

  • Validity for CK*, WK*, and the diamond-free fragment CK*_box is EXPTIME-complete, matching the complexity of classical PDL.
  • Every satisfiable formula of these logics has a finite model of size at most exponential in the formula's length.
  • The diamond-free fragment's EXPTIME-completeness settles the previously open conjecture about the intuitionistic master modality.
  • CS4 and WS4 validity are in EXPTIME, improving the earlier upper bound for CS4 from NEXPTIME.
  • CS4 embeds in CK* as the ♢*,□*-fragment, giving a new way to view constructive S4 as part of a PDL-like framework.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • If the folklore lower-bound assertion is given a direct proof, the paper's EXPTIME-completeness conclusion is secure; the most direct test is to locate an explicit proof that the single-atomic-program fragment K* is EXPTIME-hard, since the current citation may not cover that exact fragment.
  • The exactness of the PDL translation suggests that proof-theoretic machinery from PDL — such as tableaux or automata-based decision procedures — could be imported to give deductive calculi for WK*, the paper's explicitly stated open problem.
  • The authors conjecture PSPACE-completeness; a natural next step is to check whether the intuitionistic base alone (already PSPACE-complete) forces the lower bound, which would imply the EXPTIME upper bound is loose.
  • The ω translation that eliminates fallibility by encoding ⊥ as a boxed conjunction is modular and may generalize to other constructive logics, potentially offering a systematic way to pass from fallible to infallible semantics.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

1 major / 6 minor

Summary. The paper introduces the constructive master-modality logics CK* and WK*, with modalities □*, ♢* over arbitrary bi-relational frames, and studies their validity/satisfiability complexity. The main results are: (i) a polynomial translation of CK* into WK* (§3); (ii) a linear Gödel–Tarski-style translation of WK* into classical PDL that yields ExpTime upper bounds and the exponential-size finite model property for CK*, WK*, and the diamond-free fragment CK*_□ (§5); (iii) a lower bound via a translation of the fragment K* of PDL with a single program a and only programs a, a* into CK*_□ (§6), yielding ExpTime-completeness for the three master-modality logics; and (iv) embeddings of CS4 and WS4 into CK* and WK*, yielding ExpTime upper bounds for CS4/WS4 validity (§7). The upper-bound architecture is explicit and, apart from the lower-bound folklore claim discussed below, the proofs are coherent.

Significance. If the lower-bound claim is supported, the paper settles the conjecture of Afshari et al. on the diamond-free fragment and gives a uniform ExpTime-completeness classification for constructive master-modality logics, matching classical PDL. It also improves the known upper bound for CS4/WS4 validity from NExpTime to ExpTime. The paper is well structured: the translations are explicitly defined and their sizes are tracked (linear for τ, polynomial for ω and ι); the upper-bound proofs are high-quality and mostly self-contained. The main weakness is that the ExpTime-hardness of the fragment K*, on which all lower-bound results rest, is asserted as folklore without proof or precise citation.

major comments (1)
  1. [Theorem 4.4(2), used in §6] Theorem 4.4(2) asserts that K*, the PDL fragment with a single atomic program a and only programs a and a*, is ExpTime-hard, citing Fischer–Ladner [3] and Pratt [16]. The cited papers prove ExpTime-hardness for full PDL with composition, union, and tests; no reduction is supplied for the restricted a/a* fragment, and no theorem number or page is given. This claim is load-bearing: Theorem 6.5 reduces K* to CK*_□ via ι, and Theorem 6.6 then lifts hardness to CK* and WK* via inclusion and ω. If K* is only PSPACE-hard, the principal ExpTime-completeness claims are unsupported. The theorem may be true, but the manuscript must provide a self-contained proof or a precise reference that establishes hardness for exactly this fragment.
minor comments (6)
  1. [Appendix A, proof of Proposition 2.7] There is a typo in the definition of W_M': "W_M' := W_M' \ {y∈W_M | M,y⊩⊥}" should be "W_M' := W_M \ {y∈W_M | M,y⊩⊥}".
  2. [Theorem 6.5 proof] The proof refers to "Lemma 2.7" but the correct reference is Proposition 2.7. Also, "M, v" near the end should be "M', v".
  3. [Proposition 7.6] The proof details only the □-case and says the remaining cases are easily verified. The ♢-case is not entirely trivial (it requires a case split on the second index of the CS4 model), so it should be spelled out or at least sketched.
  4. [Definition 4.1] The PDL language is defined without union and without tests, while Theorem 4.4(1) cites the standard full PDL. This is harmless for the upper bound because τ lands in a fragment of full PDL, but the relationship should be stated explicitly to avoid confusion.
  5. [Section 3, Definition 3.1] The remark that p⊥ is "in the language of WK* but not of CK*" is confusing since both logics share the same language L*. It would be clearer to say that p⊥ is a fixed distinguished variable not occurring in the input formula φ.
  6. [Abstract and §5.1] Minor typos: "impossing" should be "imposing"; "master-modaly" should be "master-modality".

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: the main derivations are proven in-paper and the lower bound rests on external PDL folklore, not on the authors' own results.

full rationale

The paper's derivation chain is not circular. The three translations used for the upper bounds are proven by explicit induction in-paper: ω (CK* to WK*, Section 3, Theorem 3.6), τ (WK* to PDL, Section 5, Theorem 5.5), and κ (CS4/WS4 to CK*/WK*, Section 7, Theorem 7.7). None of these translations is defined in terms of the validity problem it is used to decide, and no parameter is fitted to the data being 'predicted'. The lower-bound chain does depend on Theorem 4.4(2), which states that K* is ExpTime-hard and cites Fischer and Ladner and Pratt. This is an external folklore result, not a self-citation, and even if the citation is incomplete or the folklore claim is unverified, that is a correctness risk rather than a circularity: the paper's own embedding ι (Theorem 6.5) is proven by structural induction and does not assume the hardness it is used to transfer. Self-citations ([13], [20], [25], [26]) appear only as contextual remarks or as already-known baselines and are not load-bearing for the ExpTime-completeness or ExpTime-upper-bound claims. Therefore the central claims are not equivalent to their inputs by construction; the score is 0.

Assumptions & free parameters 0 free parameters · 4 assumptions · 0 invented entities

The paper contributes translations, not new axioms or fitted constants. Its load-bearing external premises are the classical complexity results for PDL and the folklore EXPTIME-hardness of the single-program fragment K*, plus the identification of its semantics with the prior literature (needed to claim the conjecture is settled). No free parameters appear; no entities are invented to make the derivation work.

assumptions (4)
  • domain assumption K* (single atomic program, programs a and a*, full Boolean connectives) is EXPTIME-hard
    Theorem 4.4(2) cites [3,16] (Fischer–Ladner, Pratt), whose published results are for full PDL; the hardness of the single-letter star-only fragment is load-bearing for all lower bounds (Theorem 6.6) but is not proved or precisely located.
  • domain assumption PDL is decidable in EXPTIME and has the exponential-size model property
    Theorem 4.4(1), cited to [3,16]; the entire upper-bound chain (Theorems 5.6–5.7) and the transferred exponential model property rest on it.
  • domain assumption The birelational semantics of Definition 2.1 (including falsum seriality, condition 4) matches the frameworks of the cited CK/WK literature and of the IMK logic of [4]
    The 'settling the conjecture' claim and the inheritances from [4], [12], [17] require that CK*_□ as defined here is exactly the logic studied there; the paper asserts this match but never states the conjecture or compares frame conditions in detail.
  • standard math Standard classical PDL semantics and EXPTIME closure properties
    Background for Section 4; classical two-valued semantics for PDL, complementation closure of EXPTIME, and the Fischer–Ladner small-model filtration.

how reviews work

0 comments
Cite this review

Pith. "Pith review of The Complexity of the Constructive Master Modality." pith.science (2026). https://pith.science/paper/E54Y36X6

@misc{pith2026260305131,
  author       = {Pith},
  title        = {Pith review of: The Complexity of the Constructive Master Modality},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/E54Y36X6}},
  note         = {Machine review of arXiv:2603.05131}
}
abstract

We introduce the semantically-defined constructive master-modality logics $\sf CK^*$ and $\sf WK^*$, extending the basic constructive modal logic $\sf CK$ and the Wijesekera-style logic $\sf WK$ obtained by impossing infallibility. Using translations between our logics and fragments of $\sf PDL$, we show that both $\sf CK^*$ and $\sf WK^*$ are EXPTIME-complete and admit an exponential-size finite model property. In particular, for their diamond-free fragment, also studied by Afshari et al. and Celoni, we establish EXPTIME-completeness, thereby settling the conjecture of Afshari et al. As an application, we embed $\sf CS4$ and $\sf WS4$ into the master-modality logics, showing that their validity problems are in EXPTIME.

Figures

Figures reproduced from arXiv: 2603.05131 by the authors.

Figure 1
Figure 1. Overview of the master-modality logics and the embeddings. [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Master modalities. We abuse notation and write ∥φ∥M for φ ∈ L∗ to denote the set of worlds w ∈ WM such that (M, w) ⊩ φ. A formula φ is valid in M if ∥φ∥M = WM, 4 [PITH_FULL_IMAGE:figures/full_fig_p004_2.png] view at source ↗
Figure 3
Figure 3. Confluence in Lemma 7.2. This suggests a translation κ of CS4 into CK∗ , where κ(φ) is the result of replacing every occurrence of □ by □∗ and every occurrence of ♢ by ♢ ∗ . Indeed, since every CS4-model is in particular a CK-model, the exactness of the translation is reduced to the following statement. Proposition 7.3. If M is a CS4-model, w ∈ WM and φ ∈ L, then (M, w) ⊩ φ iff M, w ⊩ κ(φ). Proof. The proof proceed… view at source ↗

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

31 extracted references · 1 linked inside Pith

  1. [3]

    Fischer and Richard E

    Michael J. Fischer and Richard E. Ladner,Propositional dynamic logic of regular programs.Journal of Computer and System Sciences, 18(2):194– 211, 1979

    1979

  2. [16]

    Pratt,A near-optimal method for reasoning about action, In Journal of Computer and System Sciences, 20(2):231–254, 1980

    Vaughan R. Pratt,A near-optimal method for reasoning about action, In Journal of Computer and System Sciences, 20(2):231–254, 1980

    1980

  3. [1]

    Bellin, V

    G. Bellin, V. D. Paiva, and E. Ritter,Extended Curry–Howard correspon- dence for a basic constructive modal logic, InProceedings of the 2nd Work- shop on Methods for Modalities (M4M 2001), Amsterdam, Netherlands, 2001

    2001

  4. [2]

    Duminda Wijesekera,Constructive modal logics I.Annals of Pure and Applied Logic, 50(3):271–301, 1990

    1990

  5. [4]

    Leigh, and Lukas Zenger, Intuitionistic master modality, InAdvances in Modal Logic, pages 19–39

    Bahareh Afshari, Lide Grotenhuis, Graham E. Leigh, and Lukas Zenger, Intuitionistic master modality, InAdvances in Modal Logic, pages 19–39. College Publications, 2024

    2024

  6. [5]

    Schloss Dagstuhl, 2024

    Philippe Balbiani, Han Gao, C ¸ igdem Gencer, and Nicola Olivetti,A natural intuitionistic modal logic: axiomatization and bi-nested calculus, InCom- puter Science Logic (CSL 2024), volume 288 ofLIPIcs, pages 13:1–13:21. Schloss Dagstuhl, 2024. 16

    2024

  7. [6]

    CSLI Publications, 1996

    Carsten Grefe,Fischer Servi’s intuitionistic modal logic has the finite model property, InAdvances in Modal Logic 1, pages 85–98. CSLI Publications, 1996

    1996

  8. [7]

    Alex Simpson,The Proof Theory and Semantics of Intuitionistic Modal Logic, PhD thesis, University of Edinburgh, Edinburgh, UK, 1994

    1994

Show all 31 references
  1. [8]

    Fitch,Intuitionistic modal logic with quantifiers.Portugaliae Mathematica, 7(2):113–118, 1948

    Frederic B. Fitch,Intuitionistic modal logic with quantifiers.Portugaliae Mathematica, 7(2):113–118, 1948

    1948

  2. [9]

    Zakharyaschev,The relation between intuitionistic and classical modal logics.Algebra and Logic, 36(2):73–92, 1997

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

    1997

  3. [10]

    Dag Prawitz,Natural Deduction: A Proof-Theoretical Study, Dover Pub- lications, Mineola, NY, 1965

    1965

  4. [11]

    ACM, 1996

    Rowan Davies and Frank Pfenning,A modal analysis of staged computa- tion, InProceedings of the 23rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL 1996), pages 258–270. ACM, 1996

    1996

  5. [12]

    Sergio Celani,A fragment of intuitionistic dynamic logic.Fundamenta Informaticae, 46:187–197, 2001

    2001

  6. [13]

    Boudou, M

    J. Boudou, M. Di´ eguez, and D. Fern´ andez-Duque,A decidable intuitionistic temporal logic, InComputer Science Logic (CSL 2017), pages 14:1–14:17, 2017

    2017

  7. [14]

    Tiziano Dalmonte,Minimal modal logics, constructive modal logics and their relations.Review of Symbolic Logic, 18(2):463–504, 2025

    2025

  8. [15]

    Frank Wolter,Fusions of modal logics revisited, Technical report, Univer- sit¨ at Leipzig, 1996

    1996

  9. [17]

    Nishimura,Semantical analysis of constructive PDL, InPublications of the Research Institute for Mathematical Sciences, 18:427–438, 1982

    H. Nishimura,Semantical analysis of constructive PDL, InPublications of the Research Institute for Mathematical Sciences, 18:427–438, 1982

    1982

  10. [18]

    Degen and J

    W. Degen and J. M. Werner,Towards intuitionistic dynamic logic, InLogic and Logical Philosophy, 15:305–324, 2006

    2006

  11. [19]

    Springer, 2001

    Natasha Alechina, Michael Mendler, Valeria de Paiva, and Eike Ritter, Categorical and Kripke semantics for constructive S4 modal logic, InCom- puter Science Logic (CSL 2001), volume 2142 ofLecture Notes in Computer Science, pages 292–307. Springer, 2001

    2001

  12. [20]

    IEEE, 2021

    Philippe Balbiani, Mart ´ ın Di´ eguez, and David Fern´ andez-Duque,Some constructive variants of S4 with the finite model property, InLogic in Com- puter Science (LICS 2021), pages 1–13. IEEE, 2021. 17

    2021

  13. [21]

    Joseph Boudou, Mart ´ ın Di´ eguez, and David Fern´ andez-Duque,Complete intuitionistic temporal logics for topological dynamics, InJournal of Sym- bolic Logic, 87(3):995–1022, 2022

    2022

  14. [22]

    David Fern´ andez-Duque,The intuitionistic temporal logic of dynamical systems, InLogical Methods in Computer Science, 14(3), 2018

    2018

  15. [23]

    Michael Mendler and Valeria de Paiva,Constructive CK for contexts, In Context Representation and Reasoning (CRR-2005), CEUR Proceedings, 2005

    2005

  16. [24]

    Oxford University Press, 2001

    Kurt G¨ odel,Eine Interpretation des intuitionistischen Aussagenkalk¨ uls (1933), InKurt G¨ odel Collected Works Volume I. Oxford University Press, 2001

    1933

  17. [25]

    Philippe Balbiani, Joseph Boudou, Mart ´ ın Di´ eguez, and David Fern´ andez- Duque,Intuitionistic linear temporal logics, InACM Transactions on Computational Logic, 21(2):14:1–14:32, 2020

    2020

  18. [26]

    Philippe Balbiani, Mart ´ ın Di´ eguez, David Fern´ andez-Duque, and Brett McLean,Constructive S4 modal logics with the finite birelational frame property.arXiv preprint arXiv:2403.00201, 2024

    2024 arXiv

  19. [27]

    Appendix This appendix gathers the technical and straightforward proofs omitted from the main exposition

    Richard Statman,Intuitionistic propositional logic is polynomial-space complete, InTheoretical Computer Science, 9(1):67–72, 1979. Appendix This appendix gathers the technical and straightforward proofs omitted from the main exposition. A Proof of Proposition 2.7 Proposition 2...

    1979

  20. [28]

    Ifp /∈Var(φ), this holds trivially, since∥⊥∥ CK φ =∥ω P(φ) (⊥)∥=∥p∥ CK φ

    We show that∥⊥∥ CK φ ⊆ ∥p∥CK φ for everyp∈Prop. Ifp /∈Var(φ), this holds trivially, since∥⊥∥ CK φ =∥ω P(φ) (⊥)∥=∥p∥ CK φ . Ifp∈Var(φ), then by reflexivity, anyv∈ ∥⊥∥CK φ =∥□ ∗(V P(φ)∧♢p ⊥)∥also belongs to∥p∥=∥p∥ CK φ

  21. [29]

    Ifp∈Var(φ), thenw∈ ∥p∥ CK φ =∥p∥, and the atomic persistence ofMimpliesv∈ ∥p∥=∥p∥ CK φ

    Letw≼vwithw∈ ∥p∥ CK φ . Ifp∈Var(φ), thenw∈ ∥p∥ CK φ =∥p∥, and the atomic persistence ofMimpliesv∈ ∥p∥=∥p∥ CK φ . Ifp /∈Var(φ), then w∈ ∥p∥CK φ =∥□ ∗(V P(φ)∧♢p ⊥)∥, and the same reasoning as in condition (3) showsv∈ ∥p∥CK φ , whose details are left to the reader

  22. [30]

    By definition,w∈ ∥□ ∗(V P(φ)∧ ♢p⊥)∥implies that for allu, ifw(≼;R ∗)∗u, thenu∈ ∥ V P(φ)∧♢p ⊥∥

    Letw∈ ∥⊥∥CK φ and supposew≼vorwRv. By definition,w∈ ∥□ ∗(V P(φ)∧ ♢p⊥)∥implies that for allu, ifw(≼;R ∗)∗u, thenu∈ ∥ V P(φ)∧♢p ⊥∥. In particular, this holds forv, sov∈ ∥□ ∗(V P(φ)∧♢p ⊥)∥=∥⊥∥ CK φ

  23. [31]

    19 C Detailed proofs of the translation fromWK ∗ toPDL Proposition 5.3.LetMbe aWK-model andφ∈ L ∗

    Finally, ifw∈ ∥⊥∥CK φ =∥□ ∗(V P(φ)∧♢p ⊥)∥, then by reflexivityw∈ ∥♢p⊥∥, so there exists somev∈WwithwRv. 19 C Detailed proofs of the translation fromWK ∗ toPDL Proposition 5.3.LetMbe aWK-model andφ∈ L ∗. Then, (M, w)⊩φiff (MPDL, w)⊩τ(φ). Proof.We proceed by structural induction...

Pith tools

Reviewed August 2, 2026 · model on record in the stance chip above.