Tutorial 5. Valid arguments, searching for a proof.
Under construction 2013
Skills to be acquired in this tutorial:
Proving an argument to be valid by displaying a derivation. Simple propositional derivations using some of the Rules of Inference.
The Tutorial:
If you suspect that an symbolized argument might be valid, you should attempt to give a derivation of it.
A derivation is a proof of validity.
We will do a few derivations first, then, in the next Tutorial, explain in more detail what derivations are and how derivations do the work they should.
We use a Proof widget for doing derivations. And we are now going to look at proof 1 F,F⊃G ∴ G.
Proof widget <Press the Proof1 Button>
The Proof panel contains a number of items. In the middle there is the proof itself. There are the premises, a ? to indicate the missing proof, and the target conclusion. Notice that line 3 has << next to it; this means that any new lines will be added here. If one of the new lines being added equals the target conclusion the ? is removed (you have finished, there is no missing proof.)
Lines are selected by clicking on them (or touching them on a touchscreen). They toggle on and off, with clicking or touching, to select and de-select. The Rules Menu contains the Rules of Inference. You first select the desired lines, then choose the Rule. (Try selecting line1 and line 2 and choosing ⊃E off the Rules Menu.)
Now look at Proof 2
F,G∧H ∴ F∧H
We want to have a look at the structure of a completed proof. Fortunately, the program can do proofs for you, choose Derive It under the Wizards Menu to get a proof we can look at.
This is the proof.
Let us analyse the result.
We have a sequence of lines. For example, one of the lines is
|
3
|
H |
2 ∧E
|
Each of the lines in the sequence has a number so that we know which line we are talking about. Each line has a formula on it. And over the right-hand side there is the justification of the line. The justification consists of two components: zero or more numbers, and the name of a Rule of Inference. The zero or more numbers refer to zero or more lines that were used to get the current line using the named Rule of Inference. In the example, line 3 was obtained from line 2 using the Rule of Inference ∧E. ∧E is the Rule of Inference And Elimination which is a Rule which allows you to break a formula with ∧ as its main connective into one of its components.
There is one other item in the example proof-- it is the vertical line between the line number and the formula. The function of this will be explained later.
To continue...
When you start a proof, the program writes down the premises of the argument as the opening lines of a derivation. Then there are Rules of Inference which allow you the option of adding various further lines. Roughly speaking the Rules fall into two types: those that allow you to eliminate a main connective, and those which allow you to introduce a main connective. So, for example, the connective ∧ has two Rules associated with it:- And Introduction (∧I) and And Elimination (∧E). The task in derivation is to use the rules in such a way that the conclusion gets added as a line (in the context of the same opening assumptions). In short, if you can manipulate the Rules and lines so as to add the conclusion of the argument you are considering, you will have proved that argument to be valid.
This will become clearer with a few examples.
Exercises to accompany Tutorial 5
Exercise 1 (of 4)
Each of the derivations in the following Exercise can be done using only one rule, the Rule of Elimination of Negation ∼E.
If the formula in a line in a derivation has the form
∼∼<formula>
the Rule of Elimination of Negation ∼E allows you to remove
both negations and add
<formula>
as an extra line.
Show each of the following arguments to be valid. If you are stuck, ask the program to do one line for you (choose Next Line under the Wizard Menu); then, having seen what the next line is, go to the Edit Menu click Undo Next Line and try to do it yourself.
a) ∼∼F∴F
b) (∼(∼F))∴F
c) F, ∼∼∼∼G,H∴G
Exercise 2 (of 4)
Each of the derivations in the following Exercise can be done using only two rules, the Rule of Elimination of Conjunction ∼∧, and ∼E (learned previously).
If the formula in a line in a derivation has the form
<formula1>∧<formula2>
the Rule of Elimination of Conjunction ∧E allows you to remove the conjunction and add either
<formula1>
or
<formula2>
as an extra line. You have a choice here (whether to take the left conjunct or the right conjunct)-- you will be asked to choose.
Show each of the following arguments to be valid. If you are stuck, ask the program to do one line for you (choose Next Line under the Wizard Menu); then, having seen what the next line is, go to the Edit Menu click Undo Next Line and try to do it yourself.
a) F∧G ∴ F
b) F∧G ∴ G
c) ∼∼((F∧G)∧(F∧H)) ∴ F∧G
d) F,(F∧∼∼G)∧(F∧H),H ∴ G
Exercise 3 (of 4)
Each of the derivations in the following Exercise can be done using only three rules, the Rule of Introduction of Conjunction ∧I, and ∼E and ∧I (learned previously).
If the formula in a line of a derivation has the form
<formula1>
and a formula in a line of a derivation has the form
<formula2>
the Rule of Introduction of Conjunction ∧I allows you to add
<formula1>∧<formula2>
To use this Rule, select two formulas <firstformula> and <secondformula> (*note that the way you select a second formula is to press the command key (clover leaf on a Macintosh) and then click on the line*) and click ∧I. You choose whether the first formula is to go on the left or on the right.
Show each of the following arguments to be valid.
If you are stuck, ask the program to do one line for you (choose Next Line under the Wizard Menu); then, having seen what the next line is, go to the Edit Menu click Undo Next Line and try to do it yourself.
a) F,G ∴ G∧F
b) F∧G,F,∼∼H ∴ (F∧G)∧(F∧H)
c) F,G,H ∴ (F∧G)∧(F∧H)
d) F ∴ F∧F
e) F∧(G∧H) ∴ (F∧G)∧H
f) (F∧G)∧(F∧H) ∴ F∧(G∧H)
g) F,G∧H,(A∧B)∧C ∴ (A∧G)∧F
Exercise 4 (of 4)
Each of the derivations in the following Exercise can be done using only four rules, the Rule of Introduction of Disjunction ∨I, and ∼E, ∧E, and ∧I (learned previously).
If the formula in a line of a derivation has the form
<formula>
the Rule of Introduction of Disjunction ∨I allows you to add
<formula>∨<newformula>
or to add
<newformula>∨<formula>
To use this Rule, select a formula <formula> and click ∨I. The program will ask you what you want as the <newformula>. The program will also ask you whether the <newformula> is to go on the left or on the right.
Show each of the following arguments to be valid.
If you are stuck, ask the program to do one line for you (choose Next Line under the Wizard Menu); then, having seen what the next line is, go to the Edit Menu click Undo Next Line and try to do it yourself.
a) F ∴ F∨G
b) F ∴ G∨F
c) F∧G ∴ G∨H
d) F∧∼∼G ∴ F∧(G∨H)
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.