REVIEW 1 major objections 4 minor 4 references
On variable non-dependence of first-order formulas
T0 review · 1 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash
Pith's one-line read 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.
desk verdict 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. read the letter →
The pith
A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.
The reading
What carries the argument
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.
What would settle it
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.
Extended reading notes
Core claim
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.
Load-bearing premise
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.
Editorial extensions
If this is right
- 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.
Reading between the lines
- 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.
Signed reviews
Editorial analysis
A structured set of objections, weighed in public.
Referee Report
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.
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 (1)
- [§3, Lemma 1 (Eq. (6))] 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.
minor comments (4)
- [§3, proof of Proposition 3] 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.
- [§4, Theorem 2] 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.
- [§4, applications] 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.
- [Throughout] 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.
Circularity Check
No significant circularity: Theorem 2 is a genuine derivation from Definition 2; self-citations are motivational, and the Lemma 1 hypothesis typo is a correctness issue, not a circular one.
full rationale
The paper's derivation chain is self-contained in the relevant sense. Definition 2 introduces the semantic notion of non-dependence; Proposition 1 proves equivalent meaning-equality characterizations; Propositions 2-6 and Lemma 1 then build quantifier-pulling rules; Theorem 1 lifts these to Boolean combinations and quantifier series; Lemmas 2-3 and Theorem 2 apply the framework to the translation-simplification setting with θ = ι∧ε. The main simplification identity is not equivalent to the non-dependence definition by construction: it has additional hypotheses (x not free in ι, M |= ∃xε, no variables of z̄ free in ι or ε) and its conclusion is a meaning equality between two syntactic forms, which is derived rather than assumed. The non-dependence of the φ_i is an antecedent condition, not a fitted parameter or a renamed version of the target equality. Citations to earlier work by the authors, e.g. Lefever 2017 and Lefever and Székely 2018, appear as motivation and application context, not as load-bearing premises in the proofs; no uniqueness theorem or ansatz is imported from those papers. The paper also does not rename a known empirical pattern: it proves general model-theoretic simplification rules from an explicitly stated semantic definition. One non-circular correctness defect should be flagged: Lemma 1 as printed states that φ is non-dependent of x provided θ, but the proof and its use in Theorem 1 require the corresponding hypothesis on ψ, the formula inside the quantifier. The skeptic's counterexample shows the printed statement is false. This is a typo/omission in the hypothesis, not circularity, because the intended corrected lemma follows from Proposition 1 and Remark 3 rather than being assumed as the conclusion.
Assumptions & free parameters
assumptions (5)
- standard math Standard Tarskian satisfaction relation for first-order logic with equality over infinite variable sequences.
- standard math Every first-order formula is logically equivalent to a prenex normal form formula.
- standard math The truth of a formula depends only on the values of its free variables.
- standard math Standard quantifier equivalences when a quantified variable is not free in the other operand (Remark 5).
- domain assumption The set of variables is countably infinite and fixed as v1, v2, ... (Convention 1).
Cite this review
Pith. "Pith review of On variable non-dependence of first-order formulas." pith.science (2026). https://pith.science/paper/SEI6MSXN
@misc{pith2026250116633,
author = {Pith},
title = {Pith review of: On variable non-dependence of first-order formulas},
year = {2026},
howpublished = {\url{https://pith.science/paper/SEI6MSXN}},
note = {Machine review of arXiv:2501.16633}
}
read the original abstract
In this paper, we introduce a concept of non-dependence of variables in formulas. A formula in first-order logic is non-dependent of a variable if the truth value of this formula does not depend on the value of that variable. This variable non-dependence can be subject to constraints on the value of some variables which appear in the formula, these constraints are expressed by another first-order formula. After investigating its basic properties, we apply this concept to simplify convoluted formulas by bringing out and discarding redundant nested quantifiers. Such convoluted formulas typically appear when one uses a translation function interpreting a theory into another.
Figures
Figures from the paper (2 more)
Reference graph
Works this paper leans on
-
[1]
Andr´ eka, H., Gyenis, Z., N´ emeti, I. and Sain, I. (2022),Universal Algebraic Logic: Dedicated to the Unity of Science , Springer International Publishing. Andr´ eka, H., Madar´ asz, J. X. and N´ emeti, I. (2006), Logical axiomatizations of space-time. samples from the literature, in A. Pr´ ekopa and E. Moln´ ar, eds, ‘Non-Euclidean Geometries: J´ anos ...
work page 2022
-
[19]
URL: https://dx.doi.org/10.1088/0253-6102/66/1/019 Madar´ asz, J. X. (2002), Logic and Relativity (in the light of definability theory), PhD thesis, E¨ otv¨ os Lor´ and Univ., Budapest. – PREPRINT – ON V ARIABLE NON-DEPENDENCE OF FIRST-ORDER FORMULAS 23 Madar´ asz, J. X., Stannett, M. and Sz´ ekely, G. (2022), ‘Investigations of isotropy and homo- geneity ...
-
[33]
Barrett, T. W. and Halvorson, H. (2016 a), ‘Glymour and Quine on theoretical equivalence’, Journal of Philosophical Logic 45(5), 467–483. Barrett, T. W. and Halvorson, H. (2016b), ‘Morita equivalence’, The Review of Symbolic Logic 9(3), 556–582. Das, M., Ramanan, N., Doppa, J. R. and Natarajan, S. (2019), ‘One -shot induction of gener- alized logical conc...
work page Pith review arXiv 2016
-
[550]
URL: https://doi.org/10.1215/00294527-2022-0029 Khaled, M. and Sz´ ekely, G. (2021), Algebras of concepts and the ir networks, in T. Allahvi- ranloo, S. Salahshour and N. Arica, eds, ‘Progress in Intelligent Dec ision Science’, Springer International Publishing, Cham, pp. 611–622. Khaled, M. and Sz´ ekely, G. (2024), ‘Conceptual distance and algebras of c...
Reviewed August 10, 2026 · model on record in the stance chip above.
Discussion (0). Continue with ORCID to comment.