# 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}$$
The text passage is a discussion about a logical proof, specifically about proving a statement P from B ∨ P given ¬B. It includes a question about how to proceed with the proof and suggestions from other users on how to complete it.
no_question

the passage does not contain a direct mathematical question that requires a numerical or calculative answer. instead, it is a discussion about a logical proof and how to proceed with it. the question is more about the method of proof rather than a mathematical calculation or word problem.
Given a text passage, determine:
    1. If it contains a mathematical question (including word problems or calculations)
    2. If an answer to that mathematical question is provided in the text

First, describe the content structure you found in 1-2 sentences.

Then provide your analysis in the following format:
TYPE: <one of the following values>
- NO_QUESTION
- SINGLE_QUESTION
- SINGLE_QUESTION_WITH_ANSWER
- MULTIPLE_QUESTIONS
- MULTIPLE_QUESTIONS_WITH_ANSWERS
system
# 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}$$
user
The text passage is a discussion about a logical proof, specifically about proving a statement P from B ∨ P given ¬B. It includes a question about how to proceed with the proof and suggestions from other users on how to complete it.

TYPE: NO_QUESTION

The passage does not contain a direct mathematical question that requires a numerical or calculative answer. Instead, it is a discussion about a logical proof and how to proceed with it. The question is more about the method of proof rather than a mathematical calculation or word problem.