Proving $\vdash \exists x(P(x)\lor Q(x))\Leftrightarrow \exists xP(x)\lor \exists xQ(x) $ using natural deduction, forward direction attempt.

Question

$$ \vdash \exists x(P(x)\lor Q(x))\Leftrightarrow \exists xP(x)\lor \exists xQ(x) $$

I'm unsure about a step in my (forward direction) attempt in solving this using natural deduction proof:

Forward direction:

1.* $\exists x(P(x)\lor Q(x))$ (Assumption)

2.* $P(c)\lor Q(c)$ ($\exists$-elim 1)

3.** $\lnot Q(c)$ (Assumption)

4.** $P(c)$ ($\lor$-elim 2,3)

5.** $\exists x(P(x))$ ($\exists$-intro 4)

6.** $\exists xP(x)\lor \exists xQ(x)$ ($\lor$-intro 5)

By ($\Rightarrow$- elimination 1,6) can I deduce:

7. $\exists x(P(x)\lor Q(x))\Rightarrow \exists xP(x)\lor \exists xQ(x)$?

Thanks in advance!

Answer 1

This is very close! You showed that assuming $\exists x(P(x)\vee Q(x))$ and $\neg Q(c)$ that $\exists x P(x) \vee \exists x Q(x)$ . Notice how this uses the extra assumption that $\neg Q(c)$ is true. We can mimic a standard proof by cases here: you have already dealt with the case that $\neg Q(c)$ implies your desired conclusion, now we need to show that if we assume $Q(c)$ then your conclusion is true as well. This isn't too hard; you can just use $\exists$-intro and $\vee$-intro like you did in the other case. I'm not sure which rules your deductive system allows, but there is definitely a way to formalize a proof by cases, and this would complete your argument!

Answer 2

You didn't eliminate an implication symbol, you introduced it instead. So it would probably be better to say that you used (⇒intro) for it. Assuming $P$ and getting $Q$ allows you to write $P \Rightarrow Q$ outside the context of $P$.

Also, it seems like the (∨elim) rule in the system you use refers to disjunctive syllogism, or $(A \lor B) \land \lnot A \Rightarrow B$. It certainly eliminates a disjunction symbol, but the (∨elim) that I know of refers to deriving $C$ from $A \lor B, A \Rightarrow C, B \Rightarrow C$. As long as the system has this rule but probably with another name, you can prove the desired conclusion. This is what Brian refers to proof by cases.

---

By the way, if you're doing a proof by cases there, you don't need to assume $\lnot Q(c)$ to get $P(c)$. Just assume $P(c)$ directly.

In summary, you would do something like this. (Note: Placed in a spoiler block to show you the outline only if you want to.) $\def\block#1{\begin{array}{ll}\ &{#1}\end{array}} \def\fitch#1#2{\begin{array}{|l}#1\\\hline#2\end{array}} \def\sub#1#2{\text{#1}:\\\block{#2}}$

$$\fitch{\exists x (P(x) \lor Q(x))}{P(c) \lor Q(c). \\ \fitch{P(c)}{\exists x(P(x)) \\ \exists x(P(x)) \lor \exists x(Q(x))} \\ \fitch{Q(c)}{\exists x(Q(x)) \\ \exists x(P(x)) \lor \exists x(Q(x))} \\ \exists x(P(x)) \lor \exists x(Q(x))}$$

Answer 3

The suggestions provided by soupless and Brian are correct, however, the deductive system I'm using does not allow the $\lor$-elim they provided, nor the proof by cases. I'm now aware that I should have mentioned the rules my deductive system allows.

For ($\lor$-elim), I'm using the disjunctive syllogism $(A\lor B)\land \lnot A \Rightarrow B$ .

This is how I proceeded to solve the question (forward direction):

1.* $\exists x(P(x)\lor Q(x))$ (Assumption)

2.* $P(c)\lor Q(c)$ ($\exists$-elim 1)

3.** $\lnot (\exists x P(x) \lor \exists x Q(x))$ (Assumption)

4.*** $\lnot Q(c)$ (Assumption)

5.*** $P(c)$ ($\lor$-elim 2,4)

6.*** $\exists x(P(x))$ ($\exists$-intro 5)

7.*** $\exists xP(x)\lor \exists xQ(x)$ ($\lor$-intro 6)

8.*** $\lnot (\exists xP(x) \lor \exists x Q(x)) \land (\exists xP(x)\lor \exists xQ(x))$ ($\land$-intro 3,7)

9.** $ \lnot \lnot Q(c)$ ($\lnot$-intro 4,8)

10.** $Q(c)$ ($\lnot$-elim 9)

11.** $\exists xQ(x)$ ($\exists$-intro 10)

12.** $ \exists x P(x) \lor \exists x Q(x)$ ($\lor$-intro 11)

13.** $\lnot (\exists x P(x) \lor \exists x Q(x)) \land (\exists x P(x) \lor \exists x Q(x))$ ($\land$-intro 3,12)

14.* $\lnot \lnot (\exists x P(x) \lor \exists x Q(x))$ ($\lnot$-intro 3,13)

15.* $\exists x P(x) \lor \exists x Q(x)$ ($\lnot$-elim 14)

16.$\exists x(P(x)\lor Q(x)) \Rightarrow (\exists x P(x) \lor \exists x Q(x)) $ ($\Rightarrow$-intro 1,15)