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$ Jan 28, 2015 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$ Jan 28, 2015 at 21:45
  • 1
    $\begingroup$ @MauroALLEGRANZA, Sorry, It's just a typo while writing, I've edited it... $\endgroup$ Jan 28, 2015 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$ Jan 29, 2015 at 0:29
  • $\begingroup$ @Carl Mummert, You are right, I didn't notice that.. $\endgroup$ Jan 30, 2015 at 6:17

1 Answer 1


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$ Jan 28, 2015 at 21:59
  • 1
    $\begingroup$ Sorry, After revising the steps, I got my mistake! Thanks! $\endgroup$ Jan 28, 2015 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$ Jul 4, 2016 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$ Jul 4, 2016 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.