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!

  • $\begingroup$ Which rules of deduction are you using? $\endgroup$ – 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.

enter image description here

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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.