# formal proof challenge

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!

-
Well, it isn't really true that you can infer A from what you're given, is it? There is a situation where the assumptions hold, but A is still false, right? What situation is that? What happens then? – Ben Dec 13 '11 at 17:07
from $A\vee B$, $A\vee C$, you get $(A\vee B)\land(A\vee C)$ and from this you get $A\lor(B\land C)$. your approach cant work because if $A$ is false and both $B,C$ are true, the prop holds – yoyo Dec 13 '11 at 17:18
Without knowing what formal proof system you are using, it is impossible to answer. The details of the formal proof will vary immensely from one system to another. – Carl Mummert Dec 13 '11 at 17:20
For example, in one system I am used to, every (substitution instance of a) tautology is an axiom. So you can use $(A \lor B) \to (A \lor C) \to (A \lor (B \land C))$ as an axiom, apply modus ponens twice to cut $A \lor B$ and $A \lor C$ and you will be left with the conclusion you want. – Carl Mummert Dec 13 '11 at 17:21
If your not familiar with a term like "formal proof system", I'll ask exactly what rules of inference can you use? Exactly, what axioms (if any... you might not have any) can you use? – Doug Spoonwood Dec 13 '11 at 17:51

Is the following a "formal proof"?

Let $a$, $b$, $c$ be boolean variables representing the truth values of $A$, $B$, $C$. Then by the second distributive law of Boolean algebra we have

$$(a\vee b)\wedge(a\vee c)=a\vee(b\wedge c)\ .$$

This shows that your "argument" not only proves the truth of the third line under the assumption of the first two, but that in fact the stuff above the \hline is logically equivalent to what's underneath.

-

Since you've pointed out the text elsewhere these problems seem to come from, here goes:

1 (A v B) premise
2 (A v C) premise
3 | A hypothesis
4 | (A v (B^C)) 3 V introduction
5 | B hypothesis
6 || A hypothesis
7 || (A v (B^C)) 6 V introduction
8 || C hypothesis
9 || (B^C) 5, 8 ^ introduction
10 || (Av(B^C)) 9 V introduction
11 | (Av(B^C)) 6-7, 8-10, 2 V elimination
12 (Av(B^C)) 3-4, 5-11, 1 V elimination.

-