By Rule T, it is sufficient to show both $\vdash(\alpha\rightarrow\exists x\beta)\rightarrow\exists x(\alpha\rightarrow\beta)$ and $\vdash\exists x(\alpha\rightarrow\beta)\rightarrow(\alpha\rightarrow\exists x\beta)$ .

The first one, by deduction, contraposition and MP rules, is “equivalent” to $\forall x\neg(\alpha\rightarrow\beta)\vdash\neg(\alpha\rightarrow\exists x\beta)$ . Now, by axiom group 2 and MP, $\forall x\neg(\alpha\rightarrow\beta)\vdash\neg(\alpha\rightarrow\beta)$ . Further, $\neg(\alpha\rightarrow\beta)\rightarrow\alpha$ and $\neg(\alpha\rightarrow\beta)\rightarrow\neg\beta$ are tautologies. By MP, we have both $\forall x\neg(\alpha\rightarrow\beta)\vdash\alpha$ and $\forall x\neg(\alpha\rightarrow\beta)\vdash\neg\beta$ . By the generalization theorem, $\forall x\neg(\alpha\rightarrow\beta)\vdash\forall x\neg\beta$ . Since $\{\alpha,\forall x\neg\beta\}$ tautologically implies $\neg(\alpha\rightarrow\neg\forall x\neg\beta)$ , by Rule T, we have what we need.

The second one, by deduction, contraposition and MP rules, is “equivalent” to $\neg(\alpha\rightarrow\exists x\beta)\vdash\forall x\neg(\alpha\rightarrow\beta)$ . For this formula, using the generalization theorem based on the fact that $x$ does not occur free in $\alpha$ , it is sufficient to show $\neg(\alpha\rightarrow\exists x\beta)\vdash\neg(\alpha\rightarrow\beta)$ , which, by contraposition, deduction and MP rules, is “equivalent” to $\{\alpha,\alpha\rightarrow\beta\}\vdash\exists x\beta$ . By MP rule, it is sufficient to show $\vdash\beta\rightarrow\exists x\beta$ , or, by deduction, $\beta\vdash\exists x\beta$ , or, by contraposition and MP, $\vdash\forall x\neg\beta\rightarrow\neg\beta$ , which is an axiom of group 2.

By substituting $\neg\alpha$ for $\alpha$ and $\neg\beta$ for $\beta$ , and using contraposition tautologies among other things, we obtain $\vdash(\forall x\beta\rightarrow\alpha)\leftrightarrow\exists x(\beta\rightarrow\alpha)$ . Well, this approach is taken from the text, where it was used in a similar example on pages 121-122. However, it seems not completely fair, as among other things we would need to use the contraposition tautology inside the quantified formula $\exists x(\alpha\rightarrow\beta)$ . Of course, we could easily argue that by substituting tautologically equivalent subformulas we obtain formulas that can be proved from each other, but I don’t think there was a theorem saying this.

Alternatively, by using instead of $\alpha$ and $\beta$ their negations, what we need to show is $\vdash(\forall x\neg\beta\rightarrow\neg\alpha)\rightarrow\exists x(\neg\beta\rightarrow\neg\alpha)$ and $\vdash\exists x(\neg\beta\rightarrow\neg\alpha)\rightarrow\forall x\neg\beta\rightarrow\neg\alpha$ . Now, we can use the contraposition tautology for those prime formulas that are outside of any quantified subformulas, obtaining $\vdash(\alpha\rightarrow\exists x\beta)\rightarrow\exists x(\neg\beta\rightarrow\neg\alpha)$ and $\vdash\exists x(\neg\beta\rightarrow\neg\alpha)\rightarrow\alpha\rightarrow\exists x\beta$ . So, given what we have already proved, if we show that $\vdash\exists x(\neg\beta\rightarrow\neg\alpha)\leftrightarrow\exists x(\alpha\rightarrow\beta)$ , we are done (this formula also illustrates the point that we need to use the contraposition tautology inside quantified formulas). By using deduction and contraposition theorems, as well as MP, it is sufficient to show that $\vdash\forall x\neg(\alpha\rightarrow\beta)\leftrightarrow\forall x\neg(\neg\beta\rightarrow\neg\alpha)$ . By axiom group 3, MP and generalization theorem, it is sufficient to show that $\vdash\neg(\alpha\rightarrow\beta)\leftrightarrow\neg(\neg\beta\rightarrow\neg\alpha)$ , which is a tautology (we were able to get rid of all quantifiers to use axiom group 1).