You should now Launch Deriver and do the 3 exercises of Propositional Exercise 8 (Propex8).
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
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)
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
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)