Prove $\exists_x(\phi(x) \rightarrow \psi) \iff (\forall_x\phi(x) \rightarrow \psi)$ using natural deduction

Question

I want to prove $\exists_x(\phi(x) \rightarrow \psi) \iff (\forall_x\phi(x) \rightarrow \psi)$ where $x \notin FV(\psi)$ using natural deduction method. I was able to prove implication from left to right: $$ {\exists_x(\phi(x) \rightarrow \psi) ~~~~~~~~{{[\phi[t/x]\rightarrow \psi]~~~~~~~ {{[\forall_x\phi(x)]}\over{\phi[t/x]}}} \over {\psi}}}\over{\psi \over {\forall_x\phi(x) \rightarrow \psi}} $$

but I am not able to prove implicatin from right to left. I would appreciate any help.

Answer 1

Arguing informally in natural deduction style, assume as premiss

$\forall x\phi(x) \to \psi$

Now remember that that is elementarily equivalent to

$\neg\forall x\phi(x) \lor \psi$

So the obvious brute force proof strategy is to argue by cases. You need to show, first, that $\neg\forall x\phi(x)$ implies $\exists x(\phi(x) \to \psi)$. But we have

$\neg\forall x\phi(x)\\ \exists x\neg\phi(x)\\ \quad|\quad \neg\phi(a)\\ \quad|\quad \phi(a) \to \psi \\ \quad|\quad \exists x(\phi(x) \to \psi) \\ \exists x(\phi(x) \to \psi) $

using existential quantifier elimination at the key step. And now you need to show that $\psi$ implies $\exists x(\phi(x) \to \psi)$. But that's easy, we just need to fill in the proof

$\psi\\ \phi(a) \to \psi \\ \exists x(\phi(x) \to \psi) $

So put everything together and we are done, in this informal Fitch-style presentation.

It remains to massage the proof into your preferred tree layout: exercise!

Answer 2

Well, $\exists x \phi(x) \rightarrow \psi$ is not logically equivalent to $\forall x \phi(x) \rightarrow \psi$. If every $x$ has some property, certainly there exists an $x$ with that property. However, just because some $x$ has a property does not mean every $x$ has a property.

Unless your domain of discourse has only one element.

Edit: or if $\phi(x)$ is always false.

Answer 3

We have to prove :

$(∀xϕ(x)→ψ) \rightarrow ∃x(ϕ(x)→ψ)$

using Natural Deduction without "abbreviations".

---

Proof :

1) $\phi(x)$ --- assumed [1]

2) $\lnot \phi(x)$ --- assumed [2]

3) $\bot$ --- 1), 2) : $\rightarrow$E

4) $\psi$ --- 3) : $\bot$E

5) $\phi(x) \rightarrow \psi$ --- 1) and 4) : $\rightarrow$I, discharging [1]

6) $\exists x(\phi(x) \rightarrow \psi)$ --- 5) : $\exists$I

7) $\lnot \exists x(\phi(x) \rightarrow \psi)$ --- assumed [3]

8) $\bot$ --- 6), 7) : $\rightarrow$E

9) $\phi(x)$ --- 2), 8) : RAA, discharging [2]

10) $\forall \phi(x)$ --- 9) : $\forall$I

11) $\forall \phi(x) \rightarrow \psi$ --- assumed [4]

12) $\psi$ --- 10), 11) : $\rightarrow$E

13) $\phi(x) \rightarrow \psi$ --- 12) : $\rightarrow$I

14) $\exists x(\phi(x) \rightarrow \psi)$ --- 13) : $\exists$I

15) $\bot$ --- 14), 7) : $\rightarrow$E

16) $\exists x(\phi(x) \rightarrow \psi)$ --- 7), 15) : RAA, discharging [3]

$\vdash (∀xϕ(x)→ψ) \rightarrow \exists x(\phi(x) \rightarrow \psi)$ --- 1), 16) : $\rightarrow$I

---

Notes

A) In the above proof we have only one application of $\forall$I (step 10); in that step, the only undischarged assumption is [3], where $x$ is not free. Thus, contrary to the other "direction", the proviso : $x \notin FV(\psi)$ is not necessary.

B) In the derivation we have used RAA: this use is essential, as shown by the fact that : $(∀xϕ(x)→ψ) \rightarrow ∃x(ϕ(x)→ψ)$ is not intuitionistically valid.