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).
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$
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 ...