Natural deduction: how to prove the argument below

Question

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?

Answer 1

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

Answer 2

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