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

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}$$

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.

The following proof uses disjunction elimination (vE) for both premises. I consider case $$A$$ on lines 3-4 and case $$B$$ on lines 5-11 from the first premise. For case $$B$$, I consider the two cases from the second premise, $$¬B$$ and $$C$$. On line 8, I use explosion (X) because of the contradiction obtained on line 7.

Links to the proof checker and the forallx textbook are given below.

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Fall 2019. http://forallx.openlogicproject.org/forallxyyc.pdf