Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

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!

share|cite|improve this question
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}$$

share|cite|improve this answer
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: – 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.

share|cite|improve this answer

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

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