# Natural deduction: how to prove the argument below

Sorry my title is a bit vague, but I have a specific problem I'm trying to solve.

$$P \rightarrow Q \vdash \lnot(P\land\lnot Q)$$

I need to prove this using natural deduction, I can do it using equivalent symbols in propositional logic, but I can't seem to figure out where to even begin in terms of natural deduction.

I (mostly) understand the introduction and elimination rules for connectives, but I just don't know what to do here. I know I've got to turn the premise into the conclusion step by step using introduction and elimination of these logical connectives, but how?

• By "natural deduction" I assume you are looking for a proof "by contradiction". That is, starting from $P \to Q$ and the hypothesis $(P \land \lnot Q)$, produce a contradiction. This seems a straightforward exercise. – hardmath Nov 18 '16 at 13:23
• Would you mind showing me how? I've got: $$1. P \rightarrow Q$$ $$2. \lnot P \lor Q$$ Using Implication elimination rule How do I get to the next step – Shiny_and_Chrome Nov 18 '16 at 14:59
• Instead you want: $$2. P \land \lnot Q$$ When this leads to a contradiction, you will be able say you've done the natural deduction proof. – hardmath Nov 18 '16 at 15:04
• Ok, from my understanding of propositional logic and truth tables, I understand why this is a contradiction and how that proves the original statement, but how do I show that in a natural deduction proof? E.g. $$P \land \lnot Q, Q \lor R \vdash R \lor S$$ $$1. P \land \lnot Q$$ $$2. Q \lor R$$ $$3. \lnot Q$$ $$4. R$$ $$5. R \lor S$$ – Shiny_and_Chrome Nov 18 '16 at 15:17

1. P→Q     premise
2. P∧¬Q    assumption
3. P       ∧elim 2
4. ¬Q      ∧elim 2
5. Q       MP 1 3
6. ⊥       4 5
7. ¬[P∧¬Q] ¬intro 2 6


$$P\to Q\vdash\lnot(P\land\lnot Q)$$

I (mostly) understand the introduction and elimination rules for connectives, but I just don't know what to do here. I know I've got to turn the premise into the conclusion step by step using introduction and elimination of these logical connectives, but how?

You seek to derive a negated statement.   Negation Introduction is clearly named as the rule to use for this, so what do you need for it?   Why, it requires deriving a contradiction under the assumption of the positive statement.

$$\begin{array}{|l}~~~~\begin{array}{|l}~~\mathrm m.~\phi\\\hline~~~~\vdots\\~~\mathrm n.~~\bot\end{array}\\~~\mathrm o.~~\lnot\phi\qquad{\lnot}\mathsf I~\mathrm {m{-}n}\end{array}$$

So lets set that up

$$\def\fitch#1#2{~~~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~~P\to Q}{\fitch{~~2.~~P\land\lnot Q}{~~~~\vdots\\~~?.~\bot}\\~~?.~\lnot(P\land\lnot Q)\quad{\lnot}\mathsf I~2{-}?}$$

So, how do you derive a contradiction - or rather, what two contrary statements are you able to derive in order to use Negation Elimination -?   Well, you have that assumption and the premise to work with so Conditional Elimination and Conjunction Elimination rules are indicated.$$\begin{array}{|l}~~\mathrm m.~~\phi\\~~\mathrm n.~~\lnot\phi\\~~\mathrm o.~~\bot\qquad{\lnot}\mathsf E~\mathrm{m,n}\end{array}\qquad\begin{array}{|l}~~\mathrm m.~~\phi\\~~\mathrm n.~~\phi\to\psi\\~~\mathrm o.~~\psi\qquad{\to}\mathsf E~\mathrm {m,n}\end{array}\qquad\begin{array}{|l}~~\mathrm m.~~\phi\land\psi\\~~\mathrm n.~~\phi\qquad{\land}\mathsf E~\mathrm m\\~~\mathrm o.~~\psi\qquad{\land}\mathsf E~\mathrm m\end{array}$$

So, having assumed $$P\land\lnot Q$$, we can use that infer $$P$$, and also to infer $$\lnot Q$$, with Conjunction Elimination. Having derived $$P$$ we may use that and the premise $$P\to Q$$ to infer $$Q$$ with Conjunction Elimination. Finally, having derived both $$Q$$ and $$\lnot Q$$, we may infer the contradiction with Negation Elimination.

$$\fitch{~~1.~~P\to Q}{\fitch{~~2.~~P\land\lnot Q}{~~3.~\lnot Q\qquad{\land}\mathsf E~2\\~~4.~P\qquad{\land}\mathsf E~2\\~~5.~~Q\qquad{\to}\mathsf E~4,1\\~~6.~\bot\qquad{\lnot}\mathsf E~5,3}\\~~7.~\lnot(P\land\lnot Q)\quad{\lnot}\mathsf I~2{-}6}$$