{"id":"43ffc925-1c22-44ce-9335-3af399be5d91","arxiv_id":"2509.08165","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"One-variable, guarded, and two-variable-with-counting monodic fragments of first-order modal logics K_n and S5_n are decidable despite non-rigid constants, definite descriptions, and counting.","lead":"Monodic first-order modal logics with non-rigid constants, definite descriptions, and counting remain decidable for several key fragments, with matching complexity bounds. The paper systematically maps the decision problem, giving 2ExpTime-complete guarded and coNExpTime-complete counting fragments over K_n and S5_n, plus a decidable but Ackermann-hard transitive closure case.","discovery_kind":"extension","skeptic_critique":{"model":"deepseek-v4-flash","headline":"C2 upper bound rests on unproved Lemma 26; the sketched star-type-to-type encoding must be made explicit before Theorem 27 is accepted.","rationale":"The reader's weakest_assumption names Lemma 26 first, and that is exactly where I locate the most load-bearing concern. The paper's headline positive results are the decidability and tight complexity bounds for monodic C2_21MLc and GF=21MLc. Of these, Theorem 27 (coNExpTime for C2_21MLc) relies on a lemma whose proof is explicitly deferred: Lemma 26 asserts an exact linear-Diophantine characterization of C2 quasistates with strong size and complexity bounds, but the provided sketch leaves the crucial encoding unspecified. Lemma 43 is also sketched, but it affects only the transfer to temporal logics and K*_n/Kf*_n, not the core K_n/S5_n decidability claims; hence it is secondary. I do not claim Lemma 26 is false; the gap is that the submitted proof does not contain a verifiable construction. The two bullet points in the sketch address known difficulties (small models and star-types), but they do not demonstrate that the resulting systems remain linear, remain of the stated size, have coefficients of the stated magnitude, or that membership in C is decidable in exponential time. If the lemma fails in any of these respects, the coNExpTime upper bound in Theorem 27 is unsupported. A complete re-derivation from [8] would settle this. Because the reader already marked the paper CONDITIONAL and identified the same step, my stress test does not change the verdict: the paper should be accepted only conditionally on a full proof of Lemma 26 (or a modified upper-bound argument).","tokens_in":48583,"tokens_out":18459,"duration_ms":238524,"concrete_test":"Independently reconstruct Lemma 26 from [8, Sections 8.4–8.5]: for a small C2 sentence (e.g., Example 7's φ0 with a counting quantifier), write down the full systems E for every possible quasistate candidate, including the small-model cases, and verify (a) that every solution corresponds to a realisable quasistate and vice versa; (b) that each E is a linear extended-Diophantine system with |E| exponential and finite coefficients ≤2^{2^{p(|φ|)}}; (c) that membership E∈C is decidable in time 2^{O(|φ|)}. If the star-type elimination forces coefficients beyond double exponential, or if the small-model cases require non-linear constraints, Theorem 27's coNExpTime upper bound is unsupported and the paper should be revised to a weaker claim or a full proof.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The central coNExpTime upper bound for C2_21MLc (Theorem 27) depends entirely on Lemma 26, which asserts that quasistate realizability for C2 sentences is captured by an exponential-size set of systems of linear extended-Diophantine equations over the type-count variables, with double-exponential coefficients and exponential-time membership. The proof is a two-item sketch deferring to [8] and saying the construction is 'rather cumbersome, but straightforward in principle.' That is not enough for a load-bearing lemma. The two observations do not by themselves establish the encoding: (1) handling small models by adding 'new sets of equations' is only asserted, not defined; (2) expressing 'our' one-types as disjunctions of [8]'s star-types and then eliminating the star-type variables from the [8] systems is exactly the step where coefficients could grow beyond double exponential or the constraints could become non-linear. Since Theorem 27 also feeds the expanding-domain claim via Theorem 6(c), a failure of Lemma 26 would remove the coNExpTime upper bound for both. This is a correctness risk, not a disagreement with consensus: the result may be true, but the submitted proof does not contain it.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies monodic fragments of first-order modal logic with non-rigid constants, definite descriptions, equality, and counting (NRDC features) over K_n and S5_n, and over transitive-closure/temporal frames. It develops a quantitative quasimodel technique in which quasistates are multisets of types, runs are multisets, and a prototype function supplies local saturation witnesses. The main positive results are: Q1=MLc validity is coNExpTime-complete on K_n and S5_n with constant domains (Theorem 19), GF=21MLc validity is 2ExpTime-complete on K_n and S5_n in both constant and expanding domains (Theorem 21), C2_21MLc validity is coNExpTime-complete (Theorem 27), expanding-domain Q1=MLc validity on K_n is PSpace-complete (Theorem 41), and Kf*_n validity for C2_21MLc and GF=21MLc with expanding domains is decidable (Theorem 37), with a transfer to finite linear temporal frames (Theorem 44). The paper also records several undecidability results, including global consequence over K_n/S5_n and Ackermann-hardness for transitive-closure variants.","tokens_in":48874,"tokens_out":13461,"duration_ms":164804,"significance":"If the technical results are correct, this is a substantial contribution: it shows that NRDC features, which cause undecidability in several one-variable first-order modal/temporal logics, can still be handled in the monodic fragments over K_n and S5_n by means of counting-aware weak quasimodels. The quasimodel equivalence proofs (Lemmas 9, 13, 14, 22) and the guarded-fragment upper-bound argument are detailed and largely self-contained modulo standard GF results. The paper is also honest in marking its sketches. However, the central coNExpTime upper bound for C2_21MLc depends on Lemma 26, whose proof is only a two-item sketch, and the temporal-to-modal transfer depends on Lemma 43, whose proof is a one-sentence citation. Until those are supplied, the corresponding theorems should be treated as conditional.","major_comments":[{"comment":"This lemma is load-bearing for the coNExpTime upper bound in Theorem 27 and, through Theorem 6(c), for the expanding-domain version as well. The proof is explicitly a sketch with two observations. Observation (2) is exactly the delicate step: expressing 'our' types as disjunctions of [8]'s star-types and then eliminating the star-type variables from the [8] systems. No argument is given that the elimination preserves linearity of the resulting constraints, keeps coefficients within double exponential size, preserves the exponential bound on the number of equation sets, or yields exponential-time membership in C. Observation (1) only asserts that small models are handled by 'new sets of equations' without defining them. Since Theorem 27's upper bound depends entirely on this lemma, the proof is incomplete. Please provide a full construction, or state and prove a precise theorem from [8] t","section":"Section 7.3, Lemma 26"},{"comment":"The proof of this lemma is a single sentence: it is 'not trivial' but can be done by adapting [4, Theorem 6.24]. The lemma is used to transfer the LTL lower bounds to K*_n and Kf*_n and to derive Theorem 44 from Theorem 37. The cited theorem concerns product modal logics and does not, as cited, cover definite descriptions, partial designators, or counting. The reduction must be stated in enough detail to verify that it preserves validity in both directions for the NRDC languages in question. As written, the transfer is not verifiable and the lower-bound/decidability conclusions that rely on it are unsupported.","section":"Section 9, Lemma 43"}],"minor_comments":[{"comment":"The proof begins with a quasimodel Q=(F,q,R,p), but quasimodels were defined in Section 4 as triples (F,q,R) without a prototype function. This is harmless—one can choose p(w,t) arbitrarily for each (w,t) with q(w,t)>0—but the definition should be aligned or the choice of p should be stated.","section":"Section 5, Lemma 13"},{"comment":"The proof says 'so O' is a quasimodel' after checking realisability of the q'(w). The object constructed is a weak quasimodel; to obtain a genuine quasimodel one must invoke Lemma 14. Please add the missing sentence (and correct 'O'' to 'Q'').","section":"Section 7.2, Theorem 21 proof"},{"comment":"Typo: 'countring' should be 'counting' in the sentence introducing the need for a more subtle combination with the upper bound proofs.","section":"Section 7.3"},{"comment":"In condition (a) of the Small Non-Root construction, 'ρ(w)∈q(w)' appears to be a typo for 'ρ(w)∈q'(w)'; otherwise the condition would keep all prototypes and defeat the purpose of the reduction.","section":"Section 8.2, Lemma 39 / Small Non-Root rule"}],"recommendation":"major_revision","confidential_remarks":"The stress-test concern about Lemma 26 lands: the coNExpTime upper bound for C2_21MLc is not proved in the manuscript as submitted. Lemma 43 is a second, smaller but still load-bearing gap. The rest of the quasimodel development is careful and detailed, and the GF and Q1 results appear solid. I would not reject on the basis of disagreement with consensus; the issues are missing proofs that can in principle be supplied. If the authors provide full proofs of Lemmas 26 and 43, the paper would likely be acceptable."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"I've read arXiv:2509.08165. The headline result is real: decidability of the monodic guarded fragment and the two-variable counting fragment with non-rigid constants, definite descriptions, and equality over K_n and S5_n is a genuine advance. The paper's weak quasimodel machinery, with multisets of types and runs, is a substantive adaptation of standard quasimodel techniques, not just relabeling. The complexity bounds (2ExpTime for guarded, coNExpTime for C2) are tight and surprising, and the PSpace result for the one-variable expanding-domain case is a nice contrast to the coNExpTime constant-domain case. The paper is clearly written, and the central soundness/completeness proofs for weak quasimodels (Lemmas 13, 14, 22) are detailed and convincing. The systematic mapping of what remains decidable when NRDC features are added is valuable for the community.\n\nThe soft spots are real but localized. Theorem 4 (undecidability of global consequence) is sketched and leans on Hampson–Kurucz, but that result is independently published and the reduction is plausible. Lemma 43, transferring temporal lower bounds to K*_n and Kf*_n, is again a sketch citing [4, Theorem 6.24]. If the proof really is a straightforward adaptation, fine, but the details aren't here. The biggest concern is Lemma 26, which is the load-bearing step for the coNExpTime upper bound for C2. The sketch says the construction is 'rather cumbersome, but straightforward in principle' and defers to Pratt-Hartmann's book. The stress-test concern about the star-type-to-type encoding is legitimate: coefficients could grow beyond double exponential, or the constraints could become non-linear. The result may well be true, but the submitted proof doesn't fully contain that argument. This is a correctness risk, not a matter of taste.\n\nWho gets value from this paper? People working on decidable modal fragments, temporal description logics, and the boundary between decidable and undecidable first-order modal logics. It deserves a serious referee, but I'd expect the referee to ask for Lemma 26 to be expanded into a complete proof, and Lemma 43 to be given more detail. If those are fixed, this would be a strong paper. As it stands, it is a solid, careful paper with one important unfinished spot.\n\nReading group: yes. I'd cite it for the guarded fragment results even before the C2 lemma is repaired, since those proofs are self-contained. Would I accept for peer review? Yes, absolutely — the central results are important and the weak quasimodel framework is worth refereeing even if Lemma 26 needs work.","headline":"Strong and genuinely new decidability results for monodic modal fragments with non-rigid constants and counting, but the C2 upper bound rests on a sketched Lemma 26 that needs to be filled in before the paper is complete.","tokens_in":49358,"tokens_out":974,"would_cite":true,"duration_ms":14376,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","03B25","03B70","68Q15"],"pacs":[],"model":"deepseek-v4-flash","headline":"The paper proves that monodic guarded and two-variable counting fragments of first-order modal logic remain decidable when non-rigid constants, definite descriptions, and counting are added, with tight complexity bounds.","keywords":["first-order modal logic","monodic fragment","non-rigid constants","definite descriptions","counting quantifiers","guarded fragment","two-variable fragment","quasimodels"],"falsifier":"Apply the Lemma 26 procedure to a small C2 sentence whose types are known; if any solution to the produced Diophantine system fails to correspond to a realisable quasistate, the coNExpTime upper-bound proof for the counting fragment collapses.","tokens_in":48504,"feed_emoji":"","tokens_out":7350,"duration_ms":82668,"temperature":0.7,"pith_summary":"The paper sets out to show that three features usually blamed for undecidability in first-order modal logic—non-rigid constants, definite descriptions, and counting quantifiers—can be added to monodic fragments without destroying decidability. It establishes that validity in the monodic guarded fragment and in the monodic two-variable fragment with counting is decidable over K_n and S5_n frames, with tight 2ExpTime and coNExpTime bounds respectively. The proof works by replacing models with finite \"weak quasimodels\": multisets of types and runs that record how many individuals realise each type at each world. A sympathetic reader cares because these features are exactly what make modal logic useful for representing names, descriptions, and numerical information in philosophy and knowledge representation.","feed_headline":"Non-rigid names don't break monodic modal logic","feed_subtitle":"Validity in guarded and two-variable counting fragments stays decidable, with tight K_n/S5_n complexity bounds.","key_machinery":"Weak quasimodel: a finite tree-shaped Kripke frame in which each world is labelled by a multiset of types (Boolean-saturated sets of one-variable subformulas), and domain elements are represented as multisets of weak runs—functions from upward-closed sets of worlds to types that satisfy coherence but not necessarily saturation. A prototype function p(w,t) marks one saturated run of each type at each world; this lets the construction keep finitely many worlds by allowing the remaining runs to be unsaturated, then \"repairs\" them by duplicating witness worlds (Lemmas 13-14). For the counting fragment, weak runs are further replaced by local links between quasistates satisfying linear equations,","core_discovery":"The central claim is that satisfiability of Q=21MLc sentences in the monodic guarded fragment GF=21MLc over K_n and S5_n is 2ExpTime-complete (Theorem 21), and in the monodic two-variable counting fragment C2_21MLc is coNExpTime-complete (Theorem 27), with the same bounds for constant and expanding domains. The technical content is an equivalence: a sentence is satisfiable iff there exists a weak quasimodel of at most exponential size (Lemmas 13 and 14), where quasistates are multisets of types and domain elements are multisets of runs, with a prototype function witnessing saturation. Counting and equality are handled by the multiplicities, and the existing decision procedures for the underl","pith_inferences":["The weak-quasimodel method should transfer to other decidable first-order fragments with a monotone finite-model property, such as guarded negation or fluted fragments; testing that would require proving an analogue of Lemma 20 for those fragments.","The PSpace versus coNExpTime gap between expanding and constant domains in the one-variable fragment suggests that expanding-domain semantics can systematically lower complexity elsewhere; the paper does not investigate whether GF or C2 exhibit a similar gap.","Because Lemma 26 is the only non-elementary-looking step in the C2 upper bound, a simpler or fully constructive proof of that lemma would likely give a more modular route to complexity results for other counting extensions.","The decidability boundary for transitive-closure modal logic appears to be the absence of infinite ascending chains; extending the Kf*_n decidability argument to arbitrary K*_n frames would require a well-quasi-ordering argument that the paper's Dickson's Lemma technique does not provide."],"forward_implications":["Validity in the monodic guarded fragment with non-rigid constants, equality, and closed definite descriptions is 2ExpTime-complete on K_n and S5_n, matching the non-modal guarded fragment's complexity.","Validity in the monodic two-variable fragment with counting is coNExpTime-complete on K_n and S5_n, again matching its non-modal base.","Over finite acyclic frames with expanding domains, the transitive-closure extension of these monodic fragments is decidable; the one-variable case is Ackermann-hard.","The one-variable fragment is coNExpTime-complete for constant domains but PSpace-complete for expanding domains on K_n.","These decidability results transfer to monodic temporal logics over finite strict linear orders with expanding domains for the guarded and counting fragments."],"supporting_citations":[{"why":"Supplies the baseline decidability results for monodic fragments without NRDC features, which the paper extends.","marker":"[9]"},{"why":"Provides the normal forms and linear extended-Diophantine characterisation of C2 quasistates used in Lemma 26.","marker":"[8]"},{"why":"Gives the guarded-fragment complexity and functionality-undecidability results that justify the 2ExpTime lower bound and the restriction to closed definite descriptions.","marker":"[39]"},{"why":"Supplies the guarded-fragment finite model property used to bound quasistate sizes in Lemma 20.","marker":"[40]"},{"why":"Underpins the standard quasimodel machinery, tree-unfolding, and product-logic reductions used in Lemmas 11, 14, and 43.","marker":"[4]"},{"why":"Provides the undecidability result for the product modal logic with the elsewhere quantifier transferred in Theorem 4.","marker":"[14]"},{"why":"Gives the undecidability and Ackermann-hardness results for one-variable first-order temporal logic with counting used for the lower bounds in Theorem 42 and hence for K*_n and Kf*_n.","marker":"[13]"},{"why":"Supplies the product modal logic complexity result used for the coNExpTime lower bound in the one-variable fragment Theorem 19.","marker":"[44]"}],"fun_headline_variants":["Monodic modal logic remains decidable with non-rigid constants","Non-rigid constants: monodic modal fragments still decidable","Guarded and two-variable counting modal logic decidable","Tight decidability bounds for monodic modal logic","Monodic modal logic tolerates non-rigid constants"],"cache_read_input_tokens":2688,"weakest_assumption_plain":"The upper bounds for the counting and temporal results rest on two delegated technical steps—an exponential-time linear-equation encoding of counting-fragment quasistates and a reduction from temporal to transitive-closure modal logics—that the paper sketches rather than proves in full.","fun_headline_variants_meta":{"raw":{"variants":["Monodic modal logic remains decidable with non-rigid constants","Non-rigid constants: monodic modal fragments still decidable","Guarded and two-variable counting modal logic decidable","Tight decidability bounds for monodic modal logic","Monodic modal logic tolerates non-rigid constants"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.00043,"raw_usage":{"total_tokens":2018,"prompt_tokens":713,"completion_tokens":1305,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":457,"completion_tokens_details":{"reasoning_tokens":1221}},"tokens_in":457,"tokens_out":1305,"duration_ms":12882,"temperature":1.0,"reasoning_tokens":1221,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-04T21:07:56.228614+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Apply the Lemma 26 procedure to a small C2 sentence whose types are known; if any solution to the produced Diophantine system fails to correspond to a realisable quasistate, the coNExpTime upper-bound proof for the counting fragment collapses.","supporting_citations":[],"review_version":1}