{"id":"565bb2b0-cc40-44fb-b257-3afe0f0601a7","arxiv_id":"1908.03509","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The satisfiability problems of K4×S5, S4×S5, and subset-space logic are proven EXPSPACE-hard, giving EXPSPACE-completeness with the companion upper bounds.","lead":"By encoding runs of exponentially space-bounded machines into modal formulas, this paper proves that checking satisfiability in three related modal logics is EXPSPACE-hard. With matching upper bounds from its companion paper, this settles the complexity of these logics as EXPSPACE-complete.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Omitted proof of Lemma 5.6 (L ∈ ALOGTIME) is the main load-bearing gap: the logspace reductions in §5–6 from SSL to S4×S5 and from S4×S5 to K4×S5 depend on it, and the paper explicitly omits the proof.","rationale":"The paper's main contribution is EXPSPACE-hardness under logspace reduction. The most substantial part, the ATM-to-SSL reduction of Section 4, appears structurally sound: the shared-variable mechanism is used consistently, the counter construction works, and the partial-tree extension lemma correctly derives an accepting tree from any model. The logspace computability of fSSL itself also seems plausible from the regular structure described in §4.2. The same cannot be said for the reductions in Sections 5 and 6, whose logspace complexity depends on an omitted membership test for the language L of bimodal formulas. Lemma 5.6 is explicitly not proved, and Corollary 5.7 is used to decide whether the input is a formula before applying the translations. Without it, the reduction functions in §5.3 and §6 are not shown to be logspace, so the EXPSPACE-hardness of S4×S5 and K4×S5 under logspace reduction is not fully established. This is a fixable gap rather than a fatal flaw, so the reader's CONDITIONAL verdict is appropriate; no adjustment is needed.","tokens_in":57902,"tokens_out":40366,"duration_ms":440805,"concrete_test":"Supply a complete proof of Lemma 5.6: give an explicit ALOGTIME/DLOGTIME-uniform NC1 membership algorithm for the grammar (variables x(binary), unary prefixes ¬/K/□, binary ∧ with parentheses), or a logspace reduction to Buss's ALOGTIME Boolean-formula language. The proof must handle nested unary prefixes and variable-token maximization; then re-derive Corollary 5.7. If no such proof can be given, the logspace status of the §5–6 reductions fails.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central result is logspace EXPSPACE-hardness. The direct ATM-to-SSL construction of §4.2 is logspace without Lemma 5.6. But the chains SSL → S4×S5 (§5) and S4×S5 → K4×S5 (§6) need the reduction to be defined on all strings, not just well-formed formulas. In §5.3 and §6 the algorithms first decide membership in the language L of bimodal formulas and output a fixed non-formula on malformed input; they also parse ϕ, find occurrences of subformulas xbin(j), and count which K/□-subformulas end at each position while printing T(ϕ). These steps are justified solely by Corollary 5.7, which rests entirely on Lemma 5.6: the paper states 'we omit the proof of Lemma 5.6'. If L is not decidable in logspace (or ALOGTIME), the SSL→S4×S5 and S4×S5→K4×S5 reductions are not established as logspace, so Theorem 1.1 would only give polynomial-time EXPSPACE-hardness for S4×S5 and K4×S5. The lemma is standard and likely provable, but it is a real, explicitly acknowledged gap in a load-bearing premise.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper establishes EXPSPACE-hardness under logspace reductions for the satisfiability problems of three bimodal logics: K4×S5, S4×S5, and the logic SSL of subset spaces (Theorem 1.1). The proof proceeds in three stages. Section 4 gives the main construction: a logspace reduction from AEXPTIME (= EXPSPACE) to SSL satisfiability. The reduction encodes accepting trees of exponential-time alternating Turing machines by cross axiom models, using shared variables and binary counters (Section 3) to store time, tape head position, state, and read/written symbols, and to propagate the content of revisited cells via the cross property. Both directions are verified: from accepting trees one constructs a model (Section 4.3), and from any model one extracts an accepting tree by an extension argument on partial trees (Section 4.4, Lemma 4.2). Sections 5 and 6 then give logspace translations SSL→S4×S5 and S4×S5→K4×S5; their correctness is proved as Propositions 5.3 and 6.3, and their logspace computability relies on Corollary 5.7 (the language of bimodal formulas is in LOGSPACE), which rests on Lemma 5.6 (L ∈ ALOGTIME). An appendix provides an alternative direct logspace reduction from AEXPTIME to S4×S5. With the ESPACE upper bounds of the companion paper [8], the paper concludes EXPSPACE-completeness (Theorem 1.2).","tokens_in":58132,"tokens_out":33318,"duration_ms":314734,"significance":"The result is substantial and, if the logspace gap discussed below is closed, settles a conjecture of Marx reported in Kurucz et al. [13, Problem 6.67], improving the known NEXPTIME lower bounds for K4×S5 and S4×S5 and the PSPACE lower bound for SSL to the presumably optimal EXPSPACE bound matching the upper bounds of [8]. The paper's strengths include the original 'shared variable' mechanism for SSL, the explicit binary counters in cross axiom models, and the unusually detailed bidirectional verification of the ATM simulation: the model construction (Section 4.3) and the partial-tree extraction (Section 4.4) are spelled out with full case analyses, and the appendix's direct S4×S5 reduction provides an independent route to the same lower bound for S4×S5. The logspace computability of the Section 4 reduction is argued directly with counter bounds; the only load-bearing missing piece is the proof of Lemma 5.6.","major_comments":[{"comment":"The logspace claim for two of the three reductions rests on an unproved lemma. Lemma 5.6 states that the language L of bimodal formulas is in ALOGTIME, and Corollary 5.7 concludes L ∈ LOGSPACE. The proof of Lemma 5.6 is explicitly omitted ('we omit the proof of Lemma 5.6'). This lemma is load-bearing in two places: the SSL→S4×S5 reduction (§5.3) first decides membership of the input string in L and then parses ϕ to locate subformulas, match parentheses, and count modal subformulas; the S4×S5→K4×S5 reduction (proof of Theorem 6.1) likewise invokes Corollary 5.7 before any parsing. If L were not decidable in logspace, Theorems 5.1 and 6.1 would only yield polynomial-time reductions, and Theorem 1.1 would be reduced to a polynomial-time hardness statement for S4×S5 and K4×S5. The lemma is standard (a Buss-style ALOGTIME argument should suffice), but as written the paper contains a load-bearing gap. Please supply a proof of Lemma 5.6 or replace Corollary 5.7 with a direct logspace parsing algorithm that also justifies the subformula-extraction steps.","section":"§5.3, Lemma 5.6 and Corollary 5.7; also used in §6"}],"minor_comments":[{"comment":"Definition 5.2 chooses main as the alphabetically first propositional variable not occurring in sf(ϕ), while the algorithm in §5.3 searches for the numerically smallest index j with xbin(j)∉sf(ϕ); these two orders need not coincide, and although any fresh variable works semantically, the definition and the implementation should be reconciled.","section":"§5.2/§5.3 (Definition 5.2)"},{"comment":"In Proposition A.2(2), the statement 'p0|= counter SSL,n' should read 'p0|= counterS4×S5,n', since the proposition concerns S4×S5 models.","section":"Appendix A.1 (Proposition A.2)"},{"comment":"The paper uses both 'ESPACE' and 'EXPSPACE' for exponential space; please either standardize the notation or state explicitly on first use that the two names denote the same class.","section":"Abstract and §1"},{"comment":"In the backward direction of Proposition 6.3, the verification that the constructed model M is an S4×S5-commutator model and the K-case of the induction are both delegated to 'similar' arguments without stating the key observation that every L'-successor and every ♦'-successor of a point in W lies in W; stating this observation explicitly would make the proof easier to check.","section":"§6 (Proposition 6.3)"},{"comment":"Several definitions used throughout the paper (cross axiom models, the induced cloud relation, the exact syntax of bimodal formulas) are deferred to the companion paper [8]; given that Theorem 1.2 is conditional on [8], it would improve self-containedness to restate the most load-bearing definitions.","section":"§2"}],"recommendation":"major_revision","confidential_remarks":"The completeness claim of Theorem 1.2 depends on the companion paper [8], which is listed as submitted for publication; please make the companion paper available to the referees. Apart from the omitted proof of Lemma 5.6, I found no other load-bearing gap; the proof of Proposition 6.3 is terse in places but sound. The paper is long and somewhat repetitious, but the appendix's direct reduction is a genuine asset. I would support acceptance after the authors supply the missing lemma."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the short version: this is a real result. It improves NEXPTIME-hardness for K4×S5 and S4×S5 and PSPACE-hardness for SSL to EXPSPACE-hardness under logspace reduction, and with the companion upper-bound paper this makes all three EXPSPACE-complete and confirms Marx's conjecture. The core Section 4 construction—reducing exponential-time ATMs to SSL satisfiability using shared variables to handle persistence—is worked out in genuinely careful detail, with both directions of the correctness proof. The binary counter implementation is a nice piece of technical work, and the appendix giving a direct S4×S5 reduction is a useful addition.\n\nThe main proof idea is sound as far as I can tell. The shared-variable trick is the right way around the persistence problem in SSL, and the tree-to-model and model-to-tree arguments line up. The reductions in Sections 5 and 6 are short and credible, and the correctness proof for the SSL-to-S4×S5 translation is complete.\n\nSoft spots:\n\n1. Lemma 5.6, that the language of bimodal formulas is in ALOGTIME, is invoked for the logspace computability of the §5 and §6 reductions, and its proof is omitted. This is the one load-bearing unproved premise. The lemma is standard and almost certainly true—Buss's ALOGTIME result for Boolean formulas should adapt—but as written the reductions are conditional on it. A referee should ask for either a proof or a precise citation.\n\n2. The completeness theorem depends on the companion paper [8] for the ESPACE upper bound and for some definitions. That's a normal division of labor, not a flaw, but it does mean the full EXPSPACE-completeness claim can't be independently checked from this manuscript alone.\n\n3. Minor: the §5.3 algorithm description, while convincing, is a bit hand-wavy in places (e.g., counting closing brackets with binary counters). I think it's correct, but it would benefit from a cleaner presentation.\n\nThe citation pattern is appropriate: Marx, Kurucz et al., Lange/Lutz, and Buss are all relevant, and the self-citation to [8] is doing real work rather than padding.\n\nBottom line: this deserves a serious referee. I'd send it out. The omitted lemma should be supplied or properly cited before publication, but I don't think it threatens the result.","headline":"Genuinely new EXPSPACE lower bounds for three modal logics, with a careful ATM simulation; the only real gap is an omitted standard lemma that the logspace reductions depend on.","tokens_in":58731,"tokens_out":1848,"would_cite":true,"duration_ms":20534,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","68Q17","03D15"],"pacs":[],"model":"deepseek-v4-flash","headline":"The logics K4×S5, S4×S5, and SSL are EXPSPACE-hard under logspace reduction.","keywords":["EXPSPACE-completeness","bimodal product logics","subset space logic","satisfiability problem","alternating Turing machines","logspace reduction","K4×S5","S4×S5"],"falsifier":"Test the omitted lemma directly: for families of bimodal formulas with deeply nested $\\mathsf{K}$ and $\\Box$ prefixes, try to decide well-formedness using only logarithmic working space; any concrete family that provably exceeds logarithmic space would falsify the lemma and break the logspace strength of all three reductions.","tokens_in":57655,"feed_emoji":"🧮","tokens_out":13844,"duration_ms":139381,"temperature":0.7,"pith_summary":"The paper proves that the satisfiability problems of the product logics K4×S5 and S4×S5 and of the subset-space logic SSL are EXPSPACE-hard under logspace reduction. Together with the matching upper bound proved in the companion paper, this makes all three satisfiability problems EXPSPACE-complete and resolves the previously open complexity question for the two product logics. The proof reduces any exponential-time alternating Turing machine computation to the satisfiability of an SSL formula by encoding accepting computation trees as equivalence classes, then transfers the lower bound by logspace translations from SSL to S4×S5 and from S4×S5 to K4×S5. Since these logics are used for reasoning about knowledge and about subset spaces, the result gives a precise worst-case space bound for their satisfiability algorithms.","feed_headline":"Satisfiability in three modal logics is EXPSPACE-complete","feed_subtitle":"Logspace reductions from alternating Turing machines settle the complexity of K4×S5, S4×S5, and subset spaces.","key_machinery":"The load-bearing device is the shared variable: in SSL it is the formula $\\alpha_i := \\mathsf{L}(A_i \\land \\Box_L B)$, and in S4×S5 it is the simpler $\\alpha_i := \\mathsf{L}\\,A_i$. A shared variable is constant along $\\mathsf{L}$-equivalence classes (the clouds) but can change along the vertical $\\lozenge$-direction, while ordinary propositional variables have the opposite persistence; this lets the encoding copy and update bit vectors for time, tape-head position, state, and written symbol. These vectors feed binary-counter formulas that force a staircase of points $p_i \\xrightarrow{\\mathsf{L}} p'_i \\xrightarrow{\\lozenge} p_{i+1}$, so any model of the reduction contains an accepting tree of the alternating Turing machine realized as clouds. The later translations between logics work by adding a fresh variable $\\mathit{main}$ whose false points act as universal successors, and by forcing reflexivity instances for the modal subformulas involved.","core_discovery":"The central claim is Theorem 1.1: the satisfiability problems of K4×S5, S4×S5, and SSL are each EXPSPACE-hard under logspace reduction. Starting from EXPSPACE = AEXPTIME, the paper fixes an alternating Turing machine M running in time $2^{p(n)}$ and builds, for input w, a bimodal formula $f_{SSL}(w)$ that is satisfiable in a cross-axiom model exactly when M has an accepting tree on w. In such a model, $\\mathsf{L}$-equivalence classes (clouds) stand for computation-tree nodes; shared variables carry time, head position, state, and read and written symbols; and the cross property lets a later cloud retrieve the symbol written at an earlier visit to the same tape cell. The formula has polynomial size and is generated in logarithmic space, and both directions of the satisfiability equivalence are verified. The paper then gives a logspace translation of SSL formulas into S4×S5 formulas and of S4×S5 formulas into K4×S5 formulas, so the lower bound transfers. With the companion upper bound, Theorem 1.2 follows: all three logics are EXPSPACE-complete under logspace reduction.","pith_inferences":["Editorial inference: the shared-variable construction is a reusable encoding trick for any bimodal logic with an equivalence relation in one dimension, a preorder in the other, and a cross property: such logics can simulate alternating time-bounded computation directly.","Editorial inference: the delicate subformula is the one that recovers the symbol written at the previous visit to a tape cell; streamlining that bookkeeping could adapt the reduction to prove lower bounds for fragments with fewer propositional variables or restricted modal depth.","Editorial inference: because Lemma 5.6 is stated without proof, any reuse of these reductions should first supply the omitted ALOGTIME membership argument; a reader who wants only the satisfiability equivalence rather than the logspace strength can bypass that lemma."],"forward_implications":["The three satisfiability problems are EXPSPACE-complete, not merely NEXPTIME-hard or PSPACE-hard as previously known.","Any solver for SSL, S4×S5, or K4×S5 must face instances that require exponentially much space on infinitely many inputs, unless EXPSPACE collapses to a smaller class.","The logspace chain SSL ≤ S4×S5 ≤ K4×S5 transfers lower bounds uniformly, so future lower-bound proofs for any one of these logics immediately apply to the others.","The direct reduction in the appendix shows that exponential-time alternating Turing machine computations can be encoded straight into S4×S5, without passing through subset-space semantics.","The previously open conjecture reported in the introduction—that K4×S5 and S4×S5 are EXPSPACE-complete—is confirmed by the paper together with its companion."],"supporting_citations":[{"why":"companion paper supplying the matching upper bound that turns hardness into EXPSPACE-completeness.","marker":"[8]"},{"why":"establishes alternation and the equivalence AEXPTIME = EXPSPACE used to choose the machine model.","marker":"[2]"},{"why":"introduces alternating Turing machines and the one-tape simulation used in the paper's ATM variant.","marker":"[3]"},{"why":"records the previous NEXPTIME lower bound and N2EXPTIME upper bound and states the EXPSPACE-completeness conjecture this paper confirms.","marker":"[13]"},{"why":"demonstrates the method of proving sharp lower bounds via alternating Turing machines that Section 4 follows.","marker":"[14]"},{"why":"supplies the cross-axiom model framework and doubly exponential model property for SSL used in the satisfiability arguments.","marker":"[5]"},{"why":"previous PSPACE-hardness for SSL, the lower bound this paper improves.","marker":"[11,12]"},{"why":"provides the ALOGTIME decision procedure for Boolean formulas that Lemma 5.6 adapts to bimodal formulas.","marker":"[1]"},{"why":"records ALOGTIME ⊆ LOGSPACE, used to convert Lemma 5.6 into logspace decidability of bimodal formula syntax.","marker":"[4]"}],"fun_headline_variants":["Three modal logics now EXPSPACE-complete","Logspace reductions prove EXPSPACE-hardness","K4×S5, S4×S5, SSL: all EXPSPACE-complete","Hardness proof for product and subset-space logics"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The load-bearing premise is that checking whether a string is a well-formed bimodal formula can be done in logarithmic space; the paper states this as Lemma 5.6, explicitly says the proof is omitted, and every logspace claim in the reduction chain depends on that fact.","fun_headline_variants_meta":{"raw":{"variants":["Three modal logics now EXPSPACE-complete","Logspace reductions prove EXPSPACE-hardness","K4×S5, S4×S5, SSL: all EXPSPACE-complete","Hardness proof for product and subset-space logics"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000275,"raw_usage":{"total_tokens":1626,"prompt_tokens":913,"completion_tokens":713,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":529,"completion_tokens_details":{"reasoning_tokens":638}},"tokens_in":529,"tokens_out":713,"duration_ms":6865,"temperature":1.0,"reasoning_tokens":638,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-14T14:11:10.451719+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Test the omitted lemma directly: for families of bimodal formulas with deeply nested $\\mathsf{K}$ and $\\Box$ prefixes, try to decide well-formedness using only logarithmic working space; any concrete family that provably exceeds logarithmic space would falsify the lemma and break the logspace strength of all three reductions.","supporting_citations":[{"cited_title":"Hertling and G","cited_arxiv_id":null,"evidence_quote":"companion paper supplying the matching upper bound that turns hardness into EXPSPACE-completeness."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"establishes alternation and the equivalence AEXPTIME = EXPSPACE used to choose the machine model."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"introduces alternating Turing machines and the one-tape simulation used in the paper's ATM variant."},{"cited_title":"Kurucz, F","cited_arxiv_id":null,"evidence_quote":"records the previous NEXPTIME lower bound and N2EXPTIME upper bound and states the EXPSPACE-completeness conjecture this paper confirms."},{"cited_title":"Lange and C","cited_arxiv_id":null,"evidence_quote":"demonstrates the method of proving sharp lower bounds via alternating Turing machines that Section 4 follows."},{"cited_title":"Dabrowski, L","cited_arxiv_id":null,"evidence_quote":"supplies the cross-axiom model framework and doubly exponential model property for SSL used in the satisfiability arguments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"provides the ALOGTIME decision procedure for Boolean formulas that Lemma 5.6 adapts to bimodal formulas."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"records ALOGTIME ⊆ LOGSPACE, used to convert Lemma 5.6 into logspace decidability of bimodal formula syntax."}],"review_version":1}