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


  • 1
    $\begingroup$ As you can see, MathJax works in titles, too. In the future, please use it to make the titles of your questions more informative (by including the specific formula whose proof in ND you're after). $\endgroup$
    – Lord_Farin
    Nov 19 '13 at 17:49
  • $\begingroup$ Thx for the remark, I'll do so in future. $\endgroup$ Nov 19 '13 at 21:18
  • $\begingroup$ Mmmm, not exactly trivial -- and nasty to prove in some standard ND systems (I can imagine having used it as a rather evil exam question to sort out those who'd really got the hang of proof-building in ND). $\endgroup$ Nov 19 '13 at 23:48

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.

  • $\begingroup$ You've proved the wrong thing. It says $\exists x (\phi (x) \rightarrow \psi(x))$ $\endgroup$ Nov 20 '13 at 8:19
  • $\begingroup$ Oops many thanks for spotting the typo which propagated by cutting and pasting. Now corrected. $\endgroup$ Nov 20 '13 at 16:11
  • $\begingroup$ I learned the followong $\exists$-elimination rule: $\exists x\varphi(x)$ and a derivation (with assumption $\varphi$) of $\psi$ given we can derive $\psi$ and cancel $\varphi$. But we have the following conditions: $x$ is not free in $\psi$ and $x$ is also not free in any assumption of the subderivation of $\psi$ other than $\varphi$. I don't see how this coincides with the $\exists$-elimination you performed. $\endgroup$ Nov 20 '13 at 17:18
  • $\begingroup$ @Naturaldeduction I've used different letters $a$, $b$, for parameters rather than put $x$, $y$ to a double use as bound variables and parameters. Which is entirely traditional (see Gentzen and Prawitz, for example), and I'd say is much to be preferred. $\endgroup$ Nov 20 '13 at 17:34
  • 1
    $\begingroup$ @Naturaldeduction The (first relevant) temporary hyp is $\exists y(\phi(a) \to \psi(y))$, and the conclusion of that subproof is $\bot$. So $a$ doesn't occur in the conclusion $\bot$ or in any premiss on which that $\bot$ depends other than $\exists y(\phi(a) \to \psi(y))$. So the restrictions you mention a version of are obeyed. $\endgroup$ Nov 20 '13 at 19:26

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


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.

  • $\begingroup$ This is not natural deduction. $\endgroup$
    – Kasper
    Nov 19 '13 at 18:57
  • $\begingroup$ Which rules did you use for these transformations? For example the first thing you did looks like an $\land$-elimination. But in fact it isn't since the outer connective is no $\land$ but an $\forall$. Don't we need a $\forall$-elimination first? Also the renaming part is no ND rule I know. $\endgroup$ Nov 19 '13 at 21:24

$$\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}$$

  • $\begingroup$ Lines 3 and 4 are not legitimate applications of E elimi in any standard system. $\endgroup$ Nov 20 '13 at 6:43
  • $\begingroup$ Really? It looks standard to me. I instantiated the existentially quantified formula in line (1) with fresh variables, and concluded with one in which those variables don't occur. $\endgroup$
    – danportin
    Nov 20 '13 at 7:20
  • $\begingroup$ The instantiation is, in your terms, a new HYP, which later needs to be discharged by E eliminate. $\endgroup$ Nov 20 '13 at 8:04
  • $\begingroup$ I thought it was implied that a subderivation was being produced and the instantiated formula subsequently discharged. At least, that's how I learned to write these proofs. I'll keep your comment in mind for later, though. Thanks for the correction. $\endgroup$
    – danportin
    Nov 20 '13 at 9:13
  • $\begingroup$ I'm using the text book Logic and Structure from Van Dalen. There is no such thing like $\neg\exists$-elimination. $\endgroup$ Nov 20 '13 at 15:48

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.