I believe that "less than $\alpha$ variables" is equivalent to "every subformula has less 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!

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!