Logic Natural Derivation in S

Question

How do you go about proving this conclusion from the set of premises?

$$\lbrace A\vee\neg B, \neg A\vee C, \neg C\to B\rbrace\vdash\neg D\vee C$$

I figure that if you assume $\neg C$, you can contradict yourself to end up with $C$. Something like getting $B$ from $\neg C$, and then using $B$ to get $\neg A$, and then $\neg A$ to get $C$ - I just have no idea how to reference these rules.

Any help/advice is greatly appreciated.

Edit: Using only rules R, ∧I/E, vI/E, →I/E, ⟺I/E, and ¬I/E

Answer 1

I figure that if you assume $¬C$, you can contradict yourself to end up with $C$. Something like getting $B$ from $¬C$, and then using $B$ to get $¬A$, and then $¬A$ to get $C$ - I just have no idea how to reference these rules.

A good thought, and very close.

Assuming $\neg C$ you can derive $B$ (from $\neg C\to B$), use that to derive $A$ (from $A\vee\neg B$), and in turn derive $C$ (from $\neg A\vee C$), thereby contradicting the assumption.

This is simple derivation, save that disjunctive syllogism is not a fundamental rule of your system.   Its derivation is based on disjunction elimination and the principle of explosion, which is implemented in your rules through negation-elimination/introduction.

Anyhow, here's how to derive $A$ when given $B$ and $A\vee\neg B$:

$$\def\fitch#1#2{\boxed{\begin{array}{l}#1\\\hline#2\end{array}}} {\begin{array}{|l|}&B&\\&A\vee\neg B\\&\fitch{A\hspace{10ex}\mathsf A}{A\hspace{10ex}\mathsf R}\\&\fitch{\neg B\hspace{8.5ex}\mathsf A}{\fitch{\neg A\hspace{6.5ex}\mathsf A}{B\hspace{8ex}\mathsf R\\\neg B\hspace{6.5ex}\mathsf R}\\A\hspace{10ex}\neg\mathsf E}\\&A\hspace{12ex}{\vee}\mathsf E\end{array}}$$

Answer 2

Here is a proof. Pipe characters | are used to denote lines of hypothesis. Line 13 technically doesn't use any single rule of replacement, but I'm sure the reader can figure out how to make it formal.

1. $A \vee \neg B \quad$ given
2. $\neg A \vee C \quad$ given
3. $\neg C \to B \quad$ given
4. $\neg B \to C \quad$ contrapositive (3)
5. | $A \quad$ assumption
6. | $\neg\neg A \quad$ double negation (5)
7. | $C \quad$ elimination of $\vee$ (2,6)
8. $A\to C$ introduction of $\to$ (5-7)
9. | $\neg A \quad$ assumption
10. | $\neg B \quad$ elimination of $\vee$ (1, 9)
11. | $C \quad$ elimination of $\to$ (4, 10)
12. $\neg A \to C$
13. $(A\vee \neg A) \to C \quad$ combining (8, 12)
14. $\mathbf{T} \to C \quad$ tautology (13)
15. $C \quad$ elimination of $\to$ (14)
16. $\neg D \vee C \quad$ introduction of $\vee$ (15)