4
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Welcome to MSE. Please use MathJax. $\endgroup$ – José Carlos Santos Jan 28 '18 at 12:07
  • $\begingroup$ Have you tried using the law of excluded middle (or an equivalent axiom)? $\endgroup$ – Luca Bressan Jan 28 '18 at 12:20
  • $\begingroup$ @user15269 what formal proof system are you using? 'Natural Deduction' can still cover several different styles and specific rules. $\endgroup$ – Bram28 Jan 28 '18 at 13:28
0
$\begingroup$

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}

$\endgroup$
  • $\begingroup$ Hello, Taroccoesbrocco. How can I find out more about the test diagrams you used in your answer? $\endgroup$ – MathOverview Jan 28 '18 at 12:52
  • 1
    $\begingroup$ @MathOverview - This is a quite standard notation for natural deduction. See Wikipedia (forget about "true" in derivations), or here and here for a quick introduction. $\endgroup$ – Taroccoesbrocco Jan 28 '18 at 12:59
1
$\begingroup$

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

$\endgroup$
1
$\begingroup$

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$

$\endgroup$
0
$\begingroup$

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

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.