I've been struggling with a natural deduction problem for a while now...can anyone perhaps shed some light on where I'm going wrong here?

enter image description here

As you can see, I need to prove C from the given premises. My natural first move is to assume the negation of C and then prove a contradiction, but I run into a dead end if I start with ¬C as it doesn't flow into any other premises.

I therefore decided to start with a subproof with A as the premise. This leads to a couple of other deductions, and I get to the point where I have (C V D). I know that D is false (as per line 1) but I don't know how to get this over the line (to show that C is true as D is false).

Can someone please put me out of my misery?

Thanks all!


The idea of the proof of $C \lor D, \neg D \therefore C$ (known under the name "disjunctive syllogism") is the following: We know that one out of C or D must hold, so we consider both cases and start to assume either of the disjuncts, D and C. But we know that it can't be D that holds, because if we assume that it does, this contradicts our premise that D is false, so we derive a contradiction from which we can conclude anything, including C. And in the other case where we assume C to be true, we trivially get C as well, so in any case, we can conclude C, not matter which of the disjuncts C or D is in fact true.

This is precisely the idea of disjunction elimination. And with a disjunction elimination, the proof has the following structure:

enter image description here

The lines to be cited in the $\lor E$ application are the lines of the major premise $C \lor D$ and the two subproofs $C \vdash C$ and $D \vdash C$. This explains one of the errors you got: The line range for the subproof with premise $C$ was missing. The other error is that the subproof with premise $D$ does not have the conclusion $C$.

With the above skeleton, we just ned to find out how to get from C to C, and from D to C, using the premises in lines 1 and 2.
$C \vdash C$ is easy: We already have $C$ as the premise of the subproof, so we can just reiterate the line.
For $D \vdash C$, you were already on the right track: The premise $D$ of the subproof contradicts the previous assumption $\neg D$, which yields a contradiction. By es falso quodlibet, from $\bot$ we may conclude anything; conventiently, we can choose $C$.
Since from both $C$ and $D$ we derived $C$, we can apply $\lor E$ on the premise $C \lor D$ and conclude $C$, as desired.

enter image description here

(The rule name $X$ in line 7 is more commonly known as $\bot$, or $\bot E$, or "ex falso quodlibet (EFQL)", or "principle of explosion", depending on which of the hundreds of textbooks out there you're using.)

Then to finish the whole proof, you just need one final $\lor E$ to derive $A \lor C \vdash C$ and you're done:

enter image description here

  • $\begingroup$ Thank you so much for the concise explanation @lemontree! Just some context: I am working from the "Language Proof And Logic" book by Barwise and Etchemendy. From what I can see, they do not have "X" as a justification rule (as per your line 12 above). Is there another option for X, or can you explain what it means? Oh, and I am assuming that "R" is equivalent to "Reit" in the abovementioned book. Thanks again! $\endgroup$ – Gerhardus Carinus May 1 at 16:56
  • $\begingroup$ As I added as a comment somehwere in my explnation, that X should be a $\bot$ (apparently I accidentally typed "X" instead of "XX" (which is the key combination to produce $\bot$), and it wasn't detected as an error for some reason). I just didn't want to set up the proofs all anew when I realized the error. $\endgroup$ – lemontree May 1 at 16:57
  • $\begingroup$ Yes, R is equivalent to Reit (reiteration). "R" is just the rule name that the online tool uses. $\endgroup$ – lemontree May 1 at 17:01
  • $\begingroup$ Thanks! Okay so I finished the proof by using ⊥E - I'm assuming that's what you meant to illustrate? So just to get my bearings straight: if you have a disjunction and you manage to prove that one side of the disjunction is false, you use ⊥E to show that the other side of the disjunction is true. That's what the solution makes it seem like. Thanks for your help thus far! $\endgroup$ – Gerhardus Carinus May 1 at 21:15
  • 1
    $\begingroup$ Yes, $\bot E$ is another name for the rule I mean, if by $\bot E$ you refer to the rule that allows you to conclude any formula $A$ from $\bot$ without closing any assumptions, often referred to as "ex falso quodlibet (EFQL)". (And it turns out that indeed $X$ and not $\bot$ is the symbol used by the ND proof editor, so not a typo.) Naming conventions differ between different books/tools, it can get messy especially with rules involving $\bot$ and $\neg$. $\endgroup$ – lemontree May 1 at 21:21

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.