You should now Launch Deriver and do the 4 exercises of Propositional Exercise 9 (Propex9).
You have choice here of how to do this. You can work on the exercise which is reproduced below. Or you can click Propositional Exercises (A click should download a zipped folder of files ('PropositionalExercises<mostRecentVersion>.zip'). Your web browser may expand this directly or double clicking will expand (unzip) it. Launch Deriver first, then open the files in Deriver.)
Derive the following using Tactics. (Start the derivation, switch
Tactics on, select the disjunt formula, and click ∨E-- this will lay out
the derivation for you.) Then repeat the derivations without using
Tactics.
a) F∨G,F⊃H,G⊃H∴H
b) (F∧F)∨(G∧G),F⊃H,G⊃H∴H
c) F∨G ∴G∨F
d) (F⊃G)∧(H⊃D), F∨H ∴ G∨D
Derive the following.
a) F∨(G∧∼G)∴ F
b) F∨G, G⊃H ∴ ∼F⊃H
c) ∼F∧∼G∴ ∼(F∨G)
There are a number of important theorems which can be expressed as equivalences-- here we consider slightly weakened versions of them which are conditionals.
Derive
De Morgan's Laws
d) ∴ (∼F∧∼G)⊃∼(F∨G)
Distribution
e) ∴ (F∧(G∨H))⊃((F∧G)∨(F∧H))
f) ∴ ((F∨G)∧(F∨H))⊃(F∨(G∧H))
g) ∴ (F∧(G∨H))⊃((F∧G)∨(F∧H))
h) ∴ ((F∨G)∧(F∨H))⊃(F∨(G∧H))
Implication
j) ∴ (∼F∨G)⊃(F⊃G)
Derive the following with or without Tactics. (Start the derivation, switch Tactics on, and click ≡I --this will lay out the derivation for you.) Then do the derivations without using Tactics.
a) (F⊃G)∧(G⊃F) ∴ F≡G
b) ∴ (F∧F)≡F
c) ∴ (F∨F)≡F
There are a number of well-known theorems which express equivalences between formulas, derive them
Association
a) ∴ F∨(G∨H)≡(F∨G)∨H
b) ∴ F∧(G∧H)≡(F∧G)∧H
Commutation
c) ∴ F∨G≡G∨F
d) ∴ F∧G≡G∧F
De Morgan's Laws
e) ∴ ∼(F∧G)≡∼F∨∼G
f) ∴ ∼(F∨G)≡∼F∧∼G
Distribution
g) ∴ F∧(G∨H)≡(F∧G)∨(F∧H)
h) ∴ F∨(G∧H)≡(F∨G)∧(F∨H)
Double Negation
i) ∴ F≡∼∼F
Equivalence
j) ∴ (F≡G)≡(F⊃G)∧(G⊃F)
k) ∴ (F≡G)≡(F∧G)∨(∼F∧∼G)
Exportation
l) ∴ (F⊃(G⊃H))≡((F∧G)⊃H)
Implication
m) ∴ F⊃G≡∼F∨G
Transposition
n) ∴ F⊃G≡∼G⊃∼F