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 ϕ$.
Best Answer
Having the OP's question already received answers, I submit this "long" comment aimed at providing a proof using Enderton's axioms and modus ponens, which is the only rule of inference (see Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001)).
We have to prove (Q3A) [see Exercise 8, page 130] :
First part : $\leftarrow$
(1) $\forall x \beta$ --- assumed
(2) $\beta_c^x$ --- from (1) by Ax.2 and mp, where the constant symbol $c$ does not occur in $\alpha, \beta$
(3) $\beta_c^x \rightarrow \alpha$ --- assumed
(4) $\alpha$ --- from (2) and (3) by mp
By COROLLARY 24H (RULE EI) [page 124], having proved $\forall x \beta, \beta_c^x \rightarrow \alpha \vdash \alpha$, where $c$ does not occur in $\beta$ nor in $\alpha$ (because $x \notin FV(\alpha)$), we have :
(5) $\forall x \beta, \exists (\beta \rightarrow \alpha) \vdash \alpha$
Second part : $\rightarrow$
(1) $\lnot \beta \vdash \beta \rightarrow \alpha$ --- by $\vDash_{TAUT} \lnot \phi \rightarrow (\phi \rightarrow \psi)$, assuming $\lnot \beta$
(2) $\forall x \beta \rightarrow \alpha$ --- assumed
(3) $\lnot \exists x (\beta \rightarrow \alpha)$ --- assumed
(4) $\exists x (\beta \rightarrow \alpha)$ --- from (1) by the "derived rule" : $\varphi_t^x \rightarrow \exists x \varphi$ [provable from Ax.2] and mp
Thus we have : $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$, from (1) and (4) and $\lnot \beta, \lnot \exists x (\beta \rightarrow \alpha) \vdash \lnot \exists x (\beta \rightarrow \alpha)$, from (1) and (3); we apply : COROLLARY 24E (REDUCTIO AD ABSURDUM) [page 119] and $\vDash_{TAUT} \lnot \lnot \phi \rightarrow \phi$ and mp to conclude with :
(5) $\lnot \exists x (\beta \rightarrow \alpha) \vdash \beta$
(6) $\forall x \beta$ --- from (5) by GENERALIZATION THEOREM [page 117] ($x$ is not free in assumptions (2), because $x \notin FV(\alpha$), and (3) and assumption (1) has been "discharged" in (5))
(7) $\alpha$ --- from (2) and (6) by mp
(8) $\beta \rightarrow \alpha$ --- From (7) and $\vDash_{TAUT} \phi \rightarrow (\psi \rightarrow \phi)$ and mp
(9) $\exists x(\beta \rightarrow \alpha)$ --- from (8) by the "derived rule" in (4) above
We apply again COROLLARY 24E (REDUCTIO AD ABSURDUM) with : $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \lnot \exists x (\beta \rightarrow \alpha)$, and $\lnot \exists x (\beta \rightarrow \alpha), \forall x \beta \rightarrow \alpha \vdash \exists x (\beta \rightarrow \alpha)$, from (2)-(9), and Double Negation to conclude with :
Addendum
We add as an exercise the proof in Enderton's system of (Q2B) [see Exercise 8, page 130] :
First part : $\rightarrow$
(I've "streamlined" a little bit the "tautological" steps)
(1) $\alpha \rightarrow \exists x \beta$ --- assumed
(2) $\forall x \lnot (\alpha \rightarrow \beta)$ --- assumed
(3) $\alpha \land \lnot \beta$ --- from (2) by Taut
(4) $\lnot \beta$ --- from (3) by Taut
(5) $\forall x \lnot \beta$ --- by the Generalization Theorem [page 117], because $x$ is not free in assumptions (1) and (2)
(6) $\lnot \exists x \beta$ --- abbreviation
(7) $\alpha$ --- from (3) by Taut
(8) $\exists x \beta$ --- from (1) by mp.
Having derived the contradiction [with (6) and (8)], we apply Corollary 24E (Reductio ad Absurdum) [page 119] : if $\Gamma \cup \{ \varphi \}$ is inconsistent, then $\Gamma \vdash \lnot \varphi$, with $\Gamma = \{ \alpha \rightarrow \exists x \beta \}$, and $\varphi := \forall x \lnot (\alpha \rightarrow \beta)$.
Thus we may conclude :
(9) $\lnot \forall x \lnot (\alpha \rightarrow \beta)$
that is : $\alpha \rightarrow \exists x \beta \vdash \exists x (\alpha \rightarrow \beta)$.
Finally :
Second part : $\leftarrow$
(1) $\alpha \rightarrow \beta[x/c]$ --- assumed, where $c$ is an individual constant
(2) $\lnot \beta[x/c] \rightarrow \lnot \alpha$ --- by Taut
(3) $\forall x \lnot \beta$ --- assumed
(4) $\lnot \beta[x/c]$ --- from Ax.2 and (3) by mp
(5) $\lnot \alpha$ --- form (2) and (4) by mp
(6) $\forall x \lnot \beta \rightarrow \lnot \alpha$ --- form (3) and (5) by Deduction Theorem
(7) $\alpha \rightarrow \lnot \forall x \lnot \beta$ --- by Taut
(8) $\alpha \rightarrow \exists x \beta$ --- abbreviation.
Now we apply Corollary 24H (Rule EI) : assume that the constant symbol $c$ does not occur in $\varphi, \psi$ or $\Gamma$, and that $\Gamma \cup \{ \varphi[x/c] \} \vdash \psi$; then $\Gamma, \exists x \varphi \vdash \psi$, where $\Gamma = \emptyset$, $\varphi[x/c] := \alpha \rightarrow \beta[x/c]$ and $\psi := \alpha \rightarrow \exists x \beta$.
Thus we may conclude with :
$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.
Finally :
The theorem follows from (A) and (B).
2nd Addendum
For the second part : $\leftarrow$, we can prove it without Corollary 24H (Rule EI).
(1) $\exists x(\alpha \rightarrow \beta)$ --- assumed
(2) $\alpha$ --- assumed
(3) $\lnot \exists x \beta$ --- assumed
(4) $\lnot \lnot \forall x \lnot \beta$ --- abreviation for $\exists$
(5) $\forall x \lnot \beta$ --- by Taut
(6) $\lnot \beta$ --- Ax.2
(7) $\vDash_{TAUT} \alpha \rightarrow (\lnot \beta \rightarrow \lnot (\alpha \rightarrow \beta))$
(8) $\lnot (\alpha \rightarrow \beta)$ --- from (2), (6) and (7) by mp
(9) $\forall x \lnot (\alpha \rightarrow \beta)$ --- by Gen Th ($x \notin FV(\alpha)$)
(10) $\lnot \exists x (\alpha \rightarrow \beta)$ --- abbreviation
(11) $\lnot \lnot \exists x \beta$ --- we apply Corollary 24E (Reductio ad Absurdum) [page 119] to (3), with (1) and (10)
(12) $\exists x \beta$ --- by Taut
(13) $\alpha \rightarrow \exists x \beta$ --- from (2) by Deduction Theorem.
So again :