# Propositional Logic - Formal Proofs using natural deduction

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

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:

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.

Thanks

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

• @ Mauro ALLEGRANZA Thanks for the input let me try this. – 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.
• 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? – Metamorphosis Oct 19 '15 at 21:34
• 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$. – BrianO Oct 19 '15 at 21:39
• 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. – Metamorphosis Oct 19 '15 at 21:52
• @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). – Mauro ALLEGRANZA Oct 20 '15 at 6:26
• @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. – Mauro ALLEGRANZA Oct 20 '15 at 19:25