12/21/06 under revision
Learning conditional proof.
There is an additional propositional rule of inference-- Conditional Proof-- which is slightly more difficult than the ones that we have met before. It is slightly more difficult in that it requires you to make new assumptions, and the correct new assumptions at that.
Conditional Proof is a classical form of inference, dating back thousands of years. Conditional proof is a technique for proving statements of the form 'If A, then B' and it procedes by first assuming A, then deriving B, and finally dropping the assumption of A to conclude 'If A, then B'. (This technique is commonplace in mathematics. Many mathematical theorems have the right form (for example, 'If a triangle is Euclidean, then its angles sum to 180 degrees'), and such theorems are proved in the manner indicated (for example, 'Assume that the triangle is Euclidean, ... )).
In our rule system conditional proof appears as the Rule for Conditional Proof (CP). This, then, is a rule which gets used when you are trying to obtain a conditional formula ie one with a ⊃ as its main connective.
The circumstance it gets invoked looks like this.
? ? << G⊃F ?
That is, the formula you are trying to obtain has a ⊃ as its main connective-- the formula you are trying to obtain has the form <if-clause> ⊃ <then-clause>. In the illustration, for example, G is the <if-clause> and F is the <then-clause> .
You follow a three stage process. First you assume the <if-clause>. The illustrated fragment will then become
-> n. G ? ? << G⊃F ?
Second you continue deriving in this new context until you manage to derive the <then-clause> thus
-> n. G
<proof fragment in here> ?
F ? ? ? << G⊃F ?
Finally you select the <then-clause> and click CP to complete the conditional proof.
-> n. G
<proof fragment in here> ? k
F ?
G⊃F k ⊃I
After starting the derivation switch on Tactics (under the Wizard Menu in the Proof Panel) and derive the following. Start by selecting the Rule CP 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) (*This proof can be carried out quickly and directly by Hypothetical Syllogism-- however, ignore this and prove it by CP*)
b) (F⊃(G⊃H)), (F⊃G) ∴ (F⊃H)
c) (F⊃G) ∴ (F⊃(F.G)) (*This is direct by Absorption, but instead use CP*)
Proofs
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 CP.
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*)
Proofs
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))
Proofs
The last derivation ∴ ((F.G)⊃H)⊃(F⊃(G⊃H)) brings up an interesting point. If you do it by Tactics , part way through you can end up like this
Now, you are trying to get (F.G) from lines 2 and 3 (to use to get H from line 1), but, on the Rules Menu Conjunction is not enabled! What to do? Well, what is happening here is that Tactics is switched on, and Conjunction is enabled only if the target line is an 'And' (and line 5, H, does not have 'And' as its main connective). You have a choice here. The timid way is to switch Tactics off and do the step (and switch Tactics back on, if you wish). The bolder way is to use New Sub Goal (under Edit) and enter (F.G) as the New Sub Goal. There is a Help movie showing this: New Sub Goal.