Assume $x$ doesn't occur free in $\alpha$, show that: $$\vdash (\forall x \beta \to \alpha) \leftrightarrow \exists x (\beta \to \alpha)$$
This is an exercise on page 130, A Mathematical Introduction to Logic, Herbert B. Enderton（2ed).
Here's my attempt: For the '$\to$' direction, since $x$ doesn't occur free in $\alpha$, we have $α→∀x α$ and $\forall x \alpha \to \alpha$ as logical axiom(In the second formula, we have$\alpha_x^x = \alpha$). Thus it suffice to show $\vdash (\forall x \beta \to \forall x \alpha) \rightarrow \exists x (\beta \to \alpha)$. By logical axiom $∀ x(α→β)→( ∀ x α→∀x β)$, it would suffice to show $\vdash \forall x (\beta \to \alpha) \rightarrow (\exists x (\beta \to \alpha))$. It has been shown in a previous exercise that there's a deduction $∀ x ϕ→∃x ϕ$, so we are done for the "$\to$" part.
The problem for me is how to show the "$\leftarrow$" direction.
Added: Here's logical axioms that we can employ:
- Tautologies(in the sense of propositional logic);
- $∀ x α →α^x_ t $, where $t$ is substitutable for $x$ in $α$($α^x_ t$ is the formula derived from $\alpha$ by replacing $x$ by a term $t$);
- $∀ x(α→β)→( ∀ x α→∀x β)$;
- $α→∀x α$, where $x$ does not occur free in $α$.
Besides, generalization theorem and deduction principle can be utilized:
If $\Gamma \vdash ϕ$ and $x$ do not occur free in any formula in$\Gamma$, then$\Gamma \vdash ∀ x ϕ$.
If $\Gamma ; γ \vdash ϕ,$ then $\Gamma \vdash γ \to ϕ$.