Here are some further derived rules. In naming these rules I have used the same name for similar or closely connected primitive rules.
Biconditional Introduction Bioconditional Elimination
| | X | X≡Y
| | . | X
| | . | Y ≡E
| | Y and
| | X≡Y
| | Y
| | X ≡E
| | Y
| | .
| | .
| | X
| X≡Y ≡I
| ~XvY | Xv~Y
| X and | Y
| Y vE | X vE
Denying the Consquent Reductio Ad Absurdum
(Traditionally called "Modus Tolems")
| X⊃Y | X⊃~Y | ~X⊃Y | | ~X
| ~Y | Y | ~Y | | .
| ~X DC | ~X DC | X DC | | .
| | Y
| | ~Y
| X RD
The reductio ad absurdum rule looks like a negation elimination rule. Actually, as you will see when you do the exercises, it uses both ~I and ~E.
We can get further derived rules from the laws of logical equivalence (chapters 3 and 4). For example, any sentence of the form ~(XvY) is logicalley equivalent to ~X&~Y. Because two logically equivalent sentences have the same truth value in any assignment of truth values to sentence letters, if one of these sentences validly follows from some premises and assumptions, so does the other. We can use these facts to augment our stock of derived rules:
| ~(XvY) | ~X&~Y
| ~X&~Y DM | ~(XvY) DM
Similarly, one can use other logical equivalences to provide derived rules. Here is a list of such rules you may use, given in a shortened notation. You should understand the first line as the pair of derived de Morgan rules immediately above. Understand the following lines similarly.
DE MORGAN'S RULES
~(XvY) and ~X&~Y are mutually derivable (DM).
~(X&Y) and ~Xv~Y are mutually derivable (DM).
X⊃Y and ~Y⊃~X are mutually derivable (CP).
~X⊃Y and ~Y⊃X are mutually derivable (CP).
X⊃~Y and Y⊃~X are mutually derivable (CP).
X⊃Y and ~XvY are mutually derivable (C).
~(X⊃Y) and X&~Y are mutually derivable (C).
The letters in parentheses are the abbreviations you use to annotate your use of these rules.
We could add further rules of mutual derivability based on the distributive, associative, commutative, and other laws of logical equivalence. But in practice the above rules are the ones which prove most useful.
It is not hard to prove that these rules of mutual derivability follow from the primitive rules-in fact, you will give these proofs in the exercises.
Many texts use rules of logical equivalence to augment the rules for derivations in a much more radical way. These strong rules of replacement, as they are called, allow you to substitute one logical equivalent for a subsentence inside a larger sentence. Thus, if you have derived '(AvB)⊃C', these strong rules allow you to write down as a further conclusion '(Av~~B)⊃C', where you have substituted '~~B' for the logically equivalent 'B'.
By the law of substitution of logical equivalents, we know that such rules of replacement must be correct, in the sense that they will always take us from true premises to true conclusions. But it is not so easy to prove these replacement rules as derived rules. That is, it is hard to prove that one can always systematically rewrite a derivation using one of these replacement rules as a longer derivation which uses only primitive rules. For this reason I won't be using these replacement rules. Your instructor may, however, explain the replacement rules in greater detail and allow you to use them in your derivations. Your instructor may also choose to augment the list of logical equivalents you may use in forming such rules.
7-3. Prove all the derived rules given in the text but not proved there. In each of your proofs use only those derived rules already proved.
7-4. Provide derivations which establish the validity of the following arguments. You may use any of the derived rules. In fact, many of the problems are prohibitively complex if you don't use derived rules!
a) M&(~BvC) b) M⊃(D⊃P) c) (K⊃S)⊃(S⊃H)
B⊃C M⊃S S
d) F⊃O e) ~[(F&H)v~F] f) B⊃(HvR)
L⊃J ~H B⊃(~H⊃R)
g) ~(~M&D) h) (A⊃B)&(D⊃~B) i) P⊃(DvM)
F⊃~M (CvD)&(C⊃~B) (P⊃D)v(P⊃M)
j) (G&~M)⊃(~M&K) k) AvB l) S=J
K⊃~G ~B≡(CvD) (S&J)v(~S&~J)
m) ~C⊃[Fv~(DvN)] n) (GvA)⊃(H⊃B) o) F⊃(KvB)
~N⊃D [H⊃(H&B)]⊃K (~FvG)&(~Gv~K)
~F⊃C G⊃K F⊃B
p) Dv(M⊃J) q) Q-~(A&F) r) (J&~T)⊃P
[M⊃(M&J)]⊃(PvK) ~(MvA)⊃~H ~A⊃~T
(P⊃D)&(K⊃F) ~(Q&A)vF ~TvC
DvF Q⊃(H⊃M) C⊃D