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

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

-
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. –  coffeemath Mar 7 at 11:41
@coffeemath: Thank you for pointing that out. That's a silly mistake. –  Metta World Peace Mar 8 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.

-
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? –  Metta World Peace Mar 8 at 0:48
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).$ –  coffeemath Mar 8 at 3:34
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. –  Metta World Peace Mar 8 at 5:21

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

-
Thank you for your answer. It's really cool, except for a minor problem, some symbols seem not to display properly in your answer. –  Metta World Peace Mar 10 at 0:29
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. –  Makarius Mar 10 at 11:36