# Fitch natural deduction proof of $\neg D, A \to B, B \to (C \lor D), A \lor C \vdash C$

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? 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: 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. (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: • 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! – Gerhardus Carinus May 1 at 16:56
• 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. – lemontree May 1 at 16:57
• Yes, R is equivalent to Reit (reiteration). "R" is just the rule name that the online tool uses. – lemontree May 1 at 17:01
• 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! – Gerhardus Carinus May 1 at 21:15
• 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$. – lemontree May 1 at 21:21