Proof of $\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x (\varphi(x)\rightarrow \psi(x))$ in natural deduction

Question

How to show the following trivial implication with natural deduction?

$\exists x \exists y (\varphi(x)\rightarrow \psi(y)) \rightarrow \exists x (\varphi(x)\rightarrow \psi(x))$

Thx.

Answer 1

Using proof by contradiction:

$$\forall x \colon (\varphi (x) \wedge \neg \psi(x)$$

It follows:

$$\forall x \colon \varphi(x)$$

$$\forall x: \neg \psi(x)$$

Renaming variables:

$$\forall y \colon \neg \psi (y)$$

Using modus tollens:

$$\exists x \colon \neg \varphi(x)$$

This is a contradiction. We're done.

Answer 2

It's a conditional. So the shape of the proof, we know, is going to look like this:

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\ \quad\quad|\quad \ldots\\ \quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\ \quad \exists x \exists y(\phi(x) \to \psi(y)) \to \exists x(\phi(x) \to \psi(x)) $

where we use conditional proof.

If in doubt, a good strategy is to try reductio: and assuming the negation of our target in the subproof is nice as it is equivalent to a universal from which we can extract lots of info. Good! So this should work:

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\ \quad\quad|\quad\quad|\quad \neg\exists x(\phi(x) \to \psi(x))\\ \quad\quad|\quad\quad|\quad \forall x\neg(\phi(x) \to \psi(x))\\ \quad\quad|\quad\quad|\quad \ldots\\ \quad\quad|\quad\quad|\quad \bot\\ \quad\quad|\quad \neg\neg\exists x(\phi(x) \to \psi(x))\\ \quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\ \quad \exists x \exists y(\phi(x) \to \psi(x)) \to \exists x(\phi(x) \to \psi(x)) $

Right! So now we need to use the initial assumption. The only thing we can do with an existential is start off on an existential quantifier elimination proof .... so we know we need to fill in this:

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

Do you see that the initial assumption at line 1, and the sup-proof from lines 4 to 6 entitle to the conclusion at line 7 where we discharge the temporary assumption at line 4? This is an application of existential quantifier elimination.

So how do we get from line 4 to line 6. Drat! Another existential. Same trick, then ...

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\ \quad\quad|\quad\quad|\quad \neg\exists x(\phi(x) \to \psi(x))\\ \quad\quad|\quad\quad|\quad \forall x\neg(\phi(x) \to \psi(x))\\ \quad\quad|\quad\quad|\quad\quad|\quad \exists y(\phi(a) \to \psi(y))\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad (\phi(a) \to \psi(b))\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \ldots\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \bot\\ \quad\quad|\quad\quad|\quad\quad|\quad \bot \\ \quad\quad|\quad\quad|\quad \bot\\ \quad\quad|\quad \neg\neg\exists x(\phi(x) \to \psi(x))\\ \quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\ \quad \exists x \exists y(\phi(x) \to \psi(y)) \to \exists x(\phi(x) \to \psi(x)) $

Now, we haven't used the universal quantifier, and we have two names to instantiate it with. Do it!!

$\quad\quad|\quad \exists x \exists y(\phi(x) \to \psi(y))\\ \quad\quad|\quad\quad|\quad \neg\exists x(\phi(x) \to \psi(x))\\ \quad\quad|\quad\quad|\quad \forall x\neg(\phi(x) \to \psi(x))\\ \quad\quad|\quad\quad|\quad\quad|\quad \exists y(\phi(a) \to \psi(y))\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad (\phi(a) \to \psi(b))\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \neg(\phi(a) \to \psi(a))\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \neg(\phi(b) \to \psi(b))\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \ldots\\ \quad\quad|\quad\quad|\quad\quad|\quad\quad | \quad \bot\\ \quad\quad|\quad\quad|\quad\quad|\quad \bot \\ \quad\quad|\quad\quad|\quad \bot\\ \quad\quad|\quad \neg\neg\exists x(\phi(x) \to \psi(x))\\ \quad\quad|\quad \exists x(\phi(x) \to \psi(x))\\ \quad \exists x \exists y(\phi(x) \to \psi(y)) \to \exists x(\phi(x) \to \psi(x)) $

Ahah! The remaining bit of proof to fill in the dots is just propositional calculus reasoning. Can you do it???

And if you prefer your ND proofs laid out Gentzen style, you'll have to massage this proof idea into a spreading tree.

Answer 3

$$\begin{align} (1) ~ & \exists x \exists y (\phi(x) \rightarrow \psi(y)) && [\text{HYP}] \\ (2) ~ & \neg \exists x (\phi(x) \rightarrow \psi(x)) && [\text{HYP}] \\ (3) ~ & \exists y (\phi(a) \rightarrow \psi(y)) && [\exists\text{-elim}(1)] \\ (4) ~ & \phi(a) \rightarrow \psi(b) && [\exists\text{-elim}(3)] \\ (5) ~ & \forall x \neg (\phi(x) \rightarrow \psi(x)) && [\neg\exists\text{-elim}(2)] \\ (6) ~ & \neg (\phi(a) \rightarrow \psi(a)) && [\forall\text{-elim}(5)] \\ (7) ~ & \neg (\phi(b) \rightarrow \psi(b)) && [\forall\text{-elim}(5)]\\ (8) ~ & \phi(a) \wedge \neg\psi(a) && [\text{DM}(6)] \\ (9) ~ & \phi(b) \wedge \neg\psi(b) && [\text{DM}(7)] \\ (10) ~ & \phi(a) && [\wedge\text{-elim}(8)] \\ (11) ~ & \neg\psi(b) && [\wedge\text{-elim}(9)] \\ (12) ~ & \psi(b) && [\text{MP}(4,10)] \\ (13) ~ & \exists x (\phi(x) \rightarrow \psi(x)) && [\text{RAA}(2,11,12)] \\ (14) ~ & \exists x \exists y(\phi(x) \rightarrow \psi(y)) \rightarrow \exists x(\phi(x) \rightarrow \psi(x)) && [\rightarrow\text{-intro}(1,13)] \end{align}$$

Answer 4

To prove ∃x∃y[φ(x)→ψ(y)]→∃x[φ(x)→ψ(x)]:

  01. ∃x∃y[φ(x)→ψ(y)]         assumption
    02. ∃y[φ(a)→ψ(y)]         assumption, a
      03. φ(a)→ψ(b)           assumption, a, b
        04. ¬φ(a)             assumption, a, b
          05. φ(a)            assumption, a, b
          06. ⊥               contradiction 05 04
          07. ψ(a)            explosion 06
        08. φ(a)→ψ(a)         →intro 05-07
        09. ∃x[φ(x)→ψ(x)]     ∃intro 08
      10. ¬φ(a)→∃x[φ(x)→ψ(x)] →intro 04-09
        11. φ(a)              assumption, a, b
          12. φ(b)            assumption, a, b
          13. ψ(b)            MP 03 11
        14. φ(b)→ψ(b)         →intro 12-13
        15. ∃x[φ(x)→ψ(x)]     ∃intro 14
      16. φ(a)→∃x[φ(x)→ψ(x)]  →intro 11-15
      17. φ(a)∨¬φ(a)          LEM                 *non-intuitionistic!
      18. ∃x[φ(x)→ψ(x)]       ∨elim 17 16 10
    19. ∃x[φ(x)→ψ(x)]         ∃elim 02 03-18
  20. ∃x[φ(x)→ψ(x)]           ∃elim 01 02-19
21. [∃x∃y[φ(x)→ψ(y)]]→[∃x[φ(x)→ψ(x)]] →intro 01-20

---

This does not hold in intuitionistic logic. Consider the Kripke frame $W=\{1\longleftarrow0\longrightarrow2\}$ with domain $\{a,b\}$, and the following facts known:

• In World $0$, there is nothing known.
• In World $1$, only $\varphi(a)$ and $\psi(b)$ are known.
• In World $2$, only $\varphi(b)$ is known.

Then, in World $0$, letting $x=a$ and $y=b$, we see that $\varphi(a) \to \psi(b)$ in every reachable world, thus the antecedent is confirmed. However, the consequent is false: if $x=a$, then in world $1$ we have $\varphi(a)$ but not $\psi(a)$; if $x=b$ in world $2$ we have $\varphi(b)$ but not $\psi(b)$.