2013
Skills to be acquired:
Learning the Rules Or Elimination and the Introduction of the Biconditional.
The Tutorial:
Or Elimination, in the guise of Dilemma, also is a form of inference dating from antiquity.
The core idea of it that if a conclusion follows from both disjuncts of a disjunction, then the conclusion follows full stop. As an example in English, if either I am going to eat an ice-cream or I am going to eat some cake, and if I eat ice-cream I break my diet, and if I eat cake I break my diet, then ... I break my diet.
In our rule system dilemma appears as the rule for the Elimination of Disjunction ∨E. This, then, is a rule which gets used when you have a formula which has disjunction as its main connective and are trying to obtain some other formula.
The circumstance that Elimination of Disjunction gets invoked looks like this.
That is, a formula you have has a ∨ as its main connective-- the formula you have has the form <left disjunct> ∨ <right disjunct>. In the illustration, for example, F is the <left disjunct> and G is the <right disjunct>. And there is a <target> which is the formula you are trying to obtain. In the illustration H is the <target>.
You follow a five stage process. First you assume the <left disjunct>. The illustrated fragment will then become
Second you continue deriving in this new context until you manage to derive <target> thus
Third you drop the assumption of the <left disjunct> and assume instead the <right disjunct>. You do this by clicking the Rule Assumption, entering the <right disjunct>. and choosing 'Drop Last' . The illustrated fragment will then become
Fourth, you continue deriving in this new context until you manage to derive <target> thus
Finally you select three items -- the disjunct formula, and the last lines of the two sub-proofs (each with the same <target> formula on them) and click ∨E to complete the Or elimination.
The final propositional Rule--the Introduction of the Biconditional-- is similar to two conditional proofs, one going the left to right, and the other from right to left. It gets used when you are trying to obtain a biconditional formula.
The circumstance it gets invoked looks like this.
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 <left> ≡ <right>. In the illustration, for example, F is the <left> and G is the <right> .
You follow a five stage process. First you assume the <left>. The illustrated fragment will then become
Second you continue deriving in this new context until you manage to derive the <right> thus
Third you drop the <left> assumption and instead assume the <right>. You do this by clicking the Rule Assumption, entering the <right>. and choosing 'Drop Last' . The illustrated fragment will then become
Fourth you continue deriving in this new context until you manage to derive the <right> thus
Finally you select the last lines of the two subproofs (that is, <right> and <left>) and click ≡I to complete the Biconditional Introduction.
-->
Exercises to accompany Tutorial 9
Exercise 1 (of 5).
Derive the following using Tactics. (Start the derivation, switch Tactics on, select the disjunt formula, and click ∨E-- this will lay out the derivation for you.) Then repeat the derivations without using Tactics.
a) F∨G,F⊃H,G⊃H∴H
b) (F∧F)∨(G∧G),F⊃H,G⊃H∴H
c) F∨G ∴G∨F
d) (F⊃G)∧(H⊃D), F∨H ∴ G∨D
Exercise 2 (of 5). (*slightly more difficult*)
Derive the following.
a) F∨(G∧∼G)∴ F
b) F∨G, G⊃H ∴ ∼F⊃H
c) ∼F∧∼G∴ ∼(F∨G)
Exercise 3 (of 5). (*slightly more difficult*)
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
De Morgan's Laws
a) ∴ (∼F∧∼G)⊃∼(F∨G)
Distribution
b) ∴ (F∧(G∨H))⊃((F∧G)∨(F∧H))
c) ∴ ((F∨G)∧(F∨H))⊃(F∨(G∧H))
d) ∴ (F∧(G∨H))⊃((F∧G)∨(F∧H))
e) ∴ ((F∨G)∧(F∨H))⊃(F∨(G∧H))
Implication
f) ∴ (∼F∨G)⊃(F⊃G)
Exercise 4 (of 5).
Derive the following with or without Tactics. (Start the derivation, switch Tactics on, and click ≡I --this will lay out the derivation for you.) Then do the derivations without using Tactics.
a) (F⊃G)∧(G⊃F) ∴ F≡G
b) ∴ (F∧F)≡F
c) ∴ (F∨F)≡F
Exercise 5 (of 5).
There are a number of well-known theorems which express equivalences between formulas, derive them
Association
a) ∴ F∨(G∨H)≡(F∨G)∨H
b) ∴ F∧(G∧H)≡(F∧G)∧H
Commutation
c) ∴ F∨G≡G∨F
d) ∴ F∧G≡G∧F
De Morgan's Laws
e) ∴ ∼(F∧G)≡∼F∨∼G
f) ∴ ∼(F∨G)≡∼F∧∼G
Distribution
g) ∴ F∧(G∨H)≡(F∧G)∨(F∧H)
h) ∴ F∨(G∧H)≡(F∨G)∧(F∨H)
Double Negation
i) ∴ F≡∼∼F
Equivalence
j) ∴ (F≡G)≡(F⊃G)∧(G⊃F)
k) ∴ (F≡G)≡(F∧G)∨(∼F∧∼G)
Exportation
l) ∴ (F⊃(G⊃H))≡((F∧G)⊃H)
Implication
m) ∴ F⊃G≡∼F∨G
Transposition
n) ∴ F⊃G≡∼G⊃∼F
If you decide to use the web application for the exercises you can launch it from here Deriver [Gentzen] — 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/CombinedExercisesEasyDGentzen.html .
Preferences
You may need to set some Preferences for this.
- you can check that the parser is set to gentzen.