{"id":"fe178e1d-815c-4eb2-aa67-468a13ff891c","arxiv_id":"2506.01421","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"The satisfiability problem for the ∃□ + □∃ bundled fragment of first-order modal logic is decidable over increasing domain models.","lead":"Proof of decidability: for the bundled fragment of first-order modal logic allowing exact sequences ∃□ and □∃, the satisfiability problem is decidable over increasing domain models. It answers an open question from Liu et al. (2023) and collapses their trichotomy to a dichotomy.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Claim 14's ∀-case misuses Lemma 13: the limit-model truth lemma is not proven, so the completeness direction of Theorem 9 is unsupported as written.","rationale":"The paper's central claim is decidability of ∃□+□∃, which Theorem 9 reduces to the existence of an open tableau. The soundness direction is supported by Lemma 10 with a bounded skolem-forest and appears plausible. The real risk is completeness: Section 6 constructs a sequence of tableaux and a limit model M, and Claim 14 is the lemma connecting membership in tableau labels to truth in M. The written proof of the ∀-case of Claim 14 is not a valid derivation: it uses Lemma 13, a failure-detection lemma, to conclude truth, and it applies the induction hypothesis to substitution instances outside the stated range of the induction. This is exactly the kind of hidden assumption that can invalidate the decidability proof if it cannot be repaired. The reader's weakest_assumption identifies the same step, and I agree with that assessment. The concern is not that the theorem is false—the illustrative example for φ1 is suggestive—but that the limiting argument is incomplete. Conditional acceptance pending a rigorous truth lemma is appropriate. Note also that Corollary 15's 'direct' 2NExpTime algorithm is terse: bounded label size does not by itself bound the number of tableau nodes, so a decision procedure would additionally need a proof that a finite open tableau exists whenever an infinite one does.","tokens_in":26169,"tokens_out":19586,"duration_ms":214953,"concrete_test":"Re-prove Claim 14's ∀-case by induction over the closure of SF(θ) under substitutions of variables from the evolving domains. For each z ∈ δ(w) with ψ[y/z] first added at stage j, show that the repair sequence of Lemma 12 eventually makes M, w, ι |= ψ[y/z] true; do not cite Lemma 13. As an analytical test case, instantiate this on φ1 from §3: run the repair sequence and check that in the limit model at world u, the nested ∀ formula ψ1 holds for every leaf d_i, including the non-existential conjuncts ψ4(d_i) and ψ7(d_i). If some leaf receives only an existential witness but not the full atom, the truth lemma is false.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Claim 14 is the core of the completeness direction of Theorem 9: it asserts that every formula appearing in a node of T_i is true in the limit model M under the identity assignment. In the ∀-case, the proof (Appendix D) picks z ∈ δ(w), finds a node where ψ[y/z] ∈ Γ'', and concludes 'by Lemma 13, M, w, ι |= ψ[y/z]'. This is a misapplication: Lemma 13 asserts only that if a formula is false then some nested-∀ leaf violation exists; it does not yield truth. Furthermore, ψ[y/z] is a substitution instance, not a member of SF+(θ), so the structural induction of Claim 14 cannot be applied to it. A correct proof must induct over the set of all formulas that appear in the tableau, including substitution instances, and use the repair mechanism of Lemma 12 to establish truth for each instance. Without this, the limit model is not shown to satisfy the root formula, so an open tableau is not witnessed to be satisfiable.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper studies the bundled fragment of first-order modal logic that allows the quantifier-modal combinations ∃□ and □∃, over increasing-domain models. It claims to settle the case left open by Liu et al. 2023 by proving that this fragment is decidable even though it fails the finite model property. The proof introduces a tableau calculus in which each world-node carries a finite 'skolem forest' that records witnesses for nested ∀∃ alternations. Soundness is argued via rule-by-rule preservation of satisfiability together with a bounded-size skolem-forest lemma. Completeness is argued by an infinite repair sequence of tableaux: whenever a leaf witness is missing, the tableau is extended, and the root formula is claimed to hold in the limit model. The main result is Theorem 9, with Corollary 15 giving a 2NExpTime upper bound.","tokens_in":26344,"tokens_out":5685,"duration_ms":66529,"significance":"If the proof can be completed, this is a substantial result: it collapses the trichotomy of Liu et al. to a dichotomy over increasing-domain models, and it gives a rare example of a decidable first-order modal fragment without the finite model property. The skolem-forest construction is a novel pseudo-finite witness mechanism that may be reusable in other settings. The paper does not fit parameters or assume the target result; it relies on the published trichotomy and non-finite-model theorems of Liu et al. The main weakness is that the completeness direction, which is the core of the paper, is not established as written: the limit-model truth lemma is missing, and the proof of Claim 14 contains a load-bearing inference that is not licensed by the stated Lemma 13.","major_comments":[{"comment":"The inference 'by Lemma 13, M, w, ι |= ψ[y/z]' is not justified. Lemma 13 only says that if a formula is false at a node in the associated fixed-tableau model, then there is a descendant leaf violation involving some nested ∀ subformula; it does not prove truth. Moreover, ψ[y/z] is a substitution instance that need not belong to SF+(θ), so the structural induction on φ ∈ SF+(θ) cannot be applied to it. The completeness direction of Theorem 9 therefore requires a separate limit-model truth lemma, for example an induction over all formulas and substitution instances that appear during the repair sequence, using the fact that every leaf violation is eventually repaired by Lemma 12. This lemma is not supplied.","section":"Appendix D, proof of Claim 14, final paragraph (∀yψ case)"},{"comment":"Lemma 13 is stated and proved for the model M_T associated with a fixed open tableau T, using reverse induction on the height of T. Claim 14, however, is applied to the limit model M = ⋃_i M_i, whose domains and valuations are infinite unions over the repair sequence. No analogue of Lemma 13 is proved for this limit model, and the height induction does not directly transfer to the limit. The proof must either establish the needed failure-characterization property for the limit model or show that the finite-stage lemmas can be used uniformly to derive a contradiction from M, w, ι ⊭ ψ[y/z].","section":"Section 6, Lemma 13 vs. Claim 14"},{"comment":"Lemma 12 is load-bearing for the existence of the infinite repair sequence, but its proof is only a sketch. In particular, the final step that adds intermediate nodes to ensure all rule applications are valid is described as 'a tedious but routine induction' without presenting the induction invariant. Since the completeness argument depends on the repaired tableau remaining an open tableau and on the newly added formulas being propagated correctly, this step should be written out in full or at least with a precise invariant.","section":"Appendix C, Lemma 12"}],"minor_comments":[{"comment":"The meaning of the symbol ⋆ is given only in the caption; it would be clearer to include a legend inside the figure, since the table is central to the claimed trichotomy-to-dichotomy result.","section":"Figure 1"},{"comment":"There are several typos and grammatical slips, including 'fragemtns' in Section 1, 'intution' in Appendix A, 'antecedant' in Section 5, 'is also is also' in Appendix D, and the garbled sentence in the proof sketch of Lemma 10 beginning 'For every z ∈ S, we make z as a root and assign them the atom that corresponds to what σ(z) prove in that in the same model Γ′ will also be valid.'","section":"Throughout"},{"comment":"The step from bounded labels at each tableau node to a 2NExpTime decision procedure is too quick. The authors should state a bound on the depth and branching of the saturated tableau that they intend to search, or formulate an explicit nondeterministic algorithm that guesses a finite tableau of doubly exponential size.","section":"Corollary 15"}],"recommendation":"major_revision","confidential_remarks":"The central idea is credible and the result, if correct, is a good fit for the journal. The main issue is the completeness proof: the limit-model truth lemma is not actually proved, and the appeal to Lemma 13 in Claim 14 is a genuine logical gap rather than a mere presentation problem. I would encourage a revision that supplies a full proof of Claim 14 with an appropriate induction over substitution instances and the repair sequence, and that clarifies the status of Lemma 13 in the limit model."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Dear colleague,\n\nHeadline: this paper answers a real open question from Liu et al. 2023 by proving that the ∃□ + □∃ bundled fragment is decidable over increasing domains, and the Skolem-forest construction is a genuinely new way to obtain finite combinatorial witnesses in a logic without the finite model property. If the proof goes through, it collapses the trichotomy to a dichotomy and gives a 2NExpTime upper bound. I have not seen this technique before, and the running example in Appendix A actually helped me see the intended repair sequence.\n\nThe soft spot is real. The completeness direction of Theorem 9 rests on Claim 14, the limit-model truth lemma, and the written proof does not work. In the ∀-case, the authors pick z ∈ δ(w), find ψ[y/z] in the tableau, and conclude truth by citing Lemma 13. But Lemma 13 only says: if a formula is false, then there is a nested-∀ leaf violation. That is a necessary condition for falsity, not a sufficient condition for truth, so it cannot be inverted to prove M,w |= ψ[y/z]. Worse, ψ[y/z] is a substitution instance, which is not in SF+(θ), so the structural induction in Claim 14 cannot be applied to it. The same issue appears in the ♢-case for nested ∀ formulas, where the induction hypothesis is applied to α[z/x]. The likely fix is a generalized truth lemma for all formulas occurring in the tableau, including ground substitution instances, using the repair sequence (Lemma 12) to show every leaf violation eventually gets a witness. That is a nontrivial rewrite of Appendix D, not a one-line patch.\n\nSmaller issues: Lemma 10's proof sketch has a garbled sentence, the (∃ −rule) explanation about y ∈ S is easy to misread, and there are typos. None of these affect the math if the completeness proof is fixed. Soundness and the bounded-size skolem-forest lemma look plausible. Citation practice is fine; relying on the published trichotomy is appropriate, and the shared author with Liu et al. does not create a circularity problem.\n\nBottom line: the main idea is novel and the result is probably true, but the paper as submitted does not prove the completeness direction. It deserves a serious referee, but the referee should ask for a corrected limit-model argument. I would not cite it as a proven decidability result until that gap is closed; I would cite it as a promising technique.\n\nRecommendation: send to peer review, flag the completeness gap as the main issue.","headline":"A genuinely new decidability result with a promising Skolem-forest technique, but the completeness proof's limit-model truth lemma has a gap that needs repair before the result is established.","tokens_in":26862,"tokens_out":4357,"would_cite":false,"duration_ms":44825,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","03B25","68Q17"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that the bundled fragment of first-order modal logic combining existential-with-necessity (∃□) and necessity-with-universal (□∃) formulas is decidable over increasing domain models, even though it lacks the finite model…","keywords":["bundled fragments","first-order modal logic","decidability","finite model property","increasing domain models","tableau procedures","skolem-forest","satisfiability"],"falsifier":"Run the tableau-repair procedure on the formula φ1 from Section 3, which is satisfiable and forces an infinite domain. If the sequence of finite tableaux ever reaches a stage where some leaf variable's required witness is never supplied in the union model, or where a leaf is labelled by both a literal and its negation, then the completeness direction is refuted; the paper predicts instead that every leaf violation is repaired by copying subtrees, so checking that every existential requirement at every leaf is met in the limit model settles the matter.","tokens_in":1966,"feed_emoji":"🧩","tokens_out":1770,"duration_ms":96368,"temperature":0.7,"pith_summary":"The paper answers an open question in the classification of bundled fragments of first-order modal logic. It proves that the fragment combining ∃□ and □∃ is decidable over increasing domain models, despite the fact that it does not have the finite model property: some satisfiable formulas force an infinite domain even when only finitely many worlds are needed. The decidability proof is a tableau procedure whose finite nodes carry a finite labelled forest, called a skolem-forest, that records which local-domain elements need witnesses for nested ∀∃ formulas and when the witness chain can be cut off because an atom repeats. When the model extracted from a tableau does not yet satisfy the root formula, the forest is extended by copying a repeated subtree with fresh variables, producing an infinite sequence of finite tableaux whose union yields a genuine infinite model. This gives a 2NExpTime upper bound and turns the trichotomy of Liu et al. (2023) into a dichotomy for increasing domain models.","feed_headline":"Logic fragment stays decidable without finite model property","feed_subtitle":"A tableau that builds infinite models by copying witness trees proves decidability.","key_machinery":"The load-bearing object is the skolem-forest, a finite labelled forest associated with a tableau node that contains a unique nested ∀ formula of the form ∀xψ. Each tree in the forest has as its root a variable from the current local domain, and each edge from a variable z to a child records that a fresh variable was created as a witness for some existential subformula ∃yβ that must hold for z; vertices are labelled by atoms of ψ. The forest's cutoff condition stops a tree when the atom at a leaf repeats among two earlier ancestors on the same root-to-leaf path, guaranteeing finiteness while still encoding enough information to generate witnesses in the limit. Its role is to make every node of the tableau finite and to provide the template for the repair operation that copies a repeated subtree onto a leaf, producing the infinite sequence of tableaux whose union gives the intended model.","core_discovery":"The central claim is that the satisfiability problem for the ∃□ + □∃ bundled fragment of first-order modal logic over increasing domain models is decidable. The proof works by constructing, for every satisfiable formula, an open tableau whose nodes hold sets of subformulas together with a finite skolem-forest: each tree in the forest is rooted at a local-domain element, and edges record that a child variable was introduced as a witness for an existential subformula sitting inside a nested universal formula. The forest stops growing along a root-to-leaf path once the same atom occurs twice among earlier ancestors, which keeps the tableau finite despite the fact that the models themselves may be infinite. If the model read off from a finite open tableau fails to satisfy the root formula, the tableau is repaired by copying the subtree rooted at the repeated atom onto the deficient leaf, with all copied variables renamed fresh; iterating this repair gives a sequence of finite open tableaux whose union is a model satisfying the formula. Theorem 9 states that an open tableau exists if and only if the root formula is satisfiable, and Corollary 15 concludes that satisfiability is decidable with a nondeterministic double-exponential-time upper bound.","pith_inferences":["If the completeness gap in the written proof of Claim 14 is closed by a direct induction on instantiated subformulas, the repair-and-limit construction would provide a general template for proving completeness of tableau systems whose models are deliberately infinite generated by non-terminating repair sequences.","The same forest-with-repetition scheme may transfer to the □∃ fragment over constant domain models, which the paper leaves open; a natural test would be to run the repair construction on the constant-domain analogue of the paper's infinite-model formula and see whether the atom-repetition cutoff survives the change in domain discipline.","The result suggests that any lower bound for this fragment must come from formula-size encoding rather than from forced infinitude itself; the authors' suspicion that the problem is 2ExpSpace-complete, if confirmed, would show that the infinite-domain feature costs at most a single exponential blow-up over the stated upper bound."],"forward_implications":["The bundled-fragment trichotomy of Liu et al. (2023) collapses to a dichotomy for increasing domain models, since the only combination whose decidability status was open is now known to be decidable.","Every satisfiable ∃□+□∃ formula admits an open tableau, and Lemma 10 bounds the skolem-forest at each node by n · m^{2^{O(m)}} in terms of domain size n and formula length m, yielding the 2NExpTime decision procedure of Corollary 15.","Decidability is not obtained through the finite model property; instead the construction deliberately builds infinite models as unions of an infinite sequence of finite tableau repairs, so the fragment becomes a rare example of a decidable first-order-logic extension that still forces infinite domains.","The paper proposes the skolem-forest technique as a reusable tool for other first-order modal fragments that lack the finite model property, citing the two-variable term modal logic with equality as a candidate where the same idea might apply."],"supporting_citations":[{"why":"Established the bundled-fragment trichotomy, proved that the ∃□+□∃ fragment lacks the finite model property, and left the decidability of this fragment open, which the paper resolves.","marker":"(Liu et al. 2023)"},{"why":"Earlier version of the generalized bundled-fragment classification, also cited for the open decidability question and for the naming conventions of the fragments.","marker":"(Liu et al. 2022)"},{"why":"Proved decidability of the related bundled fragment ∃□+∀□ over increasing domain models, providing the prior decidability result that the tableau-based approach builds upon.","marker":"(Padmanabha, Ramanujam, and Wang 2018)"},{"why":"Introduced bundled fragments with the ∃□ restriction as a decidable fragment of first-order modal logic, originating the framework used here.","marker":"(Wang 2017)"},{"why":"Established that first-order modal logic is undecidable even with only unary predicates, providing the backdrop of undecidability that makes new decidable fragments significant.","marker":"(Kripke 1962)"},{"why":"Introduced the monodic fragment, the earlier major approach to decidable fragments of first-order modal logic, against which the bundled-fragment line is compared.","marker":"(Wolter and Zakharyaschev 2001)"}],"fun_headline_variants":["Bundled FOML fragment decidable despite no finite model property","Decidable bundled modal logic without finite model property","Tableau proof: bundled fragment decidable even without FMP","Collapsing trichotomy: bundled FOML fragment decidable","No finite model property, but this logic fragment is decidable"],"cache_read_input_tokens":29056,"weakest_assumption_plain":"The load-bearing assumption is that the limit model obtained by taking the union of the infinite sequence of repaired tableau models satisfies the original root formula; the manuscript's proof of that fact cites a lemma that only detects failures inside finite stages, so a full induction on instantiated subformulas showing that no failure survives in the limit is required.","fun_headline_variants_meta":{"raw":{"variants":["Bundled FOML fragment decidable despite no finite model property","Decidable bundled modal logic without finite model property","Tableau proof: bundled fragment decidable even without FMP","Collapsing trichotomy: bundled FOML fragment decidable","No finite model property, but this logic fragment is decidable"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000622,"raw_usage":{"total_tokens":2891,"prompt_tokens":962,"completion_tokens":1929,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":578,"completion_tokens_details":{"reasoning_tokens":1844}},"tokens_in":578,"tokens_out":1929,"duration_ms":14379,"temperature":1.0,"reasoning_tokens":1844,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-07T11:44:58.952178+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Run the tableau-repair procedure on the formula φ1 from Section 3, which is satisfiable and forces an infinite domain. If the sequence of finite tableaux ever reaches a stage where some leaf variable's required witness is never supplied in the union model, or where a leaf is labelled by both a literal and its negation, then the completeness direction is refuted; the paper predicts instead that every leaf violation is repaired by copying subtrees, so checking that every existential requirement at every leaf is met in the limit model settles the matter.","supporting_citations":[{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Established the bundled-fragment trichotomy, proved that the ∃□+□∃ fragment lacks the finite model property, and left the decidability of this fragment open, which the paper resolves."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Earlier version of the generalized bundled-fragment classification, also cited for the open decidability question and for the naming conventions of the fragments."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Proved decidability of the related bundled fragment ∃□+∀□ over increasing domain models, providing the prior decidability result that the tableau-based approach builds upon."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduced bundled fragments with the ∃□ restriction as a decidable fragment of first-order modal logic, originating the framework used here."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Established that first-order modal logic is undecidable even with only unary predicates, providing the backdrop of undecidability that makes new decidable fragments significant."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Introduced the monodic fragment, the earlier major approach to decidable fragments of first-order modal logic, against which the bundled-fragment line is compared."}],"review_version":1}