6/10/07
Learning reductio proof, as Negation Introduction and Negation Elimination.
Bergmann[2004] The Logic Book Section 5.1 and 5.4
Reductio ad Absurdum is the second of the classical forms of inference.
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 primarily as the rule for the Introduction of Negation ∼I. This, then, is a rule which gets used when you are trying to obtain a formula which is a negation. And the contradiction that is derived is not just a single formula, instead it is two formulas which contradict each other (one has to be the negation of the other).
The circumstance that Introduction of Negation gets invoked looks like this.
? ? << ∼G ?
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 ∼<formula>. In the illustration, for example, G is the <formula>.
You follow a three stage process. First you assume the <formula>. The illustrated fragment will then become
G Ass ? ? << ∼G ?
Second you continue deriving in this new context until you manage to derive two formulas, any two formulas, which contradict each other thus
G Ass
<proof fragment in here> ? n
Q ?
<proof fragment in here> ? k
~Q ? ? ? << ∼G ?
[Here we are using Q and ~Q to illustrate the sentences which contradict. But the sentences which contradict do not have to be simple atomic sentences, for example (A&B) and ~(A&B) would do fine. Also, they can appear in either order, for example ~(C&B) followed by (C&B) would be perfectly acceptable.]
Finally you select the two lines that contradict each other and click ∼I to complete the Reductio proof.
G Ass
<proof fragment in here> ? n
Q ?
<proof fragment in here> ? k
~Q ? k+1 ∼G n,k ~I
The Logic Book insists that the formulas Q and ~Q actually appear in subproof. This is by no means necessary from a logic point of view (for example, Q or ~Q could be an assumption of the derivation as a whole-- in which case either sentence would be fine as a component of the contradiction). But this requirement may be desirable for clarity when teaching derivations. To help meet it, there is another rule Reiteration (R) which allows a line to be repeated or reiterated into contexts which that is permitted. So, if Q was one of the assumptions of the proof as a whole, the Rule R allows it to be repeated into the sub-proof.
There is a second technique based on Reductio, and it can be used to prove formulas which do not have a negation as their main connective. Consider this, admittedly advanced, proof aimed at proving ∴ F∨∼F,
1
∼(F∨∼F) Ass 2
F Ass 3
F∨∼F 2 ∨I 4
∼(F∨∼F) 1 R
5
∼F 3,4 ∼I 6
F∨∼F 5 ∨I 7
∼(F∨∼F) 1 R 8 ∼∼(F∨∼F) 6,7 ∼I ? ?<< 9 F∨∼F ?
Notice lines 8 and 9. Line 8 has been obtained by Negation Introduction (or Reductio) ~I. But what is needed is line 9, which is line 8 with the double negation taken out. Many logical systems have a rule to do this. But The Logic Book uses a slightly different approach which shortens the number of steps here.
They have a Rule for Negation Elimination (~E). For this, you assume a formula which has negation as its main connective, derive two formulas that contradict, and then you are entitled to your assumed formula, but without its negation.
Schematically
The circumstance that Elimination of Negation gets invoked looks like this.
? ? << G ?
That is, the formula you are trying to obtain might be any formula. In the illustration, for example, G is the <formula>.
You follow a three stage process. First you assume the ~<formula>. The illustrated fragment will then become
~G Ass ? ? << G ?
Second you continue deriving in this new context until you manage to derive two formulas, any two formulas, which contradict each other thus
~G Ass
<proof fragment in here> ? n
Q ?
<proof fragment in here> ? k
~Q ? ? ? << G ?
[Here we are using Q and ~Q to illustrate the sentences which contradict. But the sentences which contradict do not have to be simple atomic sentences, for example (A&B) and ~(A&B) would do fine. Also, they can appear in either order, for example ~(C&B) followed by (C&B) would be perfectly acceptable.]
Finally you select the two lines that contradict each other and click ~E to complete the Reductio proof.
~G Ass
<proof fragment in here> ? n
Q ?
<proof fragment in here> ? k
~Q ? k+1 G n,k ~E
So, our example advanced proof of ∴ F∨∼F, would go through as follows
1
∼(F∨∼F) Ass 2
F Ass 3
F∨∼F 2 ∨I 4
∼(F∨∼F) 1 R
5
∼F 3,4 ∼I 6
F∨∼F 5 ∨I 7
∼(F∨∼F) 1 R 8 (F∨∼F) 6,7 ∼E
So, briefly put, if you embark on a Reductio, you assume the 'opposite' of what you want to prove. If you want to prove ∼<formula> you assume <formula> and eventually invoke ~I. If you want to prove <formula> you assume ∼<formula> and eventually invoke ~E.
Derive the following. First use Tactics. Start the derivation, switch on Tactics under the Wizard, then click ∼I to lay out the derivation properly. Then repeat the derivations without using Tactics.
a) F ∴ ∼(∼F)
b) F ∴ ∼(∼(∼(∼F))) (*Tactics give you a poor hint here*)
c) ∼F ∴ ∼(F&G)
d) F&∼G ∴ ∼(F⊃G)
e) F&∼G ∴ ∼(F≡G)
f) ∴∼(F&(∼F))
g) C&(∼F), A&((∼G)&B) ∴ ∼(F&G)
Proofs
Derive the following. There is a circumstance in which Reductio is used where the initial target formula in not a negation-- the derivation proceeds by assuming a negation using Reductio to get the desired formula. This is the Rule of the Elimination of Negation. The first derivation that follows is an illustration of this.
Use Tactics if you wish. (Start the Proof, Switch on Tactics, Choose ∼E, Choose ∼I. That will lay the proof out correctly.)
a) F&(∼F) ∴ G
b) ∼(F&G),F,G∴H
c) ∴ F∨∼F (*this is difficult, but important-- learn how to do it*)
d) ∼(F&G)∴∼F∨∼G
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
Double Negation
a) ∴ F⊃∼∼F
Transposition
b) ∴ (F⊃G)⊃(∼G⊃∼F)
c) ∴(∼G⊃∼F)⊃(F⊃G) (*The automatic theorem prover gives a very long winded proof of this due to missing the trick about using reductio to prove the double negation of what you want.*)
De Morgan's Laws
d) ∴ ∼(F&G)⊃(∼F∨∼G)
e) ∴ ∼(F∨G)⊃(∼F&∼G)
Implication
f) ∴ (F⊃G)⊃(∼F∨G)
Proofs