2/3/06
You should now Launch Deriver and do the 3 exercises of Propositional Exercise 6 (Propex6).
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.)
Each of the derivations in the following Exercise can be done using the Rule of Elimination of the Conditional ⊃E, and the rules learned previously.
If a formula in a line of a derivation has the form
<formula1>
and a formula in a line of a derivation has the form
<formula1> ⊃ <formula2>
the Rule of Elimination of the Conditional ⊃E allows you to add
<formula2>
The elimination of ⊃ {⊃E} is the classical inference rule known as Modus Ponens. In English, if you have A and If A then B you are entitled to B.
Show each of the following arguments to be valid. (Select, Copy, Start Proof and go from there.)
(a) F, F⊃G ∴ G
(b) F⊃G, F ∴ G∧F
(c) F⊃G, G⊃H,F ∴H
(d) F⊃(G⊃H), F⊃G,F ∴H∧F
(e) F⊃((~G)⊃H), F⊃~G,F ∴H∧F
Each of the derivations in the following Exercise can be done using only the rule the Rule of Elimination of the Biconditional ≡E, and the rules learned previously.
If the formula in a line in a derivation has the form
<formula1>≡<formula2>
the Rule of Elimination of the Biconditional ≡E allows you to remove the biconditional and add either
<formula1>⊃<formula2>
or
<formula2>⊃<formula1>
as an extra line. You have a choice here (on the direction of the conditional).
Show each of the following arguments to be valid.
(a) F≡G ∴ G⊃F
(b) F≡G ∴ F⊃G
(c) F≡G, G ∴ H∨F
(d) F≡G, G≡H, F ∴ H
After you have started the proof switch on 'Tactics' under the Proof Wizard menu, and do the derivations in the following way. If any of the lines you wish to obtain has a connective in it, click the appropriate Introduction rule (in these examples this will split the problem in two). If any of the lines you have obtained has a connective in it, use an Elimination rule to take it out.
(a) F≡G, H∧G ∴G∧F
(b) (F∧H)∧(R∧G) ∴F∧G