1
$\begingroup$

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

enter image description here

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!

$\endgroup$
  • 3
    $\begingroup$ $\neg P$ is often defined as $P\Rightarrow\bot$ which is apparently what's going here. $\endgroup$ – Derek Elkins May 16 at 19:17
  • $\begingroup$ @DerekElkins Ah of course, I'd totally forgotten about that. But in that case, how do we even reach bottom from $P(x)$? Thanks. $\endgroup$ – iaskdumbstuff May 16 at 19:20
  • 1
    $\begingroup$ 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? $\endgroup$ – lemontree May 16 at 19:52
  • 1
    $\begingroup$ As for the rest, you'd have to a bit more specific about what else you'd like to have explained. $\endgroup$ – lemontree May 16 at 19:53
  • $\begingroup$ @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! $\endgroup$ – iaskdumbstuff May 16 at 20:13

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.