{"id":"574822e8-77eb-41a0-97e9-17b8a5f8eeec","arxiv_id":"2603.04512","paper_version":3,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":8.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":0,"one_line_summary":"Fusing one-variable first-order modal logics preserves completeness and decidability without equality, but adding equality and non-rigid constants can make fusions undecidable.","lead":"This paper studies what happens when you combine two simple modal logics that can talk about one object, and whether nice properties like decidability survive the combination. It finds that without equality the good properties transfer, but adding equality and non-rigid constants can break them entirely, even making the fused logic undecidable.","discovery_kind":"first_principles","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Negative theorems target the semantic product logic, not the syntactic fusion defined in §2; the abstract's non-preservation claims are therefore unsupported.","rationale":"The reader's verdict correctly flags the abstract's overclaim: the body proves non-preservation of decidability and recursive axiomatisability, not Kripke completeness. However, I find a more specific and load-bearing issue: the non-preservation results are stated for Log^=d(C1⊗C2), which is the logic of the product frame class, whereas the paper's formal definition of fusion is the smallest syntactic logic containing the components. The proof of Theorem 4.1 works by showing satisfiability of a formula on product frames; this does not, without a completeness transfer theorem, imply anything about derivability in the syntactic fusion. In fact, since Log^=d(C1⊗C2) is Kripke complete by definition, Corollary 4.2 cannot establish failure of Kripke completeness for the syntactic fusion. This affects the negative half of the abstract and the paper's central advertised contrast. I do not dispute the positive equality-free transfer theorems; my concern is that the negative results need either to be reinterpreted as results about semantic product logics or supplemented with a proof that the syntactic fusion coincides with that semantic logic in the counterexamples. The reader's weakest assumption, property (†), is a different—though also legitimate—proof gap in the local decidability argument; I do not take issue with it here. Thus I recommend the same conditional acceptance as the reader, but for a sharper reason than the abstract mismatch alone.","tokens_in":27473,"tokens_out":52166,"duration_ms":416596,"concrete_test":"For L1=Log^=cd D and L2=Log^=cd Dfin from Theorem 4.1, determine whether the syntactic fusion L1⊗L2 equals Log^=cd(D⊗Dfin). Concretely: check whether the proof of Theorem 4.1 ever derives φ_E or ¬φ_E from the axioms of L1 and L2 using MP, Generalization, Necessitation, and Substitution. If it only constructs models on D⊗Dfin frames, the reduction establishes undecidability of validity on the product frame class, not of derivability in L1⊗L2. As a sharper test, try to exhibit a formula valid on D⊗Dfin that is not derivable in L1⊗L2; such a formula would separate the semantic product logic from the syntactic fusion and show that the negative theorems are about a different object than the paper's Definition 2.5.","verdict_should_be":"CONDITIONAL","load_bearing_attack":"The paper's central negative claim is that Kripke completeness and decidability are not preserved for fusions of one-variable modal logics with equality. But Section 4 proves undecidability of Log^=d(C1⊗C2), i.e., the set of formulas valid on the product frame class. This is not the same as the syntactic fusion L1⊗L2 defined in §2 as the smallest logic containing L1∪L2. For Kripke complete L1,L2, one always has L1⊗L2 ⊆ Log(C1⊗C2); undecidability of the larger set does not imply undecidability of the subset. The Diophantine reduction in Theorem 4.1 shows satisfiability of φ_E over D⊗Dfin, i.e., non-validity of φ_E. Non-validity implies non-derivability only by soundness. The converse direction—unsolvability implies φ_E is *not satisfiable*, hence ¬φ_E is valid—does not imply ¬φ_E is derivable in L1⊗L2 unless completeness for C1⊗C2 is known. That completeness is precisely the transfer property under investigation. Corollary 4.2 makes the conflation explicit by stating the result for the mapping (Log^=d C1, Log^=d C2) ↦ Log^=d(C1⊗C2), a logic that is Kripke complete by definition. Consequently, the abstract's assertion that Kripke completeness and decidability are not preserved for fusions of the defined kind is not established by the body: the theorems address a semantically defined product logic, not the syntactic fusion.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"This paper investigates preservation of Kripke completeness and decidability under fusions of one-variable first-order modal logics. In §3 the authors prove a positive transfer theorem for the equality-free case: if L1 and L2 are Kripke complete one-variable modal logics for frame classes C1, C2 closed under disjoint unions, then their fusion L1⊗L2 is Kripke complete for C1⊗C2 and decidable, for local and global consequence and expanding/constant domain semantics (Theorem 3.1, Lemmas 3.2 and 3.6). They also show the finite model property transfers only for local consequence (Theorems 3.5 and 3.10). In §4 they prove undecidability of the semantic product logic Log^=d(C1⊗C2) in several settings with equality and non-rigid constants, via encodings of Diophantine equations and Minsky machines, and state that this gives non-preservation for fusions with equality. §5 gives a sufficient condition for transfer in propositional fusions sharing an S5 modality using E-homogeneous models.","tokens_in":27842,"tokens_out":12149,"duration_ms":106984,"significance":"The equality-free positive theorem is a substantial result: it extends the classical fusion-transfer theorems to a first-order fragment, using a careful cactus/quasimodel construction. If the property (†) in §3.2 is proved, the decidability part is convincing. The non-preservation results in §4 are interesting as statements about product frame classes, but as written they do not establish the abstract's claim about fusions of logics. The §5 sufficient condition for S5-sharing fusions is a useful contribution and addresses a real problem. Overall, the paper contains valuable ideas but needs substantial revision of the negative claims.","major_comments":[{"comment":"The abstract and Theorem B state that Kripke completeness and decidability are not preserved for fusions with equality. The formal results in Section 4, however, concern Log^=d(C1⊗C2), the set of formulas valid on the product frame class, not the syntactic fusion L1⊗L2 defined in §2. For Kripke complete components one always has L1⊗L2 ⊆ Log^=d(C1⊗C2); undecidability of the superset does not imply undecidability of the fusion, and non-recursive enumerability of the superset does not imply non-recursive enumerability of the subset. Corollary 4.2 states the conclusion for the mapping (Log^=d C1, Log^=d C2) ↦ Log^=d(C1⊗C2), which is not the fusion operation. Moreover, Log^=d(C1⊗C2) is Kripke complete by definition, so the claimed non-preservation of Kripke completeness does not follow from it either. Please either prove the non-preservation for the syntactic fusion or re-state the negative r","section":"§4 (Theorem 4.1, Corollary 4.2), Abstract"},{"comment":"The decidability of local consequence in Theorem 3.1 rests on the recursion in Lemma 3.6: membership in QQQ_i(ϕ) is decided by applying Lemma 3.6 to the Θ_i(ϕ)-quasistate realisations, and this requires adp(Θ_i(Φ)) = max{0,adp(Φ)-1} and adp(Θ_i(Φ)) = adp_{3-i}(Θ_i(Φ)). This is stated as 'Observe that' and no proof is supplied. It is load-bearing: if it fails for some formula shapes, the local decidability transfer collapses. Please give a formal proof of (†) and of the well-foundedness of the recursion, or show that the alternation-depth measure is well-defined.","section":"§3.2, property (†)"}],"minor_comments":[{"comment":"The proof omits the (i)⇒(iii) direction as 'similar to the one-variable case'. Since this implication is essential for completeness/decidability in Theorem 5.2, please spell out the construction of QQQ or give a precise pointer to the corresponding part of Lemma 3.2.","section":"§5, Lemma 5.3"},{"comment":"Theorem 4.6 is stated as a theorem but only an informal sketch is given after it. Either provide the full reduction or explicitly label the statement as a conjecture/sketch.","section":"§4, Theorem 4.6"},{"comment":"The notation '2≤md_i(ϕ)_i' in item (L3) is used without prior definition; please define the iterated box notation used here.","section":"§3.2, Lemma 3.6"}],"recommendation":"major_revision","confidential_remarks":"The positive transfer theorem is strong and likely correct. The main obstacle is the mismatch between the abstract/Theorem B and the formal results in Section 4: the negative theorems are about the semantic product logic rather than the syntactic fusion. This is fixable by rephrasing the claims, but as it stands the advertised non-preservation is not established. I would also ask the authors to supply the missing proof of property (†) in §3.2 before the decidability claim is accepted."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Here's the take: the positive half of this paper is genuinely new and looks correct; the negative half, as presented in the abstract and Theorem B, is not established by the body. The body proves that the semantically defined logic Log^=cd(D⊗Dfin) is undecidable, not that the syntactic fusion L1⊗L2 of two decidable logics is undecidable. Those are different objects.\n\nOn the positive side, the equality-free transfer theorems—completeness and decidability for local and global consequence, expanding and constant domains—are the first systematic treatment for one-variable first-order modal logics. The quasimodel/cactus construction is a real technical piece of work. The shared-S5 theorem (Theorem C) is also new and gives a clean sufficient condition, with the semicommutator applications. The Diophantine encoding itself is clever and shows something interesting about the product logic—but it lands on the wrong target.\n\nThe central issue is the gap between the abstract's claim and what is proven. For the syntactic fusion, you need to show either that the fusion is undecidable or that it is incomplete. Undecidability of the larger Log^=(C1⊗C2) doesn't imply undecidability of the subset L1⊗L2, and validity of ¬φ on the product doesn't imply derivability in the fusion without completeness. The paper needs to either prove those implications for these particular logics or restate the negative results honestly as non-preservation for the frame-class logic. This is not a cosmetic fix; it changes the main contribution.\n\nA smaller concern: property (†) in Section 3.2 is stated as an observation, but the termination of the recursive enumeration for local decidability depends on it. It is plausible, but it should be proved rather than left to the reader. Some other proof details are compressed, consistent with the preliminary-report label.\n\nWho benefits: modal logicians and description-logic people interested in combinations. The positive theorems deserve a place in the literature. The negative claims, as stated, would be a major result if proven for the fusion; right now they are overreach.\n\nRecommendation: send to peer review, but the referee should require the authors to fix the negative statements. If they cannot, the paper can still be salvaged as a positive-transfer paper with a cautionary note about the semantic product.","headline":"Positive fusion transfer theorems are solid and new; the advertised non-preservation results for fusion with equality are not proven—they target the semantic product logic instead.","tokens_in":28310,"tokens_out":4913,"would_cite":true,"duration_ms":45566,"reading_group":"yes","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03B45","03B25"],"pacs":[],"model":"deepseek-v4-flash","headline":"This paper proves that Kripke completeness and decidability transfer under fusions of equality-free one-variable first-order modal logics, for local and global consequence and for both expanding and constant domain semantics — and that addi","keywords":["one-variable first-order modal logic","fusion","Kripke completeness","decidability","local and global consequence","finite model property","equality and non-rigid constants","shared S5 modality"],"falsifier":"Check property (†) on a concrete formula with mixed nesting, for example φ = 2_1 2_2 p ∧ 2_2 2_1 2_2 q with adp(φ) = adp_1(φ), and compute adp(Θ_1(φ)) against max{0, adp(φ)−1} and against adp_2(Θ_1(φ)); a single mismatch is a counterexample to the unproved observation that underpins local decidability.","tokens_in":27369,"feed_emoji":"🧩","tokens_out":6358,"duration_ms":55336,"temperature":0.7,"pith_summary":"The paper asks which good properties survive when two one-variable first-order modal logics are fused — combined without mixing axioms. It proves that, as long as equality is absent, Kripke completeness and decidability transfer for both local and global consequence and under both expanding and constant domain semantics; the finite model property transfers only in the local case. It also shows that once equality is admitted together with non-rigid constants — equivalently, the ability to count up to one — all positive transfer collapses: the fusion can become undecidable, via an encoding of Diophantine equations. A complementary result views one-variable logics as propositional modal logics sharing an S5 modality and gives a sufficient condition for transfer of completeness and decidability in that setting. These results matter because one-variable modal logics are a tractable middle ground between propositional modal logic and full first-order modal logic, and fusion is a standard modular way to build combined logics.","feed_headline":"Decidability survives fusions of one-variable modal logics","feed_subtitle":"Kripke completeness and global/local consequence transfer too; non-rigid constants break it.","key_machinery":"The central device is the cactus model construction, lifted to one-variable first-order logic through quasimodels. A quasistate is a finite set of types — Boolean-consistent sets of subformulas — closed under existential witnesses, so a single finite object stands for arbitrarily many domain elements. Surrogate predicates isolate the two components: each factor replaces the other's maximal modal subformulas by fresh atoms. The fusion proof grafts one component's quasimodels onto the other's at 'thorn' worlds, alternating between the two accessibility relations, until a limit cactus is built whose runs are coherent and saturated for both modalities. For the harder local consequence case, the","core_discovery":"The central assertion is Theorem A: for Kripke complete one-variable first-order modal logics without equality, fusing any two preserves Kripke completeness and decidability of both the local and global consequence relations, under both expanding-domain and constant-domain semantics. The proof uses the cactus model construction lifted through quasimodels: each factor contributes a tapered model, the two are grafted along alternating accessibility relations, and truth of all relevant subformulas is preserved in the limit. The paper further establishes Theorem B: once equality and non-rigid constants are present, the transfer fails — decidability and recursive axiomatisability are not preserve","pith_inferences":["Editorial inference: the paper's boundary suggests that the expressive ability to count up to one is what makes fusion unsafe; one could test whether one-variable logics with genuine counting quantifiers beyond one fail even more badly, perhaps by a similar Diophantine encoding.","Editorial inference: the E-homogeneous model condition is a reusable design pattern — any propositional modal logic that can be inflated so every formula occurs either nowhere or κ times inside each equivalence class can be fused safely; one could try verifying the condition for logics beyond semicommutators, such as graded modal logics.","Editorial inference: the sketched adaptation to monodic fragments over the two-variable fragment with counting suggests that decidability collapses once equality-rich base fragments are combined with modal layers; a full proof for the two-variable-with-counting monodic case would extend Theorem 4.6 beyond the sketch.","Editorial inference: the global finite model property failure for all nontrivial fusions means automated reasoning should target local consequence or develop non-finite bounded structures rather than expect small finite countermodels for global reasoning."],"forward_implications":["Any two Kripke complete, decidable one-variable modal logics without equality can be fused, and the fusion remains Kripke complete and decidable for both local and global consequence, under expanding or constant domains.","Global reasoning in such fusions cannot in general be supported by finite models: for every nontrivial fusion the global finite model property fails, even when both factors have it; only local consequence retains the finite model property.","Equality plus non-rigid constants is a genuine threshold: decidability and recursive axiomatisability are not preserved, with undecidability coming from Diophantine equations.","For fusions of propositional modal logics sharing an S5 modality, Kripke completeness and decidability transfer under the sufficient condition that the components admit E-homogeneous models; semicommutators and expanding products with S5 satisfy this condition.","Because one-variable first-order logic without equality embeds as S5, the proof gives a method for fusing any two modal logics that share an S5 fragment, not just the first-order examples."],"fun_headline_variants":["Fusing one-variable modal logics: completeness survives if no equality","One-variable modal fusion: decidability transfers, but equality breaks it","When modal logics fuse: completeness and decidability transfer unless equality added","Modal fusion paradox: without equality it transfers, with equality it collapses","One-variable modal logics: fusion preserves decidability only without equality"],"cache_read_input_tokens":2304,"weakest_assumption_plain":"The local decidability transfer rests on property (†) in Section 3.2, stated as an observation without proof: projecting a formula through Θ_i lowers its alternating modal depth by exactly one; if that fails for some formula shape, the recursive enumeration of quasistates in Lemma 3.6 need not terminate.","fun_headline_variants_meta":{"raw":{"variants":["Fusing one-variable modal logics: completeness survives if no equality","One-variable modal fusion: decidability transfers, but equality breaks it","When modal logics fuse: completeness and decidability transfer unless equality added","Modal fusion paradox: without equality it transfers, with equality it collapses","One-variable modal logics: fusion preserves decidability only without equality"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000209,"raw_usage":{"total_tokens":1204,"prompt_tokens":665,"completion_tokens":539,"prompt_tokens_details":{"cached_tokens":256},"prompt_cache_hit_tokens":256,"prompt_cache_miss_tokens":409,"completion_tokens_details":{"reasoning_tokens":454}},"tokens_in":409,"tokens_out":539,"duration_ms":59073,"temperature":1.0,"reasoning_tokens":454,"cache_read_input_tokens":256,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-02T18:48:04.873657+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Check property (†) on a concrete formula with mixed nesting, for example φ = 2_1 2_2 p ∧ 2_2 2_1 2_2 q with adp(φ) = adp_1(φ), and compute adp(Θ_1(φ)) against max{0, adp(φ)−1} and against adp_2(Θ_1(φ)); a single mismatch is a counterexample to the unproved observation that underpins local decidability.","supporting_citations":[],"review_version":1}