To enter an exercise:
Click on the top button of the proof-checkers toolbar. The toolbar is the vertical column of buttons on the right of the checker.
NOTE: Proof-checker uses the following symbols for the logical connectives:
|
Meaning |
Symbol |
|
|
Conjunction |
...and ... |
. |
|
Disjunction |
Either ... or ... |
+ |
|
Implication |
If ... then ... |
> |
|
Equivalence |
... if and only if ... |
= |
|
Negation |
not |
~ |
M>H
H>L
~L
--------
~M
in the dialog box which has slots for 5 premises and a conclusion.
NOTE: Pressing the Tab key will move the cursor from slot to slot.
Click the 'Accept' button before the 'Close' button.
First example:
Click the button with the question mark icon. A dialog box will give a hint.
On the toolbar click on the stepper button (light bulb icon). Under 'Inference Rules', click on the bar with the wedge. In the drop down list, click on 'MT'. Under 'First Line' click on the bar with the wedge. In the drop down list click on 2. Under 'Second Line' click on the bar with the wedge, In the drop down list click on 3. Click the 'Close' button. The following new line should show as part of the proof: 5. ~H 2, 3 MT.
Repeat the above steps until the proof is complete.
Second example :
For this let's select one of the built in exercises: On the menubar of the proof-checker, click 'Exercises'. In the drop down menu, click 'For: DS, Add'. In the problem selection box, click in the circle to the left of 10. Then click the 'Close' button. . Study the problem and come up with a step in the proof. For example, W can be derived from lines 1 and 2 by DS.
NOTE: At times a dialog box may hide a critical part of the screen. You can easily move the box to another part of the screen. Move the mouse to the dark blue bar at the top of the box. Click and hold down the mouse button, sliding the mouse in the direction you want to move the box.
Now to enter this step so the proof-checker can verify its correctness:
On the toolbar click on the button with the light bulb icon. Under 'Inference Rules', click on the bar with the wedge. In the drop down list, click on 'DS'. Under 'First Line' click on the bar with the wedge. In the drop down list click on 1. Under 'Second Line' click on the bar with the wedge, In the drop down list click on 2. Click the 'Close' button. The following new line should show as part of the proof: 4. W 1, 2 DS
If an invalid step is taken a dialog box will appear: it will attempt to color code the lines and law you selected to help you find your mistake.
For your next step you have decided that the conclusion can now be derived by the rule of Addition. .In the ' Rules' drop down list, click on 'Addition'. In the 'First Line' drop down box, click on 4. In the text slot, labeled 'Enter a Line', enter what is to be added to line 1. In this case: X Then click the 'Close' button.
This is formal proof where an assumption is added to the given premises to facilitate the proof. A beginner's
strategy will be
presented below..
An example:
1. P > Q / P > (P . Q)
2. P assumed
3. Q 2,1 MP
4. P . Q 2,3 Conj
5. P > ( P . Q) 2 - 4 CP
A formal proof, where an assumption is added to the given premises, has 3 components:
1. The premise(s) and conclusion: the above example has one premise and the conclusion follows the slash.
2. An indented area where all the lines ( 2 through 4 in the example above) depend on the assumption which is always the first line in the indented area.
3. Every assumed statement must be discharged before the proof is complete. Line 5 above is the discharged statement whose truth is no longer an assumption.
Another example
If there is no (G)od, then life is (m)eaningless. If life is meaningless, then it makes no sense to continue to (l)ive and it makes equally no sense to commit (s)uicide. If all we have is the choice of whether to live or commit suicide, then existance is truelly (a)bsurd. Hence if there is no God, then existance is absurd.
Translated into Sentential symbolism the argument looks like this: (There are three premises and a conclusion after the slash.)
1. ~G > M
2. M > (L . S)
3. (L + S) > A /~G > A
Click on the top button of the proof-checker's toolbar. Enter the translated version in the slots of the dialog box. After you close the dialog box where you entered the premises and the conclusion, the argument should appear in the white area of the proof-checker. (Do not enter the numbers.)
Constructing a proof with the help of an assumption:
Click on click on the toolbar button with the light bulb icon.
Click on the bar under the assumption label. And click on 'assume' in the drop down list.
In the text slot enter what is to be assumed. (When the conlusion is an implication always start by assuming the antecedent of the conclusion. In this case: type in ~G.)
Click the 'Close' button. An indented line will appear as the first line of the proof. Use ~G as an extra premise and derive the consequent of the conclusion. In this case: A.
This can be realized with the following steps:
Bring up the step box again. Select MP and lines 1 and 5. Click 'Close'.
Bring up the step box. Select MP and lines 6 and 2. Click 'Close'.
Bring up the step box. Select Simp. and line 7. Click Close.
Bring up the step box. Select MP and lines 9 and 3. Click Close. With this last step you have derived A on line 10. Note that all these lines are indented to indicate that they are derived with the help of the assumption. Now we must discharge the assumption:
Bring up the step box. In the Assumption drop down box select CP. Now select lines 5 and 10. Click 'Close'.
So, when the conclusion of an argument is an implication and we choose to use the law of assumption: We assume the antecedent of the conclusion. Use it in conjunction with the premises to derive the consequent of the conclusion. Then we discharge the assumption by making the assumed statement the antecedent and the last statement, in the indented area, the consequent. It is alwas a conditional statement, and it is always identical to the conclusion. Note that the discharged statement is not indented. Our formal proof using assumption is now complete. It is a valid argument where the conclusion has been proven true. Why? The assumed statement ~G is either true or false. If it is false then the statement on line 11 is true because a conditional statement is always true when the antecedent is fals. O the other hand, if the assumed statement, ~G, is true, then the statements on lines 6 through 10 are also true. Therefore the discharged statemnet on line 11 is true because if the assumed statemnet, ~G, is true, then A, the consequent, is also true. Whenever both the the antecedent and the consequent of an implication are true, the entire statement is true.
A formal proof where an assumption is added to the given premises to facilitate the proof. A beginner's strategy
will be
presented below.
Example:
If either (J)ones or his (w)ife paid the insurance premium on time, then the (p)olicy was in effect and the (c)ost of the repairs was covered. If the cost was covered, they would have taken the c(r)uise to Alaska. But they were not able to take the cruise. So, Jones did not pay the insurance premium on time.
In symbolic form the argument looks like this:
1. (J + W) > (P . C)
2. C > R
3. ~R / ~J
Click on the top button of the proof-checker's toolbar. Enter the translated version in the slots of the dialog box. Do not enter the numbers to the left of the prmises. After you close the dialog box, the argument should appear in the white area of the proof checker.
Constructing an indirect proof with the help of assumption:
Click on the last button on the toolbar.
Click on the bar under the assumption label. And click on 'assume' in the drop down list. In the text slot enter what is to be assumed. When the conclusion is a single letter, assume its contradiction. In this case: type in J. Click the 'Close' button. An indented line will appear as the first line of the proof. Use J as an extra premise and derive a contradiction. :
Use the stepper to complete the following::
6. ~C 2, 3 MT
7. (J + W) 5, 0 ADD
8. (P . C) 1, 7 MP
9. P 8, 0 SIMP
10. (C . P) 8, 0 COM
11. C 10, 0 COM
Click on the last button of the toolbar. In the step box select lines 11 and 6. In the inference rules drop down
list select 'Conjuction'. Close the box.
This should add the following line to the proof: 12. (C.~C) 6, 11 CONJ
As soon as you derive a contradiction within the assumption, discharge it: Bring up the step box. Select lines 5 and 12. In the Assumption drop down list, select IP. Close the step box. This should add the following unindented line to the proof: 13. ~J 5 - 13 IP This proves that the conclusion of the argument is true. Why? In the module on a conditional proof, we saw the discharged statement, J > (C . ~C), is true whether the assumed statement, J, is true or false. The consequent, (C . ~C), of the true statement, J > (C . ~C), is self contradictory and therefore false. So J, the antecedent, has to be false. If J is false, then ~J has to be true.
Hints & Tools
Clicking the question mark on the tool bar displays the hint dialog box. Clicking the 'Another Hint' button
on the dialog box
will displays successive hints when a number of steps are possible. Following are some general rules as to which
hints usually
take priority. (Naturally hints that have already been acted upon are skipped.)
1. Any hint that involves a detachment rule (the combination of two lines to derive a third) should be acted apon.
2. A hint that involves the last line derived should be given consideration.
3. Hints involving lines not yet brought into play should be given some weight.
The proof-checker has a set of tools under the 'Tools' menu item. All but the 'Calculator' are fairly intuitive.
Using the calculator:
1. If it is necessary to determine whether two logical expressions (i.e. ~(A>B) and (A.~s)) are logically
equivalent:
Enter the first expression in the first text slot, and the second expression in the second text slot. Press the
'Calculate'
button and the answer will appear in the third text slot.
2. To test and inference: enter the premises in the first text slot, each separated by a single space. Enter
the conclusion
in the second slot. Click the 'Calculate' button. If the answer is equal the inference is valid, otherwise not.