Prove $\neg A \wedge \neg B$ using the following rules S1: $A \leftrightarrow(B\vee E)$
S2: $E \rightarrow D$
S3: $C \wedge F \rightarrow \neg B$
S4: $E \rightarrow B$
S5: $B \rightarrow F$
S6: $B \rightarrow C$
I'm not quite sure how logical proofs like this work. If we have $\neg A \wedge \neg B$, do we have to prove both sides of the conjunction? If so, what rule allows us to bring them together?
 A: Consider a proof by contradiction. Suppose instead that $\neg(\neg A \land \neg B)$ is true so that by DeMorgan's Law, we have that $A \lor B$ is true. Then we claim that $B$ is true. To see this, there are $2$ cases to consider:


*

*Case 1: Suppose that $A$ is true. Then by S1 we know that $B \lor E$ is true. Now there are $2$ cases to consider:


*

*Case 1.1: Suppose that $B$ is true. Then we're immediately done.

*Case 1.2: Suppose that $E$ is true. Then by S4 and Modus Ponens, we know that $B$ is true, so we're done.


*Case 2: Suppose that $B$ is true. Then we're immediately done.

Having established that $B$ is true, notice that by S6 and S5 and Modus Ponens, we know that both $C$ and $F$ is true so that $C \land F$ is true. But then by S3 and Modus Ponens, we know that $\neg B$ is true. But this contradicts the fact that $B$ is true. So we conclude that $\neg A \land \neg B$, as desired.
A: First, by looking at the given propositions S1-S6 we see that they do not immediately show us how to derive $\neg A \wedge \neg B$ by the so-called conjunction introduction inference rule. However, if we observe that

$\neg A \wedge \neg B \equiv \neg (A \vee B)$

we can prove the equivalent negated statement instead.
Since it has the form of a negation, in order to prove it, we assume it as given and then derive a contradiction. With this we are able to conclude that the negation holds. This inference rule is known as negation introduction.
Now, suppose $A \vee B$. How do you derive a contradiction?
We observe that $B$ implies $\neg B$ (see S3,S5,S6), and that $A$ implies $B$ (that implies $\neg B$). Can you continue from here?
A: Here is a proof using a Fitch-style proof checker:


Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/
