You should now Launch Deriver and do the 3 exercises of Propositional Exercise 7 (Propex7).
After starting the derivation switch on Tactics (under the Wizard Menu in the Proof Panel) and derive the following. Start by selecting the Rule ⊃I to lay out the derivation properly. Notice the form of each derivation-- the <if-clause> gets taken as a new assumption, from it the <then-clause> is derived, and the new assumption is dropped to conclude
<if-clause> ⊃ <then-clause>
a) (F⊃G), (G⊃H) ∴ (F⊃H)
b) (F⊃(G⊃H)), (F⊃G) ∴ (F⊃H)
c) (F⊃G) ∴ (F⊃(F∧G))
Now try to do the same derivations without using Tactics. To do each of them the first move is to assume the <if-clause> and in each case here that is F. To make an assumption you choose Assumption off the Rules Menu. When you have derived the <then-clause> select it and click ⊃I. (*There are some technical terms that appear here: the Rule of Assumption is called 'TI' (short for Trival Inference), and the new assumption is called an 'Antecedent'*)
a) (F⊃G), (G⊃H) ∴ (F⊃H)
(*this requires you to assume F and try to derive H as the last line of a subproof*)
b) (F⊃(G⊃H)), (F⊃G) ∴ (F⊃H)
(*this requires you to assume F and try to derive H as the last line of a subproof*)
c) (F⊃G) ∴ (F⊃(F∧G))
(*this requires you to assume F and try to derive F∧G as the last line of a subproof*)
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 (with or without Tactics)
Commutation
a) ∴ (F∧G)⊃(G∧F)
Double Negation
b) ∴ ∼∼F⊃F
Exportation
c) ∴ (F⊃(G⊃H))⊃((F∧G)⊃H)
d) ∴ ((F∧G)⊃H)⊃(F⊃(G⊃H))