# Prove P from B ∨ P when we have proven ¬B

I have the following proof so far:

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.

• $(B\lor P)\equiv (\lnot(\lnot B\land\lnot P))\equiv(\lnot B\implies P)$ – trying Aug 8 '17 at 7:52
• @trying The first $\equiv$ isn't constructively valid from left to right. – DanielV Aug 8 '17 at 8:16
• @DanielV He is using DeMorgan's Law and the definition of implication. How is that invalid? – Dan Christensen Aug 8 '17 at 14:44
• @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. – DanielV Aug 8 '17 at 14:58
• @DanielV So, it is valid in what you call "classical" logic. Thanks. – Dan Christensen Aug 8 '17 at 16:57

The trick is to use $\bot \ Elim$. Now, to continue from what you have, you can do:
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!!):
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$:
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}$$