How to show that $\vdash (\forall x \beta \to \alpha) \leftrightarrow \exists x (\beta \to \alpha)$?

Solution 1:

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] :

$\vdash (\forall x \beta \rightarrow \alpha) \leftrightarrow \exists x (\beta \rightarrow \alpha)$, if $x$ does not occur free in $\alpha$.

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$

(6) $\exists (\beta \rightarrow \alpha) \vdash (\forall x \beta \rightarrow \alpha)$ --- from (5) by DT.

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 :

(10) $(\forall x \beta \rightarrow \alpha) \vdash \exists x (\beta \rightarrow \alpha)$.

Addendum

We add as an exercise the proof in Enderton's system of (Q2B) [see Exercise 8, page 130] :

$\vdash (\alpha \rightarrow \exists x \beta) \leftrightarrow \exists x (\alpha \rightarrow \beta)$, if $x$ does not occur free in $\alpha$.

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 :

(A) $\vdash (\alpha \rightarrow \exists x \beta) \rightarrow \exists x (\alpha \rightarrow \beta)$ --- by Deduction Theorem.

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 :

(B) $\vdash \exists x (\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \exists x \beta)$.

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 :

$\exists x (\alpha \rightarrow \beta) \vdash (\alpha \rightarrow \exists x \beta)$.

Solution 2:

If $\alpha$ holds, both sides of the iff are true, since anything implies true. So suppose $\alpha$ is false.

Now assume $\exists x (\beta \to \alpha)$. Then take $c$ as such an $x$, and get to $$\beta_c^x \to \alpha,$$ where we have used $\alpha_c^x=\alpha$, since $x$ is not free in $\alpha$. Since $\alpha$ is false, $\beta_c^x$ must be false, so that also $\forall x \beta$ is false, and from this $\forall x \beta \to \alpha$ follows.

I think the steps here are reversible, so that one could do the forward implication in a similar way. However the OP only asked about the reverse implication just treated. I used "existential instantiation" (which is what one text I used called it), which is not one of the rules cited in the OP, however I think it must be there somehow in any formal axiomitization.

Solution 3:

As coffeemath has already observed, the interesting case is α being false. In that situation the implication towards α is the same as negation, which means the direction from left-to-right is in fact just a variant of the de-Morgan law for quantifiers (the hard classical part of it).

Lets switch notation to that of the formal proof system Isabelle/Isar. The proof of that part of de-Morgan then looks like this:

theorem de_Morgan_classical:
  assumes *: "¬ (∀x. B x)"
  shows "∃x. ¬ B x"
proof (rule classical)
  assume **: "¬ (∃x. ¬ B x)"
  have "∀x. B x"
  proof
    fix x show "B x"
    proof (rule classical)
      assume "¬ B x"
      then have "∃x. ¬ B x" ..
      with ** show "B x" by contradiction
    qed
  qed
  with * show "∃x. ¬ B x" by contradiction
qed

You can read this is pseudo-code, but it is machine-checked natural deduction. Note that in the formal language, dependence on some argument is explicit, as in B x, and just A means it cannot depend on hidden variables.

Instead of using that law in the proof, we re-use its proof to make a slightly more general version as follows:

lemma
  assumes *: "(∀x. B x) ⟶ A"
  shows "∃x. (B x ⟶ A)"
proof (rule classical)
  assume **: "¬ (∃x. (B x ⟶ A))"
  have "∀x. B x"
  proof
    fix x show "B x"
    proof (rule classical)
      assume "¬ B x"
      have "B x ⟶ A"
      proof
        assume "B x"
        with `¬ B x` show A ..
      qed
      then have "∃x. (B x ⟶ A)" ..
      with ** show "B x" by contradiction
    qed
  qed
  with * have A ..
  fix a from `A` have "B a ⟶ A" ..
  then show "∃x. (B x ⟶ A)" ..
qed

The other direction is just plain natural deduction, without anything special. There are no classical cases to be considered.

lemma
  assumes *: "∃x. (B x ⟶ A)"
  shows "(∀x. B x) ⟶ A"
proof
  assume **: "∀x. B x"
  from * obtain a where ***: "B a ⟶ A" ..
  from ** have "B a" ..
  with *** show A ..
qed