12/16/06
Proving an argument to be valid by displaying a derivation. Carrying out simple propositional derivations using some of the Rules of Inference.
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 applet for doing derivations. And we are now going to look at proof 1 F,F⊃G ∴ G.
Proof applet
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. To select two lines, you click on the first, then, while pressing the command-key (which is the clover-leaf key, if you are on a Macintosh), click on the second line. 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 clicking M.P.)
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, click Derive It under the Wizards Menu to get a proof we can look at.
This is the proof.
1. F 2. G.H 3. H.G 2 Com. 4. H 3 Simp. 5. F.H 1,4 Conj.
Let us analyse the result.
We have a sequence of lines. For example, one of the lines is
4. H 3 Simp.
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 4 was obtained from line 3 using the Rule of Inference 'Simp'. Simplification is a Rule which allows you to break a formula with . as its main connective into one of its components.
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.
This will become clearer with a few examples.
Each of the derivations in the following Exercise can be done using only one rule, Simplification.
If the formula in a line in a derivation has the form
<left-formula>.<right-formula>
the Rule of Simplification (Simp) allows you to remove the conjunction (the 'and') and add
<left-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.G ∴ F
b) (G.F).(F.H) ∴G
c) F,(H.G).(F.H),I ∴H
Proofs
Each of the derivations in the following Exercise can be done using only two rules, the Rule of Conjunction (Conj), and Simp (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 Conj 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 Conj (off the Rules Menu). You choose whether the first formula is to go on the left or on the right. (It is possible, though rare, for <formula1> and <formula2> to be the same formula on the same line, in which case this rule to be used on a single line and only one line need be selected.)
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,I,H ∴ (F.I).(F.H)
c) F,G,H ∴ (F.G).(F.H)
d) F ∴ F.F
Proofs
Each of the derivations in the following Exercise can be done using only three rules, the Rule of Addition (Add) and Simp and Conj (learned previously).
If the formula in a line of a derivation has the form
<formula>
the Rule of Addition (Add) allows you to add
<formula>∨<newformula>
To use this Rule, select a formula <formula> and click Add. The program will ask you what you want as the <newformula>.
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) G.G ∴ G∨F
c) F.G ∴ F ∨H
d) F,G ∴(F.G)∨H
Proofs