# A simple problem involving natural deduction - so what am I doing wrong?

The problem is straight-forward. I'm supposed to derive the following in propositional logic, using natural deduction:

$$\lnot (A \wedge B) \vdash \lnot A \vee \lnot B$$

Here is my initial attempt at a derivation, using a tree structure:

$$\dfrac{\dfrac{\dfrac{\lnot (A \wedge B) = (A \wedge B) \rightarrow \bot \qquad (A \wedge B)}{\bot}\small{\rightarrow E}}{\lnot A}\small{RAA}}{\lnot A \vee \lnot B}\small{\vee I}$$

When I arrive at the top-line, I realize that the only way (?) for me to construct $$(A \wedge B)$$ is to use and-introduction. If I assume $$A$$ above this line, the noted $$RAA$$ discharges this particular assumption. However, I'm not quite sure how to handle $$B$$ in this instance. Have I worked myself into a corner here? Is there a better way to do this? Any feedback would be greatly appreciated!

• It is or-intro., but you need to write it out. Rather than introducing neg-B directly, reintroduce the given $\neg (A\land B)$ after deriving $\neg A$. Then repeat the analysis to obtain $\neg A$ and $\neg B$ in the same line. Then or-introduction and you're done. You are allowed to repeat given information. Apr 2, 2022 at 21:05
• You have to assume $\lnot (\lnot A \lor \lnot B)$ as well as A and B Apr 3, 2022 at 8:11
• I'm quite sure that you can find the full derivation in this site... Apr 3, 2022 at 8:13
• @M.Reeves When you say "repeat the analysis", exactly what are you referring to? Could you perhaps be more specific? I realize it might be difficult without giving away the answer completely... Apr 3, 2022 at 19:11
• I don't understand your notation, but you can just apply the definition of $\lor$ and remove the resulting double negation to get the required result. Apr 5, 2022 at 15:55

So far, so good. But first, you want to assume $$A$$ and $$B$$ seperately, so that they are the assumptions you discharge, not $$A\land B$$.
Add an assumption of $$\lnot(\lnot A\lor\lnot B)$$ and you can derive another contradiction to discharge the assumed $$B$$ in exactly the way you did with the assumed $$A$$. $$\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\dfrac{\neg(A\land B)}{(A\land B)\to\bot}{\small\textsf{def }\lnot}\quad \dfrac{[A]^1\quad[B]^2}{A\land B}{\small\land\mathsf I}}{\bot}{\small{\to}\mathsf E}}{\lnot A}{\small\lnot\mathsf I^1}}{\lnot A\lor \lnot B}{\small\lor\mathsf I}\quad\lower{1ex}{\lnot(\lnot A\lor\lnot B)}}{\bot}}{\lnot B}{\small\lnot\mathsf I^2}}{\vdots}$$
Note: These are not RAA, but Indirect Proof $$IP$$ also know as Negation Introduction ($$\lnot\mathsf I$$). You assume a proposition, derive a contradiction, therefore discharge to deduce the negation of the proposition. Your proof system might also be using conditional introduction and negation's definition to implement this (as they do with negation elimination).
$$\dfrac{\dfrac{\dfrac{\lower{5ex}\vdots\quad{[A]^1\\~~~\vdots}}{\bot}}{A\to\bot}{\small{\to}\mathsf I^1}}{\lnot A}{\small\text{def }\lnot}$$