Bounded-variable logic: "fewer than $\alpha$ variables" equivalent to "every subformula has fewer than $\alpha$ free variables"?

Question

I believe that "fewer than $\alpha$ variables" is equivalent to "every subformula has fewer than $\alpha$ free variables." The left-to-right implication is straightforward, and from right to left one can always rename variables. For example, the following trivial (and not very useful) theorem of ZFC has no more than two free variables in any subformula:

$$(\exists x) (\forall y) (y\notin x\ \&\ (\exists z) y\in z))$$

It uses three distinct variables (x, y, and z), but because no subformula contains more than two free variables, we can rewrite it to the equivalent:

$$(\exists x) (\forall y) (y\notin x\ \&\ (\exists x) y\in x))$$

So, are the two formulations of the restriction equivalent? If so, why isn't the latter formulation used more often in papers on bounded-variable logic? It seems to have the advantage that it doesn't impose a restriction on the (irrelevant) choice of which variables one uses, limiting only the number that appear free in any given subformula.

Thanks!

Answer 1

If you are speaking of infinitary logic, which your notation (and your other question) suggests, then the statement is not true. Take the case $\alpha=\omega$. Suppose that $\varphi_n$ is a sentence that uses $n$ variables, and cannot be expressed equivalently with fewer than $n$ variables. But $\varphi_n$ has no free variables. Consider the statement $\bigwedge_n \varphi_n$. This is a sentence, having no free variables, and it uses $\omega$ many variables. However, its subformulas are itself (with no free variables), plus the subformulas of any $\varphi_n$, which each have at most $n$ free variables.

Thus, this assertion has the property that every subformula has fewer than $\omega$ free variables, but the assertion does not use fewer than $\omega$ variables. So it seems to be a negative example to your conjecture.

To take a specific example, let $\varphi_n$ assert "there are at least $n$ distinct objects", which can be expressed in a finite formula using $n$ variables. The conjunction $\bigwedge_n \varphi_n$ asserts that the universe is infinite.