List of axioms:

$(A1)$ - All Tautologies.

$(A2)$ - $(\forall x(\alpha \rightarrow \beta) \rightarrow (\forall x \alpha \rightarrow \forall x \beta)) $.

$(A3)$ - $(\forall x \alpha) \rightarrow [\alpha]^{t}_{x} $ if x is free for t in $\alpha$.

$(A4)$ - $\alpha \rightarrow (\forall x \alpha) $ if x is not free in $\alpha $.

$(A5)$ - $ x = x$

$(A6)$ - $(x=y) \rightarrow (\alpha \rightarrow \beta)$ if $\beta$ if obtained by substitution of at least one occurrence of x free for y in $\alpha$.

Modus Ponens as inference rule.

And Generalization Theorem:

If $\Gamma \vdash \phi$ and x do not occur free in any formula in $\Gamma$, then $\Gamma \vdash \forall x \phi$

My attempt:

  1. $Q(x)$ (hyp)
  2. $\forall y(Q(y) \rightarrow \forall zP(z))$ (hyp)
  3. $\forall y(Q(y) \rightarrow \forall zP(z)) \rightarrow (Q(x) \rightarrow \forall z P(z)) $ (A3)
  4. $Q(x) \rightarrow \forall zP(z)$ (by MP 2,3)
  5. $\forall zP(z)$ (by MP 1,4)
  6. $\forall zP(z) \rightarrow P(x)$ (A3)
  7. $P(x)$ (by MP 5, 6)

And now, I can't use the Generalization Theorem because x does occur free in $\Gamma$. Should I use another path?

  • $\begingroup$ Aren't you missing $z$ in $\forall P(z)$ in the header? $\endgroup$ – Abstraction Aug 22 '16 at 12:55
  • $\begingroup$ Yes, thanks! Edited. $\endgroup$ – Bruno A Aug 22 '16 at 12:57
  • 2
    $\begingroup$ @Magdiragdag: first, derive $(\forall z)P(z)$. Then derive $(\forall x)P(x)$ from that. $\endgroup$ – Carl Mummert Aug 22 '16 at 13:00
  • 1
    $\begingroup$ @Luiz S.: use the generalization theorem on page 117 of Enderton. Certainly $(\forall z)P(z) \vdash P(x)$ by axiom A3. Therefore, by the generalization theorem, because $x$ is not free in $(\forall z)P(z)$, we have $(\forall z) P(z) \vdash (\forall x)P(x)$. $\endgroup$ – Carl Mummert Aug 22 '16 at 13:03
  • 1
    $\begingroup$ I think you can put it anywhere, it's a self-contained derivation to show $(\forall z)P(z) \vdash (\forall x)P(x)$. It just takes some reading of the proof of the generalization theorem to see how to write that derivation. $\endgroup$ – Carl Mummert Aug 22 '16 at 13:08

The $x$ in $Q(x)$ is free, but in $\forall x P(x)$ is bound, therefore they are "different things" and you could carry out the derivation, because when a variable is bound it is called "dummy" because it acts merely as a placeholder, therefore it could be substituted by anything else.

To summarize, the issue is due to the fact that you are using the same symbol $x$ to represent two different things, which is fine as long as you understand that difference. In the first case it is representing a free variable, but in the second it is bounded by the quantifier.

So, if you recognize that, for instance, $\forall x P(x)$ is exactly the same thing as $\forall y P(y)$ or $\forall z P(z)$ then there is no problem to use the generalization theorem. So you can, instead of instantiating $\forall z P(z)$ to $P(x)$, instantiate it to any variable that you like (different from $x$ obviously) and then generalize it to $\forall x P(x)$.


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.