This question is from Shoenfield's "Mathematical Logic", an exercise on page 25.
Show that the formula $((x \neq x) \vee \neg(x \neq x \vee x \neq x)) \vee (x \neq x \vee x \neq x)$ is a theorem, but is not provable without the associative rule.
There is also a hint:
Consider the mapping $f$ from the set of formulas to the set of integers defined as:
$f(A) = 0 $ for atomic formulas
$f(\neg A) = 1 - f(A)$
$f(A \vee B) = f(A).f(B).(f(A) + f(B) - 1)$
$f(\exists x A) = f(A)$
Show that if $A$ is provable without the associative rule, then $f(A) = 0$
The hint is easy to verify, but the given formula also evaluates to $0$. So what should I do next?
Long comment
Your concern (as well as Mitchell's comment) is correct : the "unprovable" formula must be evaluated to $1$ by $f$.
The "mechanism" of the proof (see previous exercises) is that with the said $f$, all axioms are evaluated to $0$ and the rules are sound, i.e. from premises eveluated to $0$ they produce conclusion that are so.
Thus, if the formula would be provable, by "soundness" it must evaluate to $0$, which is not.
Thus, we have to modify accordingly the rule for evaluating $\lor$ : I think that it must be "non-standard" in order that the independence proof will work.