{"id":"dc5a1273-3346-4db7-9eef-f55b5db9c422","arxiv_id":"2501.16633","paper_version":1,"verdict":"CONDITIONAL","confidence":"HIGH","novelty_score":6.0,"correctness_risk":"low","formal_verification":"none","parameter_count":0,"one_line_summary":"The paper introduces variable non-dependence in first-order logic and proves that bounded quantifiers can be pulled out of formulas whose parts are non-dependent, letting redundant nested quantifiers be dropped.","lead":"This paper defines when the truth of a first-order formula does not depend on the value of one of its variables, possibly under constraints expressed by another formula. It proves rules for pulling redundant quantifiers out of such formulas, which helps clean up formulas produced by translations between scientific theories.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Lemma 1 as printed is false: the non-dependence hypothesis is on the wrong formula, so Theorem 1 cites a false statement; a one-word correction repairs it.","rationale":"The central construction of the paper is Theorem 2, and the intended argument can be repaired: Lemma 1 should state that ψ (not ϕ) is non-dependent of x provided θ. The proof of Theorem 1 applies the lemma to a formula that is indeed non-dependent, so the main simplification theorem is very likely correct after this correction. Nevertheless, the manuscript as printed contains a false lemma, not merely a typo: the counterexample above refutes (6) under the stated hypothesis. This is a genuine correctness issue in the written proof chain and justifies the reader's CONDITIONAL verdict, though the condition is more specific than the reader's stated weakest assumption. The separate theory-relative gap noted by the reader also remains, but the false lemma is the more concrete and immediately checkable defect. The verdict should remain CONDITIONAL: accept only after Lemma 1 is corrected and the theory-level bridge is supplied or explicitly left for future work.","tokens_in":21559,"tokens_out":32755,"duration_ms":309893,"concrete_test":"Re-run the proof of Theorem 1, case Q_{k+1}=∃, checking which formula is fed into Lemma 1. Confirm that ψ=Q_k...f is non-dependent via Remark 3, so the printed 'ϕ' hypothesis is not the one being used. Then test the printed Lemma 1 on the counterexample above: M={0,1,2}, θ(x)=x=0∨x=1, φ=y=y, ψ=P(x,z) with P(0,z)=z=0 and P(1,z)=z=1. Verify that LHS of (6) is true and RHS is false. If so, Lemma 1 must be corrected to assume ψ is non-dependent; check that the corrected proof of Lemma 1 then goes through and that Theorem 2 stands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"Lemma 1 is stated with the hypothesis 'ϕ is non-dependent of x in M provided θ', but its proof and its use in Theorem 1 require the hypothesis on the formula ψ inside the quantifier: ψ must be non-dependent of x provided θ. As printed, Lemma 1 is false. Counterexample: take M={0,1,2} with P(0,z) iff z=0 and P(1,z) iff z=1; let θ(x) be x=0∨x=1, φ be y=y, ψ be P(x,z), and \\bar z=(z). Then φ is non-dependent provided θ (it does not contain x), z is not free in θ, and M|=∃xθ. The left side of (6), ⟦∀x∃z(θ→ψ)⟧, is true (choose z=0 for x=0 and z=1 for x=1), while the right side, ⟦∃xθ→∃z(∀x∈θ)ψ⟧, is false (no single z satisfies P(0,z) and P(1,z)). Hence (6) fails. In Theorem 1 the formula ψ=Q_k...f is non-dependent by Remark 3, so the intended lemma is obtained by replacing 'ϕ' with 'ψ' in the assumption. Until that correction is made, the manuscript contains a false cited statement and the proof of Theorem 1 as written is invalid.","agreement_with_reader":"partial"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper introduces a semantic notion of variable non-dependence for first-order formulas, including a relativized version: a formula phi is non-dependent of variable x in a model M provided theta if the truth of phi is invariant under changing the value of x, as long as the relevant evaluations satisfy theta. After establishing closure properties and equivalent meaning-based characterizations (Propositions 1–5), the paper proves quantifier simplification theorems: Proposition 6 pulls a bounded universal quantifier (forall x in theta) out of Boolean combinations of formulas that are non-dependent of x provided theta; Theorem 1 extends this to arbitrary quantifier prefixes over variables not free in theta; and the central Theorem 2 shows that if each phi_i is non-dependent of x in M provided iota∧epsilon, x is not free in iota, M satisfies exists x epsilon, and the variables in z-bar do not occur free in iota or epsilon, then a bounded quantifier (forall x in epsilon) can be pulled out of the whole formula (Q1 u1 in iota)...(Qk uk in iota) Q-bar z-bar f((forall x in epsilon)phi_1,...,(forall x in epsilon)phi_n), yielding (Q1 u1 in iota)...(Qk uk in iota)(forall x in epsilon) Q-bar z-bar f(phi_1,...,phi_n). The motivation is simplifying convoluted formulas produced by translations between theories, with examples from special relativity and classical kinematics.","tokens_in":21769,"tokens_out":18119,"duration_ms":178315,"significance":"If the results are correct after the repair discussed below, the paper gives a clean, fully semantic account of when redundant nested quantifiers can be discarded. It generalizes the earlier ad-hoc simplification rules used in Lefever's PhD thesis and connects the notion to the SPR+ formulation of the principle of relativity. The proofs are detailed and work directly with sets of satisfying sequences, which makes the variable conditions and the scope of the results transparent; the hypotheses such as M |= exists x epsilon and the freeness conditions are stated explicitly. The main limitation is that the central non-dependence hypothesis is semantic and no general syntactic criterion is supplied, so the theorem is a verification tool rather than an automatic simplification algorithm. For translation applications, a theory-level syntactic corollary would be useful. The paper also provides useful equivalences, especially Proposition 1 and Proposition 7, which connect the new definition to more familiar syntactic forms.","major_comments":[{"comment":"The hypothesis is on the wrong formula. The statement assumes phi is non-dependent of x in M provided theta, but the proof's first step applies Proposition 1(iv) to psi, and Theorem 1's intended application also needs the hypothesis on psi = Q_m z_m ... Q_1 z_1 f(phi_1,...,phi_n). As printed, Lemma 1 is false: take M = {0,1,2} with P(0,z) iff z=0 and P(1,z) iff z=1, let theta(x) be x=0∨x=1, let phi be y=y, and let psi be P(x,z), with z-bar = (z). Then phi is non-dependent of x provided theta, z is not free in theta, and M |= ∃xθ. The left side of (6), [[∀x∃z(θ→ψ)]], is true because for x=0 one can choose z=0 and for x=1 one can choose z=1, while the right side, [[∃xθ→∃z(∀x∈θ)ψ]], is false because no single z satisfies both P(0,z) and P(1,z). The repair is to replace 'phi' by 'psi' in the assumption of Lemma 1; with that change, Theorem 1's application is justified by Remark 3. Until this correction is made, Theorem 1's proof as written cites a false statement.","section":"§3, Lemma 1 (Eq. (6))"}],"minor_comments":[{"comment":"The step marked 'by (i) of Remark 5' is not literally justified because the formula theta may contain x free, whereas Remark 5(i) requires the first conjunct to have no free x. The equality is nevertheless valid: one should first commute the two conjuncts and then apply Remark 5(i) to the second conjunct, which has no free x.","section":"§3, proof of Proposition 3"},{"comment":"The statement should explicitly assume that the bound variable lists x, u_1,...,u_k, and z-bar are pairwise disjoint, or it should note that bound variables may be renamed; otherwise the displayed formulas are potentially ambiguous if x also appears among the quantified variables.","section":"§4, Theorem 2"},{"comment":"For the intended applications to translations, it would be convenient to add a syntactic corollary: if a theory T proves the relevant non-dependence instances and T proves ∃xε, then the two sides of Theorem 2 are provably equivalent in T; the current statement is purely model-theoretic.","section":"§4, applications"},{"comment":"There are several unbalanced parentheses and stray brackets in displayed formulas, for example in Proposition 1 items (ii)–(v), Corollary 1, and Proposition 3; these should be cleaned up in the final version.","section":"Throughout"}],"recommendation":"major_revision","confidential_remarks":"The false Lemma 1 is a typo-level mistake in a load-bearing statement, and the rest of the paper's central argument appears repairable by a one-word correction. I expect the authors can fix this in a short revision; the paper's contribution is modest but appropriate for a mathematical logic journal."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"The paper proves a clean general theorem: under a semantic non-dependence condition, a bounded universal quantifier (∀x∈ε) can be pulled out of an arbitrary Boolean combination, past other quantifiers, and redundant nested copies can be discarded. That is genuinely new relative to the ad hoc simplifications in Lefever's earlier work, and it is exactly what is needed for cleaning up translated formulas in the authors' relativity program. The proofs are detailed, the framework is standard model theory, and the central Theorem 2 appears correct as intended.\n\nWhat is actually good: Definition 2 (conditional non-dependence) is natural, Proposition 7 connects it to a substitution-style criterion, and Theorem 2 is stated with enough generality to be reusable. The paper is honest that the condition is semantic and must be checked in each model; the examples from relativity give the flavor. No fitting, no circularity, and the citation pattern is fine—self-citations point to prior work that is publicly checkable.\n\nSoft spots, in proportion: Lemma 1 as printed is false. The hypothesis says φ is non-dependent of x provided θ, but the proof and Theorem 1 require that hypothesis on ψ (the formula inside the quantifier). The stress-test counterexample works: with M={0,1,2}, θ(x) = (x=0∨x=1), φ = (y=y), and ψ = P(x,z) with P(0,z) iff z=0, P(1,z) iff z=1, equation (6) fails exactly as described. This is a one-word fix—replace φ with ψ in the assumption—and Remark 3 indeed gives that ψ is non-dependent in the uses, so the proof of Theorem 1 is repairable as written. But as submitted, the manuscript cites a false lemma, and a referee should require the correction.\n\nA more substantive limitation, which the reader noted: the main results are model-relative semantic identities. For the advertised application to simplifying theory translations, you really want a syntactic version: if a theory T proves each φ_i is non-dependent of x provided θ (in every model), then T proves the corresponding equivalence. The paper does not state such a corollary. This is not a fatal flaw—the examples show how to verify non-dependence model-by-model—but adding a syntactic corollary would materially increase usefulness for the translation program.\n\nWho is this for: people working on logical interpretations, theory translation, or cylindric algebra simplifications. It deserves a serious referee and publication after fixing Lemma 1 and, ideally, adding the syntactic version. I would recommend sending it to review rather than desk rejection.","headline":"A solid, useful generalization of the authors' earlier quantifier-pulling tricks, with one fixable typo in Lemma 1 and a semantic-condition limitation worth addressing.","tokens_in":22284,"tokens_out":3075,"would_cite":true,"duration_ms":31623,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":["03C07","03B10","03G15"],"pacs":[],"model":"deepseek-v4-flash","headline":"Bounded universal quantifiers can be pulled out of any Boolean combination of formulas that are non-dependent of the quantified variable, making redundant nested quantifiers removable.","keywords":["First-Order Logic","Algebraic Logic","Model Theory","Cylindric Algebras","Simplification Rules","Translation Functions","Logical Interpretation","Nested Quantifiers"],"falsifier":"A counterexample to the theorem would be a model $M$ and formulas $\\varphi_1,\\ldots,\\varphi_n,\\iota,\\varepsilon$ satisfying all hypotheses of Theorem 2 but for which the two meanings differ; the paper's induction proof says no such model exists. A reader who wants to test the boundary of the claim can check the case $M=\\{0,1\\}$, $\\iota=\\top$, $\\varepsilon=\\bot$, $\\varphi_1=(x=0)$, $f=\\neg$: here the equality fails, but $M\\models\\exists x\\varepsilon$ also fails, showing why the satisfiability hypothesis is essential.","tokens_in":21341,"feed_emoji":"","tokens_out":11896,"duration_ms":107006,"temperature":0.7,"pith_summary":"The paper introduces a semantic notion of when a first-order formula does not really depend on one of its variables, possibly under a side condition expressed by another formula. Its main theorem shows that if each subformula is non-dependent of $x$ in this sense, then a bounded universal quantifier $(\\forall x\\in\\varepsilon)$ can be moved to the front of the whole formula, past any Boolean combination and any other quantifiers, and any redundant nested copies of that quantifier can be discarded. The authors' motivating problem is that mechanical translations of one theory into another produce convoluted formulas full of such redundant nested quantifiers; the theorem gives a generic, model-checkable rule for cleaning them up. They demonstrate that the rule covers the translation of special relativity into classical kinematics and that a standard formalization of Einstein's relativity principle can be read as an assertion of variable non-dependence.","feed_headline":"Pull a bounded 'for all' out of any Boolean formula","feed_subtitle":"New non-dependence condition licenses deleting redundant nested quantifiers left by theory translations.","key_machinery":"The central object is the relation '$\\varphi$ is non-dependent of variable $x$ in model $M$ provided $\\theta$' (Definition 2): for every assignment $\\bar a$ and every element $b$, if $M\\models\\theta[\\bar a]$ and $M\\models\\theta[\\bar a^x_b]$, then $M\\models\\varphi[\\bar a]$ iff $M\\models\\varphi[\\bar a^x_b]$. This is a semantic invariance condition, not a syntactic one; it is what lets a bounded quantifier be treated as harmless enough to move. The mechanical work is done by the equivalent meaning identities of Proposition 1, especially the replacements $\\llbracket\\theta\\land(\\exists x\\in\\theta)\\varphi\\rrbracket_M=\\llbracket\\theta\\land\\varphi\\rrbracket_M$ and $\\llbracket\\theta\\to(\\forall x\\in\\theta)\\varphi\\rrbracket_M=\\llbracket\\theta\\to\\varphi\\rrbracket_M$, combined with Proposition 4, which identifies bounded existential and bounded universal quantifiers when the bounding region is satisfiable ($M\\models\\exists x\\theta$), and Proposition 6, which pushes $(\\forall x\\in\\theta)$ out of Boolean combinations of non-dependent formulas.","core_discovery":"Definition 2 is the engine: $\\varphi$ is non-dependent of variable $x$ in model $M$ provided $\\theta$ if, whenever two assignments both satisfy $\\theta$ and differ only in the value of $x$, they agree on the truth of $\\varphi$. Proposition 1 records five equivalent semantic identities, for instance $\\llbracket \\theta\\land(\\exists x\\in\\theta)\\varphi\\rrbracket_M = \\llbracket \\theta\\land\\varphi\\rrbracket_M$ and $\\llbracket \\theta\\to(\\forall x\\in\\theta)\\varphi\\rrbracket_M = \\llbracket \\theta\\to\\varphi\\rrbracket_M$. Theorem 2 then states that when every $\\varphi_i$ is non-dependent of $x$ provided $\\iota\\land\\varepsilon$, with $x$ not free in $\\iota$, no free variable of $\\bar z$ in $\\iota$ or $\\varepsilon$, and $M\\models\\exists x\\varepsilon$, the meanings of $(Q_1u_1\\in\\iota)\\cdots(Q_ku_k\\in\\iota)\\bar Q\\bar z\\, f((\\forall x\\in\\varepsilon)\\varphi_1,\\ldots,(\\forall x\\in\\varepsilon)\\varphi_n)$ and $(Q_1u_1\\in\\iota)\\cdots(Q_ku_k\\in\\iota)(\\forall x\\in\\varepsilon)\\bar Q\\bar z\\, f(\\varphi_1,\\ldots,\\varphi_n)$ coincide in $M$. That is, the bounded universal quantifier can be hoisted across the Boolean expression $f$ and across every quantifier in the prefix, and stacked copies collapse. The proof proceeds by induction on the quantifier prefix, using the propositional distributivity result of Proposition 6 and the standard quantifier equivalences collected in Remark 5.","pith_inferences":["A natural next step, not taken in the paper, is a syntactic sufficient condition for non-dependence: a rewrite procedure that checks whether $\\varphi$ is invariant under $x$ inside the region defined by $\\theta$ would turn the theorem into an algorithm for simplifying generated formulas.","Because the proof is entirely semantic and uses cylindric extensions of formulas, the result may transfer to cylindric algebra equations, where the quantifier-hoisting identity becomes a valid algebraic identity under the corresponding non-dependence condition.","The theorem's reliance on $M\\models\\exists x\\varepsilon$ suggests that in applications where the bounding condition is not known to be satisfiable, one could either add the satisfiability of $\\varepsilon$ as an explicit premise of the translated formula or search for a weaker condition under which the equality still holds."],"forward_implications":["Any formula produced by a translation function can be simplified by one uniform rule, provided the target model satisfies the appropriate non-dependence condition; the paper's example from special relativity and classical kinematics is one instance.","Because the theorem allows arbitrary quantifier series both before and inside the formula, the simplification is not limited to a fixed shape; it applies to every prenex-normal-form formula built from non-dependent subformulas.","The simplified and original formulas are equal in meaning in the given model, not merely provably equivalent in some theory, so the simplification preserves the exact semantic content of the translated axiom.","Formalizations of relativity principles of the SPR+ kind can be understood as non-dependence assumptions, which gives a uniform logical explanation of why inertial-observer choices do not affect experimental descriptions."],"supporting_citations":[{"why":"Supplies the standard first-order quantifier equivalences and prenex normal form used in the proofs of Lemma 1, Theorem 1, and Theorem 2.","marker":"Hinman 2005"},{"why":"The PhD thesis whose translation of special relativity into classical kinematics contains the concrete convolution problem and ad-hoc simplifications that Theorem 2 generalizes.","marker":"Lefever 2017"},{"why":"The companion paper whose interpretation procedure generates redundant nested quantifiers and where the general simplification rule is applied.","marker":"Lefever and Székely 2018"},{"why":"The SPR+ formalization of the relativity principle that Section 4 reinterprets as variable non-dependence.","marker":"Madarász et al. 2017, Section 4.1"},{"why":"Provides the substitution notation used in Proposition 7 to connect non-dependence with the examples from relativity.","marker":"Enderton 2001, p. 112"}],"fun_headline_variants":["Hoist bounded ∀ out of Boolean formulas","Non-dependence lets you drop redundant quantifiers","Pull bounded 'for all' through Boolean connectives","Simplify nested quantifiers with variable non-dependence"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"The argument depends on the semantic condition that each $\\varphi_i$'s truth is unchanged when $x$ changes inside the region $\\iota\\land\\varepsilon$; the paper gives no method for checking this condition, and if it fails the quantifier-pulling equality can be false.","fun_headline_variants_meta":{"raw":{"variants":["Hoist bounded ∀ out of Boolean formulas","Non-dependence lets you drop redundant quantifiers","Pull bounded 'for all' through Boolean connectives","Simplify nested quantifiers with variable non-dependence"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000209,"raw_usage":{"total_tokens":1427,"prompt_tokens":987,"completion_tokens":440,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":603,"completion_tokens_details":{"reasoning_tokens":381}},"tokens_in":603,"tokens_out":440,"duration_ms":5638,"temperature":1.0,"reasoning_tokens":381,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-10T11:49:34.308910+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"A counterexample to the theorem would be a model $M$ and formulas $\\varphi_1,\\ldots,\\varphi_n,\\iota,\\varepsilon$ satisfying all hypotheses of Theorem 2 but for which the two meanings differ; the paper's induction proof says no such model exists. A reader who wants to test the boundary of the claim can check the case $M=\\{0,1\\}$, $\\iota=\\top$, $\\varepsilon=\\bot$, $\\varphi_1=(x=0)$, $f=\\neg$: here the equality fails, but $M\\models\\exists x\\varepsilon$ also fails, showing why the satisfiability hypothesis is essential.","supporting_citations":[],"review_version":1}