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:

  1. Tautologies(in the sense of propositional logic);
  2. $∀ 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$);
  3. $∀ x(α→β)→( ∀ x α→∀x β)$;
  4. $α→∀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 ϕ$.

  • 1
    $\begingroup$ Your proof of the $\to$ direction seems off. The assumption (call it P) of your "it suffices to show" implication P -> Q is not known to hold. The logical axiom you quote next would get you from some other thing R to the truth of P, i.e. you have R -> P. Although from R -> P and P -> Q one could derive R -> Q, you cannot use the link P -> Q which you are trying to prove. $\endgroup$ – coffeemath Mar 7 '13 at 11:41
  • $\begingroup$ @coffeemath: Thank you for pointing that out. That's a silly mistake. $\endgroup$ – Metta World Peace Mar 8 '13 at 0:46

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.

  • $\begingroup$ Thank you for your answer.Whenever "take $c$ as such an $x$", do we need to define such $c$? What if $c$ is not definable? $\endgroup$ – Metta World Peace Mar 8 '13 at 0:48
  • $\begingroup$ The way I've seen it used, from $\exists x F(x)$ one can "instantiate" to $F(c)$ for a letter $c$ which has not yet been used in the proof. Then later on if one gets some other property of $c$ shown, say $G(c)$, one can use "existential generalization" to obtain $\exists x G(x).$ $\endgroup$ – coffeemath Mar 8 '13 at 3:34
  • $\begingroup$ It seems to me you're doing witnessing expansion,assigning distinct constant symbols to those formulas with exactly one free variables. Then $\exists x F(x) \to F(c)$ is actually henkin axiom of type one.(Handbook of mathematical logic p29-p30). It makes a lot of sense to me. Thank you. $\endgroup$ – Metta World Peace Mar 8 '13 at 5:21

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


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

  • $\begingroup$ Can you explain to me, how to prove to my the following inconsistency: "$\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)$" $\endgroup$ – thehardyreader Nov 11 '18 at 21:34

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"
    fix x show "B x"
    proof (rule classical)
      assume "¬ B x"
      then have "∃x. ¬ B x" ..
      with ** show "B x" by contradiction
  with * show "∃x. ¬ B x" by contradiction

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:

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

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

  assumes *: "∃x. (B x ⟶ A)"
  shows "(∀x. B x) ⟶ A"
  assume **: "∀x. B x"
  from * obtain a where ***: "B a ⟶ A" ..
  from ** have "B a" ..
  with *** show A ..
  • $\begingroup$ Thank you for your answer. It's really cool, except for a minor problem, some symbols seem not to display properly in your answer. $\endgroup$ – Metta World Peace Mar 10 '13 at 0:29
  • $\begingroup$ This is a direct copy-paste from the Isabelle/jEdit Unicode text view, which means you should normally see it, but you might have to tell the operating system or browser about additional math fonts. The DejaVu or STIX fonts should work, but current OSes have sufficiently many fonts already. $\endgroup$ – Makarius Mar 10 '13 at 11:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.