Is law of excluded middle necessary in this proof?

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.

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.


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

Tags:

Logic

Proof Theory

Natural Deduction

Propositional Calculus

Related

volume of tilted ellipsoid How to calculate $ \left| \sin x \right| $ derivative in a more elegant way? If $\int f(x)dx =g(x)$ then $\int f^{-1}(x)dx $ is equal to If function is differentiable at a point, is it continuous in a neighborhood? Help in simplifying combinatorial sum $\frac{n!}{(n-k)!}-{1\over(n-k)!}{\sum _{m=1}^{k-1} (-1)^{m+1} (n-m)! S(k,k-m)}$ Approximating minimum of $f(x)+g(x)$ by solving for $f(x)=g(x)$ A tricky integral using Fourier Transform and Dirac-functions combinatorics: 5 people picking 10 seats when there must be at least one space between them Propositional truncation $||$-$||$ and double negation $\neg\neg$ Prove that every permutation matrix satisfies its characteristic polynomial. Coordinate proof that the sum of a triangle's angles is $180^\circ$? If the difference quotient $\frac{f(y)-f(x)}{y-x}$ has a limit along a line $(x,y)\to(c,c)$, does the ordinary derivative $f'(c)$ exist?

Recent Posts