How to prove the theorem (¬P ∨ ¬Q) ↔ ¬(P ∧ Q)? How do I prove this theorem? So far what I have is: I create a subproof for proving (¬P ∨ ¬Q)→¬(P ∧ Q)
And the idea is that I am trying to prove ~(P ^ Q) -> (~P v ~Q) so that I can use the biconditional rule to end up with (¬P ∨ ¬Q) ↔ ¬(P ∧ Q). However, I am stuck on this and I do not know how to start this other than maybe starting with another subproof startinga s ~(P ^ Q) but then I am stuck there again. Or maybe I started wrong.
 A: Build the proof from the bottom up:$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}$
$$\fitch{}{\fitch{\neg(P \wedge Q)}{\fitch{\neg(\neg P\vee\neg Q)}{~\vdots\\P\\~\vdots\\Q\\P\wedge Q\hspace{15.5ex}\textsf{Conjunction Introduction}\\\bot\hspace{20ex}\textsf{Negation Elimination}}\\\neg\neg(\neg P\vee \neg Q)\hspace{11ex}\textsf{Negation Elimination}\\\neg P\vee \neg Q\hspace{16ex}\textsf{Double Negation Elimination}}\\ \neg(P \wedge Q) \to (\neg P \vee \neg Q)\hspace{4ex}\textsf{Conditional Introduction}}$$
I'm sure you can fill in the remaining dots.
A: How does your proof system handle excluded-middle? (De-Morgan's law is equivalent to weak excluded-middle, so you need at least some handling of that issue in your system to make it work, and I'm guessing that most proof systems we'd encounter like this will allow excluded middle outright.)
Once you have excluded middle, you can construct a proof that goes like:

*

*$\neg (P \wedge Q)$ (Assumption)

*$P \vee \neg P$ (Excluded Middle)

(Subproof 1, from $\neg P$)



*$\neg P$ (Assumption)

*$\neg P \vee \neg Q$ ($\vee$-introduction, from 3)


(Subproof 2, from $P$)



*$P$ (Assumption)

*$Q$ (Assumption)

*$P \wedge Q$ ($\wedge$-introduction, from 5 and 6)

*$\bot$ (From 1 and 7)

*$\neg Q$ (By contradiction, discharging assumption 6)

*$\neg P \vee \neg Q$ ($\vee$-introduction, from 9)




*$\neg P \vee \neg Q$ (Proof by cases, using 2 and both subproofs)

*$\neg (P \wedge Q) \implies (\neg P \vee \neg Q)$ (Deduction rule, discharging assumption 1)

You'll need to rework this proof depending on how your system does proof by cases, but structurally it will be equivalent to the above.
