10/12/26
Skills to be acquired:
Learning conditional proof, and indirect proof.
The Tutorial:
There are two additional sentential rule of inference-- Conditional Proof and Indirect Proof (Reductio ad absurdum)-- which are slightly more difficult than the ones that we have met before. They are slightly more difficult in that they require 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
Indirect Proof (IP) is the second of the classical forms of inference (it is traditionally known as Reductio ad Absurdum).
The idea of it is the following. In a valid argument the truth of the premises guarantees the truth of the conclusion or, to put it another way, the falsity of the conclusion guarantees the falsity of at least one of the premises. Some formulas are sure to be false; contradictions, for example, like (A.∼A). So, if you can derive a contradiction from just one premise, that proves the premise to be false. But proving that a statement is false is exactly the same as proving that the negation of that statement is true. To sum up, one way of proving the negation of a statement is to assume the statement and derive a contradiction from that assumption. This process is known as Reductio ad Absurdum, and one early example of its used was in the discovery of irrational numbers back in Greek times (the mathematical theorem 'It is not the case that there are two natural numbers such that one divided by the other equals the square root of two' was proved by assuming 'There are two natural numbers such that one divided by the other equals the square root of two' and deducing a contradiction from this assumption).
In our rule system Reductio ad Absurdum appears as the rule for Indirect Proof (IP).
IP is implemented to two slightly different ways, and you can take your choice among them. The first uses the sentential constant Absurd -- this implementation is easier to understand, makes simple derivations using IP one line longer, can make more difficult derivations using IP many lines shorter, and fits better with the use of Tactics. It is the recommended implementation for beginners. The other will be described briefly later.
As a preliminary, let us look at another Rule, the one for the Introduction of Absurdity. Our logical system contains the sentential constant Absurd which may be derived from any pair of formulas one of which is the negation of the other; in other words, the pair of formulas must contradict each other and if they do Absurd may be derived. The Introduction of Absurdity is just like the And Introduction except that the conjuncts must contradict each other. Here are some proof fragments illustrating the introduction of Absurd.
1 F p 2 ∼F p 3 Absurd 1,2 AbsI
1 ∼(H⊃J) p 2 H⊃J p 3 Absurd 1,2 AbsI
Notice that the formulas that lead to Absurd contradict each other. Returning to IP...the circumstance it might be invoked looks like this:
? ? << G ?
The formula you are trying to obtain has the form <formula>. In the illustration, for example, G is the <formula>. Now, every formula has this form, which amounts to 'anything goes'. This means that IP could always be used. And indeed it can. But often there are other easier proofs than an IP one.
Good advice here is: do not look at IP unless you are truly struggling to find a straightforward proof.
With IP, you follow a three stage process. First you assume the 'opposite' of what you want to prove-- 'opposite' here means negation. The first illustrated fragment, for example, will then become
->~G AP ? ? << G ?
Second you continue deriving in this new context until you manage to derive Absurd thus
->~G AP
<proof fragment in here> ? n
Absurd ? ? ? << G ?
Finally you select Absurd and click IP to complete the Indirect Proof.
->G AP
<proof fragment in here> ? k
Absurd ? k+1 ∼G k IP
If you prefer not to use Absurd, for the Second part you continue deriving in this new context until you manage to derive a contradiction (which is the conjunction of a formula and its negation, for example F.~F), thus
->~G AP
<proof fragment in here> ? n
F.~F /*this could also be ~F.F */ ? ? ? << G ?
Finally you select the contradiction and click IP to complete the Indirect Proof.
->G AP
<proof fragment in here> ? k
F.~F ? k+1 ∼G k IP
(Remarks for experienced logicians. There is a second implementation of IP which is similar except that you omit the step for introducing the contradiction-- merely by adding an assumption, eventually selecting two formulas, one of which being the negation of the other, and clicking IP, will add the assumption, without its negation sign. Use this if you wish to.)
As an example, consider this, admittedly advanced, proof of ∴ F∨∼F. Here ~( F∨∼F) has been assumed as the 'opposite' of what is sought
1
->∼(F∨∼F) AP 2
->F AP 3
F∨∼F 2 Add 4
Absurd 3,1 AbsI
5
∼F 4 ∼I 6
F∨∼F 5 Add 7
Absurd 1,6 AbsI 8 F∨∼F 7 IP
So, briefly put, if you embark on an IP, you assume the 'opposite' of what you want to prove. If you want to prove <formula> you assume ∼<formula>.
Exercises to accompany Tutorial 9
Exercise 1 (of 7)
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))
Exercise 2 (of 7)
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*)
Exercise 3 (of 7)
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))
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.
Exercise 4 (of 7)
There is a Rule for Absurdity Introduction-- in effect it is just And Introduction, but with the requirement that the conjuncts contradict each other. To use it you select a formula, and select the negation of that formula, and choose Absurd I.
Derive the following, either with or without Tactics. (Tactics will ask to you choose where the contradiction will come from; but it also gives you a hint as to the possibilities by listing all potential positive conjuncts.)
a) F, ∼F ∴ Absurd
b) F, F⊃∼F ∴ Absurd
c) F,G,∼(F∧G) ∴ Absurd
d) F, ∼(F⊃F) ∴ Absurd
Exercise 5 (of 7)
[Hausman 5-3]
Derive the following. First use Tactics. Start the derivation, switch on Tactics under the Wizard, then click IP to lay out the derivation properly. Then repeat the derivations without using Tactics.
[Any theorem can be proved by IP (although it is not always best to do so). And use of the Replacement Rules also widens possibilities. If there is one derivation, there are infinitely many different derivations of the same theorem; and, with the use of IP and Replacement, there are infinitely many derivations 'of different kinds' of the same theorem. One repercussion of this is that if you use the Theorem Prover (Derive It) to get some ideas on a proof, you may get a proof quite different to anything you imagined-- sometimes this proof will be better than one you had in mind, often it will be worse. This apparent shortcoming of theorem proving is unavoidable in the general case.]
a) A∨B, A∨~B ∴ A
b) ~A ⊃B, ~(~A.B) ∴ A
c) A ⊃(B.C), ~B ∴ ~A
d) A ∨ (~B.C), B ⊃~A∴ ~B
e) A ⊃~B, B∨C, A∨C∴ C
Exercise 6 (of 7)
Use Tactics if you wish. (Start the Proof, Switch on Tactics, Choose IP, That will lay the proof out correctly.)
a) (A.B) ⊃C, ~A⊃C,B ∴ C
b) A ⊃B, C ⊃D, (B∨D)⊃E,~E ∴ ~(A∨C)
c) A ⊃(B ⊃C), A ⊃B,~C⊃(A∨D)∴ C∨D
d) ~A, (A∨B)≡C,~B ∴ ~(C.D)
e) C ⊃(D∨~(A∨B)), ~A ⊃B∴~D⊃~C
Exercise 7 (of 7)
[Hausman 5-4 ]
Derive the following theorems twice-- once using IP or CP and once without using either of those rules. [This is a test!]
a) A⊃B, C ⊃A,C ∨(B.D) ∴ B
b) H ⊃ (A⊃ B), ~C ⊃ (H∨B), H ⊃ A ∴ C ∨ B
c) P∨Q, Q ⊃ (R.S), (R∨P)⊃ T ∴ T
d) (R ⊃ M)⊃ L, (N∨S)⊃ (M.T ), (P⊃ R)⊃ L, (T∨K)⊃ ~N ∴ L
e) H ⊃(A.B), B ⊃(M∨~A) , M ⊃(~A∨~B) ∴~H