I have a question I have come across in an old exam paper which I am trying to work through.

It states that a formal proof must be given using the rules of natural deduction

enter image description here

Now generally what I do is I work backwards to see how I could derive the conclusion then I start working forward.

Two problems I am having:

1) For C → D ∨ E this does not look well formed to me as it is lacking parentheses so it seems ambiguous to me. I have chosen to rewrite this as follows (C → D) ∨ E.

2) Working backward initially I use conditional introduction in my sub-proof before my conclusion.

See below:

enter image description here

I have chosen to reiterate B line 7 as I want to be able to derive by elsewhere in my proof.

I am not sure how to proceed next. I thought of perhaps using contradiction elimination by finally deriving a contradiction and ultimately asserting C → D.

Some advice on how to proceed would be greatly appreciated.



The usual convention for the omission of parentheses is that :

1) the negation symbol applies to as little as possible

2) $\land$ and $\lor$ apply to as little as possible, given the above convention.

Thus, $C \to D \lor E$ must be :

$C \to (D \lor E)$.

  • $\begingroup$ @ Mauro ALLEGRANZA Thanks for the input let me try this. $\endgroup$ – Metamorphosis Oct 19 '15 at 21:15

As @Mauro ALLEGRANZA points out, the convention is that $\vee$ and $\wedge$ bind more tightly than $\to$, so the formula is $C \to (D \vee E)$. Here's a sketch of how the deduction proceeds:

  1. $\neg A \to B$
  2. $C \to D \vee E$
  3. $D \to \neg C$
  4. $A \to \neg E$
  5. $C \to \neg D \quad$ from 3.
  6. $C \to E \quad$ from 2. and 5.
  7. $E \to \neg A \quad$ from 4.
  8. $C \to \neg A \quad$ from 6. and 7.
  9. $C \to B \quad$ from 8. and 1.
  • $\begingroup$ Thanks for your input here. Is this a proof by cases? Also, when citing the lines, you haven't referred to the rule of inference you have used? $\endgroup$ – Metamorphosis Oct 19 '15 at 21:34
  • 1
    $\begingroup$ True -- I did say "sketch". Not to be coy, though, in all but one case (line 6.) I'm using $\vdash (p \to q) \wedge (q \to r) \to (p \to r)$. Line 6. is really a sub-deduction: assume $C$; then $D \vee E$ by 2., and $\neg D$ by 5., soo.. $E$; so discharging the assumption proves $C \to E$. $\endgroup$ – BrianO Oct 19 '15 at 21:39
  • $\begingroup$ Thanks true, you did say sketch... Rule is Hypothetical Syllogism yes? Where it has the same feel as transitivity. I need to try cite this in the program I'm using. Will post an update once I get it right. $\endgroup$ – Metamorphosis Oct 19 '15 at 21:52
  • 1
    $\begingroup$ @Metastasis - if you are using Natural Deduction, "usually" there are no rules like HS or Transitivity (as primitive rules) ... And yes, you have to use $\lor$-elimination (i.e.proof by cases). $\endgroup$ – Mauro ALLEGRANZA Oct 20 '15 at 6:26
  • 2
    $\begingroup$ @Metastasis - you have to follow BrianO's answer, using ND rules. 1) assume $C$ and by $\to$-elim derive $D \lor E$. Here $\lor$-elim is needed : 1a) assume $D$, derive $\lnot C$ and from the contradiction, by $\bot \vdash \varphi$ conclude with $B$ and then $C \to B$. 1b) assume $E$, assume $A$, derive $\lnot E$ and, fron the contradiction, derive $\lnot A$ by $\lnot$-intro. Thus derive $B$ by $\to$-elim and then $C \to B$. Now, both 1a) and 1b) have $C \to B$: thus, conclude $C \to B$ by $\lor$-elim. $\endgroup$ – Mauro ALLEGRANZA Oct 20 '15 at 19:25

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.