TITLE: formal proof challenge
QUESTION [1 upvotes]: I am desperately trying to figure out the formal proof for this argument. 
$$\begin{array}{r}
A\lor B\\
A\lor C\\
\hline
A\lor (B \land C)
\end{array}$$
I am trying to apply the backwards method here. I am trying to infer A, in order to use vIntro in the last step and introduce the final disjunction. But I got stuck finding sufficient proof for A.
Any hint will be greatly appreciated. Thank you!

REPLY [0 votes]: I am trying to apply the backwards method here. I am trying to infer A, in order to use vIntro in the last step and introduce the final disjunction. But I got stuck finding sufficient proof for A.

You don't prove it; you assume it -- To be precise: you assume both cases aiming to derive the same conclusion from each.  The disjunction elimination rule then discharges the assumptions. This is also known as the Proof By Cases argument.  $$\dfrac{\dfrac{[A]^\star\\~~\vdots}{A\lor(B\land C)}\quad\dfrac{[B]^\star\\~~\vdots}{A\lor(B\land C)}\quad\lower{1.5ex}{A\lor B}~}{A\lor(B\land C)}{\small\lor\mathsf E^\star}$$
So, in this proof you need two $\lor$ eliminations and therefore four assumptions must be made and discharged.  The trick is how you combine the assumptions of $B$ and $C$.

 $$\dfrac{\dfrac{[A]^1}{A\lor(B\land C)}{\small\lor\mathsf I}\quad\dfrac{\dfrac{[A]^2}{A\lor(B\land C)}{\small\lor\mathsf I}\quad\dfrac{\dfrac{[B]^1\quad[C]^2}{B\land C}{\small\land\mathsf I}}{A\lor(B\land C)}{\small\lor\mathsf I}\quad\lower{1.5ex}{A\lor C}}{A\lor (B\land C)}{\small\lor\mathsf E^2}\quad\lower{1.5ex}{A\lor B}}{A\lor (B\land C)}{\small\lor\mathsf E^1}$$
{"set_name": "stack_exchange", "score": 1, "question_id": 91157}