8/21/06
You should now Launch Deriver and do the 1 exercise of Propositional Exercise 10 (Propex10).
There are a number of well-known theorems which express equivalences between formulas. Experienced logicians know these off by heart. You have already derived many of them. Be sure you can derive the rest. Feel free to use rewrite rules on these.
Absorption1) ∴ (F∨(F∧G))≡F
2) ∴ (F∧(F∨G))≡F
3) ∴ (F⊃(F⊃G))≡(F⊃G)
Association
4) ∴ F∨(G∨H)≡(F∨G)∨H
5) ∴ F∧(G∧H)≡(F∧G)∧H
6) ∴ F∨G≡G∨F
7) ∴ F∧G≡G∧F
8) ∴ (F≡G)≡(G≡F)
9) ∴ F⊃(G⊃H)≡G⊃(F⊃H)
10) ∴(F⊃G)≡(∼G⊃∼F)
11) ∴ ∼(F∧G)≡∼F∨∼G
12) ∴ ∼(F∨G)≡∼F∧∼G
13) ∴ F∧(G∨H)≡(F∧G)∨(F∧H)
14) ∴ F∨(G∧H)≡(F∨G)∧(F∨H)
15) ∴ F≡∼∼F
16) ∴ (F≡G)≡(F⊃G)∧(G⊃F)
17) ∴ (F≡G)≡(F∧G)∨(∼F∧∼G)
18) ∴ F∨∼F
19) ∴ (F⊃(G⊃H))≡((F∧G)⊃H)
20) ∴ (F∧F)≡F
21) ∴ (F∨F)≡F
22) ∴ F⊃G≡∼F∨G
23) ∴ (F⊃G)≡(∼F∨G)
24) ∴ (F⊃G)≡∼(F∧∼G)
25) ∴ (F∨G)≡(∼F⊃G)
26) ∴ (F∧G)≡∼(F⊃∼G)
27) ∴ (F≡G)≡ ((F⊃G) ∧ (G⊃F))
28) F⊃G,G⊃H∴F⊃H
29) ∴ F⊃G≡∼G⊃∼F