2
$\begingroup$

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!

  • 0
    Which rules of deduction are you using?2011-12-13

3 Answers 3

2

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}

  • 0
    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: http://ssdi.di.fct.unl.pt/~pb/cadeiras/lc/0102/lpl%20textbook.pdf2011-12-15
0

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.