1/10/2020
Skills to be acquired:
Learning reductio proof, both as plain Negation Introduction and via (double) Negation Elimination (to prove some formulas that do not have negation as their main connective).
Reading
Bergmann[2004] The Logic Book Section 5.1 and 5.4
The Tutorial:
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 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.
∼I is implemented to two slightly different ways, and you can take your choice among them. The first uses the propositional constant Absurd -- this implementation is easier to understand, makes simple derivations using ∼I one line longer, can make more difficult derivations using ∼I 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 propositional 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.
Notice that the formulas that lead to Absurd contradict each other. Returning to Reductio ad Absurdum and the Rule for the Introduction of Negation...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
|
1
|
G
|
Ass
|
|
2
|
? |
? <<
|
|
3
|
~G
|
?
|
Second you continue deriving in this new context until you manage to derive Absurd thus
Finally you select Absurd and click ∼I to complete the Reductio proof.
(Remarks for experienced logicians. The second implementation of ∼I is similar except that you omit the step for introducing Absurd-- merely by adding an assumption, eventually selecting two formulas, one of which being the negation of the other, and clicking ∼I, will add the negation of the assumption. Use this if you wish to. On the face of it this method might seem better, but it runs into awkwardnesses when combined with other rules that involve subproofs-- experts might care to think over derivations like F∨G,∼F,∼G ∴ ∼H or (∀x)∼Fx∴∼(∃x)Fx. Part of the problem is that this style of Reductio uses two lines, whereas subproofs are exited with one line, so contrivances are needed.)
(Another remark: The Logic Book insists that the contradictory formulas, say Q and ~Q, actually appear in subproof explicitly. 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 or Repeat (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. So, if you wish to follow The Logic Book style, you can certainly do that.)
There is a second technique based on Reductio and ∼I, and it can be used to prove formulas which do not have a negation as their main connective. Consider this, admittedly advanced, proof of ∴ 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.
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
Second you continue deriving in this new context until you manage to derive two formulas, any two formulas, which contradict each other thus
[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.
So, our example advanced proof of ∴ F∨∼F, would go through as follows
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.
Exercises to accompany Tutorial 8
Exercise 1 (of 4)
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 2 (of 4)
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)
Exercise 3 (of 4)
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 a double negation, then using (double) Negation Elimination to get the desired formula. 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
Exercise 4 (of 4)
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)
If you decide to use the web application for the exercises you can launch it from here Deriver[Bergmann] — username 'logic' password 'logic'. Then either copy and paste the above formulas into the Journal or use the Deriver File Menu to Open Web Page with this address https://softoption.us/test/easyDeriver/CombinedExercisesEasyDBergmann.html .
Preferences
You may need to set some Preferences for this.
- you can check that the parser is set to bergmann.