1
$\begingroup$

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?

$\endgroup$
4
  • $\begingroup$ 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. $\endgroup$ – hardmath Nov 18 '16 at 13:23
  • $\begingroup$ 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 $\endgroup$ – Shiny_and_Chrome Nov 18 '16 at 14:59
  • $\begingroup$ 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. $\endgroup$ – hardmath Nov 18 '16 at 15:04
  • $\begingroup$ 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 $$ $\endgroup$ – Shiny_and_Chrome Nov 18 '16 at 15:17
3
$\begingroup$
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
$\endgroup$
0
$\begingroup$

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

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