Proving Sequent Calculus Statement I have to prove the sequent
$$\vdash (\lnot A \lor \lnot B) \to \lnot (A \land B)$$
using the inference rules for natural deduction listed here (pp. 7-8).
I'm super new to natural deduction and sequent calculus. I've attached my work so far below. We need to prove the statement at the bottom, and we're basically working backwards. Honestly, I have no idea

*

*what the next step is, or

*how to know when I'm done.

The last step I did was Not Introduction, but that's kinda just because I didn't see any other rule that matched the form of $\Gamma \vdash \lnot P$. Again, complete newbie to this, really don't know what I'm doing or why. I've tried searching things and can understand some simpler formulas (like, just implications and conjunctions/disjunctions), but I don't know how to handle Not.

 A: What you did so far goes in the right direction. Now, how to prove the sequent $\lnot A \lor \lnot B, \, A \land B \vdash  \bot $ where you get stuck?
Let us first consider the problem from an informal point of view. Proving the sequent $\lnot A \lor \lnot B, \, A \land B \vdash  \bot $ intuitively means that a contradiction must emerge from the assumptions $\lnot A \lor \lnot B$ and $A \land B$, using the inference rules of natural deduction listed here (pp. 7-8). This is where the rule $\lor_\mathrm{elim}$ plays a crucial role. From the assumption $\lnot A \lor \lnot B$, it follows that there are two cases:

*

*either $\lnot A$ holds, but this is in contradiction with the fact $A$ holds ($A$ is derived from the assumption $A \land B$),


*or $\lnot B$ holds, but this is in contradiction with the fact $B$ holds (again, $B$ is derived from the assumption $A \land B$).
In both cases, we have the contradiction we are looking for.
Formally, a rigorous derivation in natural deduction using the inference rules listed here (pp. 7-8) is below.
For the sake of readability, I split the derivation in three parts.
The first one below is the "bottom" part of the derivation. You have to imagine that the derivation $\Pi_A$ is above the sequent $\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash \bot$, and that the derivation $\Pi_B$ is above the sequent $\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash \bot$.
\begin{align}
  \dfrac
  {\overline{\lnot A \!\lor\! \lnot B, A \!\land\! B \vdash \lnot A \!\lor\! \lnot B}^\mathrm{hyp} 
   \
   \overset{\Pi_A}{\lnot A \!\lor\! \lnot B,  A \!\land\! B, \lnot A \vdash \!\bot} 
   \ \ \
   \overset{\Pi_B}{\lnot A \!\lor\! \lnot B,  A \!\land\! B, \lnot B \vdash \!\bot}}
  {\dfrac
   {\lnot A \lor \lnot B, \, A \land B \vdash \bot}
   {\dfrac
    {\lnot A \lor \lnot B \vdash \lnot (A \land B)}
    {\vdash (\lnot A \lor \lnot B) \to \lnot (A \land B)}
    \to_\mathrm{intro}
   }
   \lnot_\mathrm{intro}
  }\!
  \lor_\mathrm{elim}
\end{align}
where
\begin{align}
\Pi_A = \
\dfrac
{\dfrac{}{\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash \lnot A}^\mathrm{hyp} 
 \quad 
 \dfrac
 {\overline{\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash A \land B}^\mathrm{hyp}}
 {\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash A}
 \land_\mathrm{elim}
}
{\lnot A \lor \lnot B, \, A \land B, \, \lnot A \vdash \bot}
\lnot_\mathrm{elim}
\end{align}
and
\begin{align}
\Pi_B = \
\dfrac
{\dfrac{}{\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash \lnot B}^\mathrm{hyp} 
 \quad 
 \dfrac
 {\overline{\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash A \land B}^\mathrm{hyp}}
 {\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash B}
 \land_\mathrm{elim}
}
{\lnot A \lor \lnot B, \, A \land B, \, \lnot B \vdash \bot}~\lnot_\mathrm{elim}
\end{align}
