Natural Deduction Proof: {A v B, ¬A v C} ⊢ B v C

Question

Prove using natural deduction: $(A \lor B), (\lnot A \lor C) ⊢ (B \lor C)$. My work so far:

1     A v B
2     A v C
3      A      :AS
4       ¬A      :AS
5       _|_     :¬E 3,4
6    ¬¬A      :¬I 4-5
7  --
8  ¬A     :AS

This is the work that I have come up with, for the past 5 hours. Can you please help me?

Answer 1

You are setting up for disjunction elimination, so when you derive contradiction, use explosion to derive the target conclusion.$$\def\fitch#1#2{~~\begin{array}{|l}#1\\\hline#2\end{array}}\fitch{~~1.~A\lor B\hspace{10ex}\textsf{Premise}\\~~2.~\lnot A\lor C\hspace{8.5ex}\textsf{Premise}}{\fitch{~~3.~A\hspace{12.5ex}\textsf{Assumption}}{\fitch{~~4.~\lnot A\hspace{8.5ex}\textsf{Assumption}}{~~5.~\bot\hspace{10ex}\textsf{Negation Elimination}\\~~6.~B\lor C\hspace{5.75ex}\textsf{Explosion (aka }\textit{Ex Falso Quodlibet}\textsf{)}}\\~~\vdots\\~~m.~B\lor C }\\~~\vdots\\~n.~B\lor C}$$

I am sure you can fill out the rest of this "proof by cases".

Answer 2

We have for $(\lnot A \lor C)$:

$1:\text{Premise}; (\lnot A \lor C) : \top$
$2:\text{Assumption}; A : \top$
$3:\text{Negation}(2); \lnot A : \bot$
$4:\text{Insertion}(3\to1); (\bot \lor C) : \top$
$5:\text{Implication}(4); C : \top$

and for $(A \lor B)$

$6:\text{Premise}; (A \lor B) : \top$
$7:\text{Assumption}; A : \bot$
$8:\text{Insertion}(7\to6); (\bot \lor B) : \top$
$9:\text{Implication}(8); B : \top$

and then:

$10:\text{Assumption}; A \lor \lnot A : \top$
$11:\text{Inference}(2,5); (A \supset C) : \top$
$12:\text{Inference}(7,9); (\lnot A \supset B) : \top$
$13:\text{Inference}(10,11,12); (B \lor C) :\top$