Natural deduction proof for $(P\to\lnot Q)\to(\lnot P \lor\lnot Q)$

Question

I can't find the proof for $(P\to\lnot Q)\to(\lnot P \lor\lnot Q)$ in natural deduction.

I've tried using the introduction of $\to$ law by assuming $P\to\lnot Q$ and $P$ but can't seem to close my assumption of $P$.

Answer 1

Following the hint by Luca Bressan, a derivation in natural deduction of $(P \to \lnot Q) \to (\lnot P \lor \lnot Q)$ without any undischarged assumption ($[A]^*$ stands for an assumption $A$ discharged by the rule $*$) is:

\begin{align} \dfrac{\dfrac{\dfrac{\vdots}{\lnot P \lor P} \qquad \dfrac{[\lnot P]^*}{\lnot P \lor \lnot Q}\lor_{\mathrm{i}_1} \qquad \dfrac{\dfrac{[P \to \lnot Q]^\# \qquad [P]^*}{\lnot Q}\to_\mathrm{e}}{\lnot P \lor \lnot Q}\lor_{\mathrm{i}_2}}{\lnot P \lor \lnot Q}\lor_\mathrm{e}^*}{(P \to \lnot Q) \to (\lnot P \lor \lnot Q)}\to_\mathrm{i}^\# \end{align} where $\lnot P \lor P$ can be proved as follows (using reductio ad absurdum, which is valid in classical logic, not in intuitionistic logic): \begin{align} \dfrac{\dfrac{[\lnot(\lnot P \lor P)]^* \qquad \dfrac{\dfrac{\dfrac{[\lnot(\lnot P \lor P)]^* \qquad \dfrac{[P]^\#}{\lnot P \lor P}\lor_{\mathrm{i}_2}}{\bot}\lnot_\mathrm{e}}{\lnot P}\lnot_\mathrm{i}^\#}{\lnot P \lor P}\lor_{\mathrm{i}_1}}{\bot}\lnot_\mathrm{e}}{\lnot P \lor P}\mathsf{raa}^* \end{align}

Answer 2

Assuming $P\to \lnot Q$ and the law of excluded middle (so $P\vee \lnot P$) will do it in classical logic.

Hint: The Constructive Dilemna.

$$(A\vee B), (A\to C), (B\to D)~\vdash~ (C\vee D)$$

Answer 3

Assume $P\implies \neg Q$ furthermore we know that $P\lor\neg P$ is tautology we may then argue from cases as follows

Case-1: $P$ is true, then using this together with $P\implies \neg Q$ and applying modus ponens we can conclude $\neg Q$ and by addition $\neg P\lor \neg Q$.

Case-2: $P$ is false, then from addition we have $\neg P\lor\neg Q$.

$\blacksquare$

Answer 4

If you don;t have the Law of Excluded Middle readily available to you (i.e. if you first need to prove it doing a proof by contradiction), then I would suggest saving yourself a bit of work and just doing a proof by contradiction directly on your goal $\neg P \lor \neg Q$.

Here is a Fitch-style proof that does this:

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$

$\fitch{ 1. P \rightarrow \neg Q \qquad \quad Assumption}{ \fitch{ 2. \neg(\neg P \lor \neg Q) \quad Assumption}{ \fitch{ 3. \neg P \qquad \quad \quad Assumption}{ 4. \neg P \lor \neg Q \quad \lor \ Intro \ 3\\ 5. \bot \qquad \qquad \top \ Intro \ 2,4 } \\ 6. \neg \neg P \qquad \quad \neg \ Intro \ 3-5\\ 7. P \qquad \qquad \neg \ Elim 6\\ 8. \neg Q \qquad \quad \rightarrow \ Elim \ 1,7\\ 9. \neg P \lor \neg Q \quad \lor \ Intro \ 8\\ 10. \bot \qquad \qquad \top \ Intro \ 2,4}\\ 11. \neg \neg (\neg P \lor \neg Q) \quad \neg \ Intro \ 2-10\\ 12. \neg P \lor \neg Q \qquad \neg \ Elim \ 11 }$