# find formal proof

Got stuck while figuring out the formal proof for the following: $$\begin{array}{r} A\lor B\\ \neg B\lor C\\ \hline A\lor C \end{array}$$

The conclusion seems obvious. But finding a formal proof for it does not seem to be a trivial task for me.

I am trying to solve it via the backwards method. The conclusion is most likely to be derived via $\lor$Elim rule, but I cannot figure out how to derive it from the premises.

I will be grateful for any hints! Thank you!

-
Which rules of deduction are you using? – Henning Makholm Dec 13 '11 at 14:43

## 2 Answers

It's been a long time, and I've forgotten the standard notation and terminology, but you can split up a disjunction (I think it's called "disjunction elimination", as you alluded to in the question) into two subproofs; if they have the same result, you can then claim that result:

$$\begin{array}{rcl} 1&A\lor B&\textrm{given}\\ 2&\neg B\lor C&\textrm{given}\\ 3&A&\textrm{assume}\\ 3.1&A\lor C&\textrm{disjunction introduction, or whatever it's called, }3\\ 4&B&\textrm{assume}\\ 4.1&\neg\neg B&\textrm{whatever the rule's called, }4\\ 4.2&C&\textrm{whatever the rule's called, }2,4.1\\ 4.3&A\lor C&\textrm{disjunction introduction, or whatever it's called, }4.2\\ 5&A\lor C&\textrm{disjunction elimination, or whatever it's called, }1,3.1,4.3\end{array}$$

-
This come as valid, but unfortunately I think you've used disjunctive syllogism here, which isn't one of the introduction and elimination rules for this text: ssdi.di.fct.unl.pt/~pb/cadeiras/lc/0102/lpl%20textbook.pdf – Doug Spoonwood Dec 15 '11 at 3:12

I think you can do the subproof where you assume A and derive (A v C). You can always re-assume any premise further in the scope lines if you really want to do so, or seems convenient. So, the other subproof might look like this, with the numbering re-worked:

0 (¬B∨C) premise
1  |    B assumption
2  ||  ¬C assumption
3  ||| (¬B∨C) assumption
4  |||| ¬B assumption
5  |||| Contradiction (not sure how you write the symbol here) 1, 4

6  |||| C assumption
7  |||| Contradiction 2, 6
8  ||| Contradiction 3, 4-5, 6-7 V elimination
9  || ¬(¬B∨C) 3-8 ¬ introduction
10 || Contradiction 0, 9
11 | ¬¬C 2-11 ¬ introduction
12 | C 11 ¬ elimination
13 C 1-12, 0, and the other subproof


Note, I'm not sure if Fitch will accept this exactly, as I've never used that program. I also feel more confident that Fitch would accept the following distinct full proof:

1     (A v B) premise
2     (¬B∨C) premise
3  |   C  assumption
4  |  (A v C) 3 V introduction
5  |   ¬B assumption
6  ||  A assumption
7  ||  (A v C) 6 V introduction
8  ||  B assumption
9  ||| ¬(A v C) assumption
10 ||| Contradiction 5, 8
11 ||  ¬ ¬(A v C) 9-10 negation introduction
12 || (A v C) 11 negation elimination
13 |  (A v C) 1, 6-7, 8-12 disjunction elimination
14    (A v C) 2, 3-4, 5-13 V introduction.


Edit: I'm not sure if Fitch will accept "(A v C)", but it should come as a simple matter to drop the parentheses here. Also, if Fitch doesn't accept "(A v C)", but does accept "A v C" this actually comes as a weakness of the program, since "A v C" is not what logicians have called a "well-formed formula", while "(A v C)" does qualify as one... though your text uses the term "well-formed formula" in a slightly different way than I have here.

-