Formal Logic/Sentential Logic/Disjunctions in Derivations

From Wikibooks, open books for an open world
Jump to navigation Jump to search
← Derived Inference Rules ↑ Sentential Logic End of Sentential Logic →



Disjunctions in Derivations[edit]

Disjunctions in derivations are, as the current inference rules stand, difficult to deal with. Using an already derived disjunction by applying Disjunction Elimination (DE) is not too bad, but there is an easier to use alternative. Deriving a disjunction in the first place is more difficult. Our Disjunction Introduction (DI) rule turns out to be a rather anemic tool for this task. In this module, we introduce derived rules which provide alternative methods for dealing with disjunctions in derivations.

Using already derived disjunctions[edit]

Modus Tollendo Ponens[edit]

We start with a new (to be) derived rule of inference. This will provide a useful alternative to Disjunction Elimination (DE).

Modus Tollendo Ponens, Form I (MTP)


Modus Tollendo Ponens, Form II (MTP)

Modus Tollendo Ponens is sometimes known as Disjunctive Syllogism and occasionally as the Rule of the Dog.

Supporting theorems[edit]

This new rule requires the following two supporting theorems.

 
1.       Assumption   
2.       1 KE
3.       1 KE
4.       3 CAdd
5.       T1 [P/Q]
6.       2, 4, 5 DE
 
7.     1–6 CI


 
1.       Assumption   
2.       1 KE
3.       1 KE
4.       3 CAdd
5.       T1
6.       2, 4, 5 DE
 
7.     1–6 CI

Example derivation[edit]

For an example using MTP, we redo the example derivation from Constructing a Complex Derivation.

    
 
1.     Premise
2.     Premise
3.     Premise
 
4.       Assumption   
   
5.         Assumption   
6.         2 KE
7.         3, 6 CE
8.         4, 7 MTP
9.         5, 8 KI
10.         1, 9 CE
11.         2 KE
   
12.       5–11 NI
 
13.     4–12 CI


After Line 4, we did not bother with subderivations for deriving the antecedent lines needed for DE. Instead, we went straight to a subderivation for the conclusion's consequent. At line 8, we applied MTP.

Deriving disjunctions[edit]

Conditional Disjunction[edit]

The next derived rule significantly reduces the labor of deriving disjunctions, thus providing a useful alternative to Disjunction Introduction (DI).

Conditional Disjunction (CDJ)

Supporting theorem[edit]

 
1.       Assumption   
   
2.         Assumption   
     
3.           Assumption   
       
4.           3 DI
5.           2 R
     
6.         3–5 NI
7.         1, 6 CE
8.         7 DI
   
9.       2–8 NI
 
10.     1–9 CI

Example derivation[edit]

This derivation will make use of T12 (introduced at Derived Inference Rules) even though its proof was left to the reader as an exercise. The correctness the following derivation, particularly Line 2, assumes that you have indeed proved T12.


  
 
1.       Assumption   
2.       T12
3.       1, 2 CE
4.       3 KE
5.       4 CAdd
 
7.     1–6 CI
8.     7 CDJ


Here we attempted to derive the desired conditional by first deriving the antecedent line needed for CDJ.