Section 7.1 introduces four implication rules
| DS | p∨q | / | ~p | // | q | |
| HS | p⊃q | / | q⊃r | // | p⊃r | |
| MP | p⊃q | / | p | // | q | |
| MT | p⊃q | / | ~q | // | ~p |
Section 7.2 introduces another four implication rules
| SIMP | p•q | // | p | |||
| CONJ | p | / | q | // | p•q | |
| ADD | p | // | p∨q | |||
| CD | (p⊃q)•(r⊃s) | / | p∨r | // | q∨s |
These rules have one or two premises and always work on Main Operators. For example, the ADD rule always produces a conclusion with a ∨ main operator. When using ADD do not look for a premise with a ∨ MO. Rather seek a conclusion or new step which needs to have a ∨ MO.
CORRECT
| 1. | (A ∨ B) ⊃ C | ||||
| 2. | A | / | C | ||
| 3. | A ∨ B | 2 Add | |||
| 4. | C | 1,3 MP |
Incorrect
| 1. | A ⊃ B | / | A ⊃ (B ∨ C) | ||
| 2. | A ⊃ (B ∨ C) | 1 Add | X since the ∨ in line 2 is NOT the MAIN OPERATOR. |
Note: the inference from 1 to 2 is truth table valid but it takes more than one step to derive it. See the next correct proof.
| 1. | A ∨ B | / | A | ||
| 2. | A | 1 Add | X since line 2 does not have a ∨ MAIN OPERATOR. |
This inference is truth table invalid. It therefore cannot be derived at all.
CORRECT
| 1. | A ⊃ B | / | A ⊃ (B ∨ C) | ||
| 2. | ~A ∨ B | 1 Impl | (A rule introduced in 7.4 | ||
| 3. | (~A ∨ B) ∨ C | 2 Add | |||
| 4. | ~A ∨ (B ∨ C) | 3 Assoc | (A rule introduced in 7.3) | ||
| 5. | A ⊃ (B ∨ C) | 4 Impl |