On variable non-dependence of first-order formulas

TL;DR

The paper introduces variable non-dependence of first-order formulas on a variable $x$ under a condition $theta$ within a model-theoretic framework. It establishes multiple equivalent characterizations, shows closure properties, and proves a bounded-quantifier extraction principle enabling $(∀ x ∈ θ)$ to be pulled out from complex Boolean compositions when subformulas are non-dependent. The authors apply these results to simplify translations between theories (e.g., from special relativity to classical kinematics) and to notions like ether-observer-independence and SPR+, arguing that the approach yields clearer, more tractable translations and provides practical tools for automatic formula simplification. Overall, the work offers a formal mechanism to detect and exploit variable independence to streamline logical translations and formalizations in physics-inspired logics.

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 (5)

• Figure 1: Here the grey color represents values which make the formulas true and white represents values which make the formulas false. On the left we have the formula $x \geq y$ of which the truth value is dependent of both the variables $x$ and $y$. Only changing the value of $x$ while keeping $y$ constant can change the truth value of this statement. On the right we have the formula $1 \leq y \leq 2$ which is variable non-dependent of $x$. Whatever value we choose for $x$, the truth value of that statement does not change since it is only dependent of the value of $y$.
• Figure 2: Let the medium grey $\left\llbracket\varphi\right\rrbracket^{\mathfrak{M}}$ be the set of all values of $x$ and $\bar{y}$ in $M^{\omega}$ for which $\varphi$ is true. On the right, the meaning of "exists" (light grey rectangle, actually a cylinder with an infinite number of dimensions) and "for all" (dark grey rectangle) are added, illustrating that $\left\llbracket\forall x\varphi\right\rrbracket^{\mathfrak{M}} \subseteq \left\llbracket\varphi\right\rrbracket^{\mathfrak{M}} \subseteq \left\llbracket\exists x \varphi\right\rrbracket^{\mathfrak{M}}$. Note that the axis $\bar{y}$ is represented as a vector because there are an infinite number of dimensions in $M^{\omega}$.
• Figure 3: On the left hand, we see a formula $\varphi$ which is not non-dependent of $x$: changing the $x$-value from $a_i$ into $b$ changes the truth value of $\varphi$. However, on the right we see that adding an extra condition $\theta$ does make $\varphi$ non-dependent of $x$ provided $\theta$: changing the $x$-value does never change the truth value of $\varphi$ as long as the evaluations of variables remain inside the area defined by $\left\llbracket\theta\right\rrbracket^{\mathfrak{M}}$.
• Figure 4: This figure illustrates the order of proving the equivalences between the items of Proposition \ref{['prop:indep']}. We need to prove "(iii)$\implies$(i)" directly because in the proof of "(iii)$\implies$(v)" we use the equivalence of (iii) and (i).
• Figure 5: This figure illustrates the special case used in Section \ref{['sec:Application']}, i.e., when the provided condition is of the form $\theta=\iota\land\varepsilon$ for some formulas such that $x$ does not occur free in $\iota$ and certain bound variables of $\varphi$ do not occur free in $\varepsilon$ and $\iota$. Here $\left\llbracket\theta\right\rrbracket^{\mathfrak{M}} = \left\llbracket\iota\right\rrbracket^{\mathfrak{M}} \cap \left\llbracket\varepsilon\right\rrbracket^{\mathfrak{M}}$ is represented by the area inside the dashed rectangle.

Theorems & Definitions (34)

• Remark 1
• Remark 2
• Definition 1
• Definition 2
• Remark 3
• Remark 4
• Proposition 1
• proof
• Proposition 2
• proof