# Step by step natural deduction: (T > E) ^ (A > L) /... (T v A) > (E v L)

I'm having trouble proving the following using natural deduction:

(T > E) ^ (A > L) /... (T v A) > (E v L)

I checked the answer but I didn't quite understanding the reason why the proof progressed in a certain way (example, at some point the book used addition but I didn't understand why).

Would anyone mind walking me through this? Thank you!

The permitted rules are found here: https://www.cse.iitk.ac.in/users/cs365/2012/rulesLogic.html

The only exception is that absorption is not allowed and constructive dilemma is allowed (but I doubt that will apply to this case).

• You sure constructive dilemma (aka proof by cases) is allowed? Because it looks to me like this is the proof of that very inference rule. Commented May 22, 2018 at 18:21
• Yes it's allowed, however since we have to directly prove it by starting from only the premise (T > E) ^ (A > L), it can't be immediately applied. But I agree this is clearly an exercise to prove the CD. Commented May 22, 2018 at 19:04

Premise :

0) (T⇒E) ∧ (A⇒L).

Use Material Implication on the premise to get :

1) (~T∨E) ∧ (~A∨L)

Use Simplification to get respectively :

2) (~T∨E)

and :

3) (~A∨L)

Using Addition on 2) get :

4) (~T∨E) ∨ L

Using Association :

5) ~T ∨ (E∨L)

Using Addition on 3) get :

6) (~A∨L) ∨ E

Using Association :

7) ~A ∨ (L∨E)

and using Commutation :

8) ~A ∨ (E∨L)

Using Conjunction on 5) and 8) get :

9) [~T ∨ (E∨L)] ∧ [~A ∨ (E∨L)]

Use Distribution to get :

10) (~T ∧ ~A) ∨ (E∨L)

Use De Morgan to get :

11) ~(T∨A) ∨ (E∨L)

Use Material imlication again to get :

12) (T∨A) ⇒ (E∨L).

I used Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker associated with the textbook by P. D. Magnus, Tim Button, J. Robert Loftis, Aaron Thomas-Bolduc, Richard Zach, forall x: Calgary Remix, to obtain the following proof.

The conjunction in the premise on line 1 is eliminated in lines 2 and 3.

A conditional is attempted by assuming the antecedent, T ∨ A, in a sub-proof on line 4.

The disjunction in line 4 is eliminated in line 11 by considering the two cases, one for T, lines 5 to 7, and one for A, lines 8 to 10. In both cases a disjunction was introduced to get the desired consequent, E ∨ L, on lines 7 and 10.

Since both cases produced the desired consequent, E ∨ L, the conditional can be introduced in line 12 which completes the proof.

• I'm wondering if this solver should be posted somewhere here under community wiki answer. It'd greatly reduce the number of homework questions regarding logic. Commented Jun 20, 2018 at 14:03
• @rus9384 It is licensed under a GNU General Purpose License v3 with source code available. Kevin Klement writes in the README: "To install, put the entire contents of this repository into a directory served to the web. It requires that your web server runs PHP 7." Commented Jun 20, 2018 at 14:08
• Also, it is not a solver, it is a checker. Commented Oct 22, 2019 at 3:21