Section 7.3 introduces five replacement rules, four of which have two versions
|
Assoc | [p•(q•r)] [p∨(q∨r)] |
:: :: |
[(p•q)•r] [(p∨q)∨r] |
|
Com | [p•q] [p∨q] |
:: :: |
[q•p] [q∨p] |
|
Dist | [p•(q∨r)] [p∨(q•r)] |
:: :: |
[(p•q)∨(p•r)] [(p∨q)•(p∨r)] |
|
DM | ~(p•q) ~(p∨q) |
:: :: |
(~p∨~q) [~p•~q] |
|
DN | p | :: | ~~p |
Section 7.4 introduces another five replacement rules, two of which have two versions
|
Equiv | [p≡q] [p≡q] |
:: :: |
[(p•q)∨(~p•~q)] [(p⊃q)•(q⊃p)] |
|
Exp | [(p•q)⊃r] | :: | [p⊃(q⊃r)] |
|
Impl | [p⊃q] | :: | [~p∨q] |
|
Taut | p p |
:: :: |
[p•p] [p∨p] |
|
Trans | [p⊃q] | :: | [~q⊃~p] |
WARNING: The text examples and answers occasionally combine several replacement rules or repeated uses of one rule into one step. LogicCoach does not allow this. So, it will reject some proofs that the text accepts.
These rules each have one premise and may work on any well formed portion of the whole line! For example, all of the following are correct.
| 1. | A ⊃ (B ∨ C) | ||
| 2. | ~~[A ⊃ (B ∨ C)] | 1 DN | |
| 3. | ~~A ⊃ (B ∨ C) | 1 DN | |
| 4. | A ⊃ ~~(B ∨ C) | 1 DN | |
| 5. | A ⊃ (~~B ∨ C) | 1 DN | |
| 6. | A ⊃ (B ∨ ~~C) | 1 DN |
Either the left or right side of the :: may serve as the premise form with the other side serving as the conclusion form.
| 1. | A ⊃ B | |||
| 2. | ~A ∨ B | 1 Impl | (Here p⊃q is the premise form and ~p∨q is the conclusion form.) | |
| 3. | (~A ∨ B) ∨ C | 2 Add | ||
| 4. | ~A ∨ (B ∨ C) | 3 Assoc | ||
| 5. | A ⊃ (B ∨ C) | 4 Impl | (Here ~p∨q is the premise form and p⊃q is the conclusion form.) |