8/12/26
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
Should you wish to use the Deriver application for this, see Exercises for Easy Deriver using the Deriver Web Application [Gentzen] . Good advice is: start these tutorials without out it, but if you get to the point of wishing to save some work, then switch to the Deriver Web Application.
Then either copy and paste the above formulas into the Journal or use the Deriver File Menu to Open from URL... with this address https://softoption.us/test/easyDeriver/CombinedExercisesEasyDGentzen.html .