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?

  • 1
    $\begingroup$ You might get more help if you don't limit yourself to those who have a copy of your book. $\endgroup$ – DanielV Nov 12 '16 at 1:32
  • 1
    $\begingroup$ 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. $\endgroup$ – Mitchell Spector Nov 12 '16 at 2:26

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.