1
$\begingroup$

I have the following proof so far:

proof

In step 9 I'm not sure how to prove P from the steps I have before. I thought that I could use ∨ Elim but I don't think I can now.

$\endgroup$
  • 2
    $\begingroup$ $(B\lor P)\equiv (\lnot(\lnot B\land\lnot P))\equiv(\lnot B\implies P)$ $\endgroup$ – trying Aug 8 '17 at 7:52
  • $\begingroup$ @trying The first $\equiv$ isn't constructively valid from left to right. $\endgroup$ – DanielV Aug 8 '17 at 8:16
  • $\begingroup$ @DanielV He is using DeMorgan's Law and the definition of implication. How is that invalid? $\endgroup$ – Dan Christensen Aug 8 '17 at 14:44
  • $\begingroup$ @DanChristensen Many classical laws aren't constructive. For DeMorgan's, $\lnot (\lnot A \lor \lnot B) \to (A \lor B)$, just take $B = \lnot A$ and you get $\lnot \lnot A \to A$, double negation elimination which is not taken for granted. $\endgroup$ – DanielV Aug 8 '17 at 14:58
  • $\begingroup$ @DanielV So, it is valid in what you call "classical" logic. Thanks. $\endgroup$ – Dan Christensen Aug 8 '17 at 16:57
1
$\begingroup$

The trick is to use $\bot \ Elim$. Now, to continue from what you have, you can do:

enter image description here

But note that you never used the subproof on lines 5-7, so this can be simplified to:

enter image description here

Although conceptually, it may be helpful to keep the original subproof, and (since it shows that $B$ leads to a contradiction $\bot$) derive $\neg B$, and to then combine $\neg B$ with $B \lor P$ (the latter is a super common patterns, so remember that one!!):

enter image description here

Finally, you can set this up as a proof by cases within a conditional proof, i.e. derive your goal $P \land D$ from each of the cases $B$ and $P$:

enter image description here

$\endgroup$
0
$\begingroup$

I've actually seen some texts define Or-Elimination as $$\frac{\lnot B,~ B \lor P}{P}$$ which is actually constructively valid. Anyway, the way to get there from regular Or-Elimination (proof by cases) is just to show that in both cases of $B$ and case $P$ that $P$ follows:

$$\begin{array} {rll} (1) & \lnot B & \text{Given} \\ \\ % (2) & \quad B & \text{assumption, Case 1} \\ % (3) & \quad \bot & \text{Contradiction} \\ % (4) & \quad P & \text{Explosion} \\ \\ % (5) & \quad P & \text{assumption, Case 2} \\ \\ % (6) & B \lor P & \text{Given} \\ % (7) & P & \text{Proof by cases (Or Elim) of 6, 2 through 4, 5 through 5} \\ % \end{array}$$

$\endgroup$

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.