When I was a kid learning algebra for the first time, I remember finding it unintuitive that each instance of a given variable had to refer to the same thing. "Why can't I set the first occurrence of $x$ to one value and the second occurrence of $x$ to a different value?" I wondered. Obviously, that's not how we do things in ordinary mathematics. However, certain formalisms like the Backus-Naur form for context free grammars use "symbols" which behave in much the same way that I imagined variables did when I was a kid. Logically, the set of mathematical statements that you can formalize using "non-coreferenced" variables like this should be exactly the set of statements that can be given by a formula with traditional "coreferenced variables" that uses no variable more than once. So my question is: what is this class of statements? Surely these "non-coreferenced" variables are strictly less expressive than the kind we typically use. But how much less expressive?
EDIT: "One occurrence of each variable" must I suppose exclude occurrences with a quantifier, so that $\forall x.P(x)$ would be allowed, but $\forall x.R(x, x)$ would not. But perhaps even this class is too large to accurately reflect the behavior of "non-coreferenced" variables; I am not sure exactly how to restrict it to make it behave as desired.