Should $x$ be not free in $\beta$ to prove $\vdash [ \forall x(\beta\rightarrow \alpha)\rightarrow (\exists x\beta\rightarrow \alpha)]$?

In "Mathematical Introduction to Logic, Enderton" This is an example where readers are asked to convince themselves that :

If $x$ does not occuer free in $\alpha$ then, $\vdash [ \forall x(\beta\rightarrow \alpha)\leftrightarrow (\exists x\beta\rightarrow \alpha)]$

For me, We have to assume that $x$ is not free in $\beta$ too. The reason comes from the argument:

To prove that: $\vdash [ \forall x(\beta\rightarrow \alpha)\rightarrow (\exists x\beta\rightarrow \alpha)]$, It suffice to prove (using deduction theorem) that $\{\forall x(\beta \rightarrow \alpha),\exists x\beta\}\vdash \alpha$, So, it suffice to show that (using contraposition): $\{\forall x(\beta \rightarrow \alpha),\neg\alpha \}\vdash \neg\exists x\beta $.

Since we have $\forall x(\beta \rightarrow \alpha)$, we can deduce $(\beta \rightarrow \alpha)$, but we have $\neg\alpha$ so we can deduce $\neg\beta$. If $x$ is NOT free in $\beta$, we can use generalization theorem to deduce $\forall x \neg\beta$ which is essentially $\neg\exists \beta$. thus we have showed that $\{\forall x(\beta \rightarrow \alpha),\exists x\beta\}\vdash \alpha$ and we are done.

My point is that, In order for this proof to be valid, we needed to assume that $x$ does not occur free in $\beta$ hence we need this assumption from the beginning.

So the question, Do we need to assume $x$ is not free in $\beta$? Or is there any other proof for this fact without any need for this assumption (in this case, please, provide such proof).

  • $\begingroup$ See Enderton, page 122 : "If $x$ does not occur free in $\alpha$, then $⊢(∃xβ→α)↔∀x(β→α)$. The reader might want to convince him- or herself that the above formula is valid." $\endgroup$ – Mauro ALLEGRANZA Jan 28 '15 at 21:38
  • $\begingroup$ @MauroALLEGRANZA, I've already mentioned that the formula is in enderton's book. But As mentioned above, it seems that We need to assume that $x$ is not free in $\beta$ too. $\endgroup$ – Fawzy Hegab Jan 28 '15 at 21:45
  • 1
    $\begingroup$ @MauroALLEGRANZA, Sorry, It's just a typo while writing, I've edited it... $\endgroup$ – Fawzy Hegab Jan 28 '15 at 21:53
  • 1
    $\begingroup$ If $x$ is not free in $\alpha$ of $\beta$ then the equivalence is trivial, because the quantifier over $x$ has no effect over the formula if neither formula has $x$ free. $\endgroup$ – Carl Mummert Jan 29 '15 at 0:29
  • $\begingroup$ @Carl Mummert, You are right, I didn't notice that.. $\endgroup$ – Fawzy Hegab Jan 30 '15 at 6:17

NO; the only proviso needed is : $x \notin FV(\alpha)$.

The complete proof is :

1) $∀x(β→α)$ --- assumed

2) $¬α$ --- assumed [a]

3) $(β→α)$ --- from 1) by Ax.2 and modus ponens

4) $\lnot \alpha \rightarrow \lnot \beta$ --- from 3) by taut impl (contraposition)

5) $\lnot \beta$ --- from 2) and 4) by mp

6) $\forall x \lnot \beta$ --- from 5) by Gen Th; the assumptions are 1) : no $x$ free, and 2) : $x$ not free in $\alpha$ by proviso

7) $\lnot \alpha \rightarrow \forall x \lnot \beta$ --- from 2) and 6) by DT, discharging [a]

8) $\lnot \forall x \lnot \beta \rightarrow \alpha$ --- from 7) by taut impl

9) $\exists x \beta \rightarrow \alpha$ --- by abbreviation for $\exists$

10) $∀x(β→α) \rightarrow (\exists x \beta \rightarrow \alpha)$ --- from 1) and 9) by DT.

The proviso : $x \notin FV(\alpha)$ is needed in step 6) for the correct application of Gen Th. The proviso in it is relative to the assumptions and not to the formula itself "to be generalized" (in our case : $\beta$).

If, in order to apply Gen Th to $\beta$, we require that $x$ is not free in it, the result of the generalization : $\forall x \beta$ would be quite useless ...

  • $\begingroup$ In step 6, we are proving that $\neg\beta\vdash \forall x\neg\beta$, So using generlization theorem, $x$ must NOT be free in $\beta$ not $\alpha$. Here the assumptions are $\{\neg\beta\}$ not $\{ \alpha\}$... $\endgroup$ – Fawzy Hegab Jan 28 '15 at 21:59
  • 1
    $\begingroup$ Sorry, After revising the steps, I got my mistake! Thanks! $\endgroup$ – Fawzy Hegab Jan 28 '15 at 22:03
  • $\begingroup$ $x\not \in FV(\alpha)$, what really means?, if it wasn't. The mean of the formula $\alpha$ would change, right? is that the reason? or what $\endgroup$ – jonaprieto Jul 4 '16 at 1:10
  • $\begingroup$ @jonaprieto - $x \notin FV(\alpha)$ means: "the variable $x$ is not free in formula $\alpha$". Example: $x \notin FV (\forall x (x=x))$. $\endgroup$ – Mauro ALLEGRANZA Jul 4 '16 at 9:21

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.