{"id":"db49952c-2742-4618-b56b-9c76c25e41ba","arxiv_id":"2603.05131","paper_version":2,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Validity in the constructive master-modality logics CK*, WK*, and their diamond-free fragment is EXPTIME-complete, transferred from classical PDL by exact polynomial embeddings.","lead":"This paper defines two new constructive modal logics with 'master modalities' (always/eventually), CK* and WK*, and proves their validity problems are EXPTIME-complete — as hard as the classical program logic PDL — by exact polynomial translations in both directions. It resolves an open conjecture about the simpler diamond-free fragment and derives a new EXPTIME upper bound for constructive S4 logics.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Folklore EXPTIME-hardness of K* is cited but not proven, and all ExpTime lower bounds depend on it.","rationale":"The reader's weakest assumption is exactly the load-bearing point. My independent spot-checks of the internal translations (ω, τ, ι, κ) and the CS4/WS4 embeddings found no errors; the M^CS4 construction works, and the recursive acceptance encoding makes K* hardness plausible. But the paper's claim rests on an external folklore theorem that is not stated precisely for the exact fragment. Because the entire ExpTime lower bound flows through Theorem 6.5, this is the single place where the central claim could fail. The conditional verdict is therefore appropriate; if a direct K* hardness proof is supplied, the results should stand.","tokens_in":16181,"tokens_out":38831,"duration_ms":414932,"concrete_test":"Provide a self-contained proof of EXPTIME-hardness of K* using only the modalities [a] and [a*] (e.g., encode an alternating polynomial-space Turing machine with a single transition relation and a polynomial binary counter, forcing bounded acyclic paths via [a*]¬overflow), or locate the exact theorem for this fragment in Fischer–Ladner 1979 / Ladner 1977. If no such proof or citation exists, the lower bound in Theorem 6.6 is not established.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Theorem 4.4(2) asserts as folklore that K* — the PDL fragment with only the programs a and a* — is EXPTIME-hard, citing Fischer–Ladner and Pratt. The cited lower-bound results are for full PDL with composition, union, and (in standard treatments) multiple program letters and tests; the text gives no reduction for the restricted a/a* fragment. This matters because the lower-bound chain is a single route: Theorem 6.5 embeds K* into CK*_□ via ι, and Theorem 6.6 lifts hardness to CK* and WK* via inclusion and ω. If K* is merely PSPACE-hard, the paper's principal ExpTime-completeness claim is unsupported. The theorem may well be true — a counter-bounded alternating-TM encoding plausibly works with only [a] and [a*] — but the manuscript does not supply or locate that proof, so the central claim is conditional on an unverified folklore statement.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","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.","tokens_in":16319,"tokens_out":23692,"duration_ms":214671,"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":[{"comment":"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.","section":"Theorem 4.4(2), used in §6"}],"minor_comments":[{"comment":"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⊩⊥}\".","section":"Appendix A, proof of Proposition 2.7"},{"comment":"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\".","section":"Theorem 6.5 proof"},{"comment":"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.","section":"Proposition 7.6"},{"comment":"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.","section":"Definition 4.1"},{"comment":"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 φ.","section":"Section 3, Definition 3.1"},{"comment":"Minor typos: \"impossing\" should be \"imposing\"; \"master-modaly\" should be \"master-modality\".","section":"Abstract and §5.1"}],"recommendation":"major_revision","confidential_remarks":"The upper-bound part of the paper is strong and the embeddings are clean. The single blocking issue is the unverified folklore lower-bound claim in Theorem 4.4(2). If the authors can supply a proof or a precise citation for the ExpTime-hardness of the one-program a/a* fragment, the paper should be publishable. I do not see evidence of circularity or unsupported self-reference elsewhere."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The genuinely new material here is the definition of CK* and WK* with the diamond-star semantics, the polynomial embedding of CK* into WK*, the Gödel–Tarski style translation into PDL, and the excluded-middle-prefix embedding of classical K* into the diamond-free fragment. The payoff is real: EXPTIME-completeness for CK*_□, CK*, and WK*, plus an EXPTIME upper bound for CS4 and WS4, improving the known NEXPTIME bound. The CS4 embedding in Section 7 is the most delicate part, and the construction with duplicated worlds works; I checked the diamond case and the confluence argument, and they hold. The proof of Prop 3.3 also works; the falsum seriality and persistence assumptions are exactly what is needed. I found no internal errors in the spots the reader flagged as risky.\n\nThe soft spot is the lower bound. Theorem 4.4(2) asserts, as folklore, that K* — PDL with a single atomic program a and only programs a and a* — is EXPTIME-hard, citing Fischer–Ladner and Pratt. Their published results are for full PDL with composition and union. The paper gives no reduction and no precise location. Since the entire lower-bound chain runs through Theorem 6.5 embedding K* into CK*_□, the main completeness claim is conditional on an unverified statement. I don't think this is fatal — the result is plausibly true and the authors may have a simple encoding of alternating Turing machines with only [a] and [a*] — but the manuscript should either prove it or give an exact citation. The identification of CK*_□ with the logic of Afshari et al. is also asserted rather than argued; that should be made precise.\n\nThe paper also defers a lot of inductive proofs to the appendix or to the reader. Most are routine, and the appendix covers several, but some are load-bearing (e.g., Prop 5.4's diamond case is only sketched in the main text and the appendix fills it; fine, but the main text says 'details are left to the reader' too often for a paper whose complexity claims rest on exact translations).\n\nWho is this for? Researchers working on constructive modal logic, PDL fragments, and proof complexity. It deserves a serious referee — the methods are interesting and the results are a genuine improvement over the state of the art, conditional on the K* folklore claim. I'd send it to peer review with a request that the authors substantiate Theorem 4.4(2) and expand the deferred proofs. If the lower bound is fixed, this is a clean, citable paper.","headline":"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.","tokens_in":16937,"tokens_out":1056,"would_cite":true,"duration_ms":13224,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","03B70","68Q15","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"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.","keywords":["constructive modal logic","master modality","propositional dynamic logic","PDL","EXPTIME-completeness","finite model property","Gödel–Tarski translation","CS4"],"falsifier":"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.","tokens_in":15982,"feed_emoji":"⏱","tokens_out":6930,"duration_ms":62604,"temperature":0.7,"pith_summary":"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.","feed_headline":"Constructive master-modality logics proven EXPTIME-complete","feed_subtitle":"Exact translations into PDL settle a conjecture and put CS4 validity in EXPTIME.","key_machinery":"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","core_discovery":"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","pith_inferences":["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."],"forward_implications":["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."],"fun_headline_variants":["Conjecture settled: CK* and WK* are EXPTIME-complete","Master-modality logics proven EXPTIME-complete, CS4 embedded","PDL translation yields EXPTIME-completeness for master-modality","CS4 and WS4 validity in EXPTIME via master-modality logics"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"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.","fun_headline_variants_meta":{"raw":{"variants":["Conjecture settled: CK* and WK* are EXPTIME-complete","Master-modality logics proven EXPTIME-complete, CS4 embedded","PDL translation yields EXPTIME-completeness for master-modality","CS4 and WS4 validity in EXPTIME via master-modality logics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.001155,"raw_usage":{"total_tokens":4599,"prompt_tokens":695,"completion_tokens":3904,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":439,"completion_tokens_details":{"reasoning_tokens":3828}},"tokens_in":439,"tokens_out":3904,"duration_ms":27283,"temperature":1.0,"reasoning_tokens":3828,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T18:50:15.335418+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"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.","supporting_citations":[],"review_version":1}