Show that a given formula is not provable without the associative rule

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?

• You might get more help if you don't limit yourself to those who have a copy of your book. – DanielV Nov 12 '16 at 1:32
• What would be the point in defining $f(A \vee B) = f(A)\cdot f(B)\cdot(f(A) + f(B) - 1)?$ Isn't that the same as saying $f(A \vee B) = f(A)\cdot f(B)$ (since the values of $f(x)$ are always $0$ or $1)?$ I suspect that there's a typo in the definition of $f$ in the book. – Mitchell Spector Nov 12 '16 at 2:26

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.