Is law of excluded middle necessary in this proof?

Question

I'm currently learning natural deduction and here is my question.

Is it possible to prove this
$\vdash \neg(P \land Q)\rightarrow (\neg P \lor \neg Q)$
without referring to the law of excluded middle ?

More precisely, using only the following set of inference rules. These rules are being introduced in the book logic: the laws of truth Page 410.
I assume these rules are complete and have tried a long time , however, still cannot come up with a correct derivation without referring to the law of excluded middle which is not included in the following rules.

Answer 1

There is already a good answer about how the implication can be achieved with the rules you gave. This answer is for the initial question about the link to the law of excluded middle.

---

The implication in the question is exactly the part of De Morgan's laws that does not hold in intuitionistic logic, see also this question.

If the implication were to hold, then we would clearly have that a weaker version of the law of the excluded middle is true: $\neg P \vee \neg \neg P$. To see this, simply substitute $\neg P$ for $Q$ and note that $\neg (P \wedge \neg P)$ is trivially true.

The weak law of excluded middle is actually exactly what we would need to prove the implication from the question. That is, we do not need the full law of excluded middle, just $\neg P \vee \neg \neg P$. In particular the implication from the question is equivalent to the weak law of excluded middle. I will give a written proof, if you want you can try to formalise it in a deduction-system.

We assume $\neg (P \wedge Q)$ and also $\neg P \vee \neg \neg P$ and $\neg Q \vee \neg \neg Q$. So we can perform a proof by cases:

1. If we have $\neg P$ or we have $\neg Q$, then we directly get $\neg P \vee \neg Q$.
2. If we have $\neg \neg P$ and $\neg \neg Q$, then we have $\neg \neg P \wedge \neg \neg Q$. This is equivalent to $\neg \neg (P \wedge Q)$. So we get a contradiction with $\neg (P \wedge Q)$, and our result follows from the principle of explosion.

Answer 2

As I already commented on the original post, the (misleadingly named) $\neg$-elimination rule of the calculus is really the rule of proof by contradiction, which is equivalent to the double-negation elimination rule $\neg\neg\alpha\vdash\alpha$, and implies the law of excluded middle $\vdash\alpha\lor\neg\alpha$.

Try to assume $\neg(P\land Q)$ and $\neg(\neg P\lor\neg Q)$, and derive a contradiction. (The most direct way is probably to derive $P\land Q$ from $\neg(\neg P\lor\neg Q)$.) Then infer $\neg P\lor\neg Q$ by the $\neg$-elimination rule, and $\neg(P\land Q)\to\neg P\lor\neg Q$ by the $\to$-introduction rule.

Answer 3

Good answers, here. FWIW, here is a possible proof using Fitch-style natural deduction system and the rules present in the book "Logic: The Laws of Truth".

$ \def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}} \def\Ae#1{\qquad\mathbf{\forall E} \: #1 \\} \def\Ai#1{\qquad\mathbf{\forall I} \: #1 \\} \def\Ee#1{\qquad\mathbf{\exists E} \: #1 \\} \def\Ei#1{\qquad\mathbf{\exists I} \: #1 \\} \def\R#1{\qquad #1\,(\mathbf{RI}) \\} \def\ci#1{\qquad #1\,(\mathbf{\land I})\\} \def\ce#1{\qquad\mathbf{\land E} \: #1 \\} \def\oi#1{\qquad #1\,(\mathbf{\lor I}) \\} \def\oe#1{\qquad\mathbf{\lor E} \: #1 \\} \def\ii#1{\qquad\mathbf{\to I} \: #1 \\} \def\ie#1{\qquad\mathbf{\to E} \: #1 \\} \def\be#1{\qquad\mathbf{\leftrightarrow E} \: #1 \\} \def\bi#1{\qquad #1\,(\mathbf{\leftrightarrow I})\\} \def\qi#1{\qquad\mathbf{=I}\\} \def\qe#1{\qquad\mathbf{=E} \: #1 \\} \def\ne#1{\qquad #1\,(\mathbf{\lnot E})\\} \def\ni#1{\qquad #1\,(\mathbf{\lnot I})\\} \def\IP#1{\qquad\mathbf{IP} \: #1 \\} \def\x#1{\qquad\mathbf{X} \: #1 \\} \def\DNE#1{\qquad\mathbf{DNE} \: #1 \\} $

$ \fitch{}{ \fitch{1.\,\lnot(P \land Q)}{ \fitch{2.\,\lnot(\lnot P \lor \lnot Q)}{ \fitch{3.\,P}{ \fitch{4.\,Q}{ 5.\,P \land Q \ci{3,4} 6.\,\lnot(P \land Q) \R{1} }\\ 7.\,\lnot Q \ni{4-6} 8.\,\lnot P \lor \lnot Q \oi{7} 9.\,\lnot(\lnot P \lor \lnot Q) \R{2} }\\ 10.\,\lnot P \ni{3-9} 11.\,\lnot P \lor \lnot Q \oi{10} 12.\,\lnot(\lnot P \lor \lnot Q) \R{2} }\\ 13.\,\lnot P \lor \lnot Q \ne{2-12} }\\ 14.\,\lnot(P \land Q) \to (\lnot P \lor \lnot Q) \ii{1-13} } $

Answer 4

Using those rules, no proof needs to refer to the Law of the Excluded Middle.

Rather, any use of LEM and disjunction elimination can be rewritten to use reiteration, negation introduction, and negation elimination instead.

$$\def\fitch#1#2{~~\begin{array}{|l|}\hline #1\\\hline #2\\\hline\end{array}}{{\fitch{\qquad}{\alpha\vee\neg \alpha\\\fitch{~~\alpha\qquad}{~~\vdots\\~~\beta}\\\fitch{\neg \alpha\qquad}{~~\vdots\\~~\beta}\\~~\beta\qquad\vee\textsf{E}}}{\quad{\iff}\quad}{\fitch{}{\fitch{\neg\beta}{\fitch{~~\alpha}{~~\vdots\\~~\beta\\\neg\beta\quad\textsf{R}}\\\neg\alpha\qquad\neg\textsf{I}\\~~\vdots\\~~\beta\\\neg \beta\qquad\textsf{R}}\\~~\beta\qquad\quad\neg\textsf{E}}}}$$

---

Remark: However, $\neg(P\to Q)\to(\neg P\vee\neg Q)$ is not valid in intuitionistic logic. Negation elimination of this system (a.k.a. Proof by Contradiction) is exactly as non-intuitionistic as LEM.