2
$\begingroup$

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!

$\endgroup$
5
  • $\begingroup$ 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. $\endgroup$
    – C. Ventin
    Apr 2, 2022 at 21:05
  • 1
    $\begingroup$ You have to assume $\lnot (\lnot A \lor \lnot B)$ as well as A and B $\endgroup$ Apr 3, 2022 at 8:11
  • $\begingroup$ I'm quite sure that you can find the full derivation in this site... $\endgroup$ Apr 3, 2022 at 8:13
  • $\begingroup$ @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... $\endgroup$
    – Azkar
    Apr 3, 2022 at 19:11
  • $\begingroup$ 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. $\endgroup$ Apr 5, 2022 at 15:55

1 Answer 1

2
$\begingroup$

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}$$

Reduction to Absurdity is where you assume a negation of a proposition, derive a condition, and therefore discharge to deduce the proposition.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .