# Using natural deduction to prove that $\forall x \lnot (P(x) \lor R(x)) \implies \exists x(\lnot P(x) \lor \lnot R(x))$

Not only do I not understand how to do this, but I don't comprehend the solution:

Here, supposons means assume, and donc means thus.

I'm specifically confused with line 5, for which I don't understand the rule $$\implies E 2,3$$ in the slightest; the lines it is referring to are not even implications! Any help would be appreciated, thanks!

• $\neg P$ is often defined as $P\Rightarrow\bot$ which is apparently what's going here. – Derek Elkins May 16 at 19:17
• @DerekElkins Ah of course, I'd totally forgotten about that. But in that case, how do we even reach bottom from $P(x)$? Thanks. – iaskdumbstuff May 16 at 19:20
• Line 5 cites $\to E 2,4$, not $\to E 2,3$ (as you wrote). So $\to E$ is done on l. 2 $\neg (P(x) \lor R(x)) \equiv (P(x) \lor R(x)) \to \bot$ and l.4 $(P(x) \lor R(x))$ to derive $\bot$. Does this resolve your confusion? – lemontree May 16 at 19:52
• As for the rest, you'd have to a bit more specific about what else you'd like to have explained. – lemontree May 16 at 19:53
• @lemontree Of course! I'm so dumb; the answer to both of my questions was that a negation can be described as an implication of bottom. That clears everything for me, the rest I understand. Thanks very much to the both of you! – iaskdumbstuff May 16 at 20:13