Perhaps the best way to see what Proof Designer does is to work out a
simple example. These instructions will lead you through using Proof
Designer to prove the following theorem: If FG then FG. You might find it easiest to print these
instructions out and then refer to them while you work through this example.
- In the main Proof Designer window, click on the
Write a Proof button. (The first time you do this, there may be a delay
while certain features of Java start up. If there is no Write a Proof
button in the main Proof Designer window, then your computer is probably
not configured correctly to run Proof Designer. Read the instructions for
setting up your computer to use Proof Designer.)
A dialog box will open, asking you to type in the hypotheses and conclusion
of the theorem you want to prove. Type FG and click the Add Hypothesis button. (To type the
subset symbol, , type alt-S (Windows)
or option-S (Macintosh), or click the mouse on the button in the symbol palette at the top of the dialog box.)
If you have made a typographical error and the statement you have typed
doesn't make sense, you will get an error message at this point. Fix the
error and try again. If you typed it correctly, the statement FG will appear in the list of
hypotheses. Now type FG
and click on the Set Conclusion button. (To type the union symbol, , type alt-shift-U (Windows) or
option-shift-U (Macintosh), or use the symbol palette.) If you have
entered the hypothesis incorrectly, you can click on it to select it, click
the Cut Hypothesis button, and then enter the hypothesis correctly. If you
have entered the conclusion incorrectly, just enter the correct one and
click the Set Conclusion button again; the new conclusion will replace the
old one. When you have the hypothesis and conclusion entered correctly,
click OK. A window will appear, containing the statement of the theorem,
the word “Proof:”, and then a summary of what you know
(“Given”) and what you have to prove (“Goal”) in
order to complete the proof. This summary is set off from the rest of the
contents of the window by being indented and enclosed in a box, and in the
upper left corner of the box there is a small button containing a
“?”. (We'll see what the button does later.) As you follow
the instructions below, an outline of the proof will gradually take shape
in this window. “Gaps” in the proof indicating where
additional steps still need to be added will always be indicated in this
outline by summaries like this one, contained in boxes with a ? button in
the upper left corner.
- Click on the statement FG
under the heading “Goal”. It will get highlighted to indicate
that it has been selected. Now choose the Reexpress command from the
Strategy menu. A dialog box will appear displaying the statement you
selected, with buttons allowing you to reexpress the statement in a number
of ways. Click on the Apply Definition button, and the statement will get
reexpressed as a(aFaG)
(applying the definition of , of
course). Click OK. The statement a(aFaG) will be listed as a
variant of the original goal FG. It is equivalent to the original
goal, so proving the statement in either form would suffice to complete the
proof. A variant of a given or goal is always listed below it, indented,
with an open circle in front of it rather than a bullet.
- Since the new variant of the goal starts with a, the best way to proceed is to let a stand
for an arbitrary object. Click on the new variant of the goal to select
it, and choose the Arbitrary Object command from the Strategy menu. A
dialog box will appear, asking what name you would like to use for the
arbitrary object. The default choice a will already be filled in,
but if you want to use a different name you can just type it in. Click OK.
The window containing the proof will get updated. Proof Designer will
create a subproof in which a is introduced as an arbitrary object.
To finish the subproof, you must prove the statement aFaG.
The declaration of a as an arbitrary object only applies to steps
inside the subproof; outside the subproof, a is undefined. To
indicate this, Proof Designer sets off the subproof from the rest of the
proof by indenting it and enclosing it in a box. In the upper left corner
of the box there is a small button containing the symbol “”. Proof Designer also writes the final
sentence of the proof, saying that since a was arbitrary, we can
conclude that FG.
- The goal is now an if-then statement. You can prove it either by doing
a direct proof, or by proving the contrapositive. In this case a direct
proof is probably easiest, so select the goal and choose Direct from the
Strategy menu. Proof Designer will introduce another subproof, nested
inside the first, in which it is assumed that aF, and you must
prove that aG. This subproof justifies the conclusion that
The subproof is set off from the rest of the proof to indicate that the
assumption aF only applies within the subproof.
- Click on the goal aG and choose Reexpress from the
Strategy menu. (Shortcut: double-clicking on a statement is equivalent to
selecting it and choosing the Reexpress command.) Click the Apply
Definition button again, and the statement will get rewritten as bG(ab).
- Since the goal starts with b,
we must find a value to plug in for b. To do this we will have to
look more closely at the givens. The best one to start with is
aF, since it will also start with when the definition of
is written out, and it is always best to use a given that starts with immediately. So select the given
aF and use the Apply Definition button in the Reexpress
dialog box to rewrite it as bF(ab).
- When you know something exists, you should always give it a name. So
select the new given variant bF(ab) and choose Existential Instantiation from the Infer
menu. A dialog box will appear, asking what name you want to give to the
object that exists. It might be best to use something other than b,
to avoid confusion with the other uses of the letter b in the proof,
so let's use X. Enter X in the dialog box, and then click
the OK button. The statements aX and XF will get added to the givens list.
- Notice that every time you do a step, a little bit gets added to the
proof. This might be a good time to look at what's been written so far.
If you click on the ? button, the givens and goal list will be hidden, and
you can see more clearly how the proof is shaping up. Click on the ?
button again to show the givens and goal again. Similarly, the buttons hide or show the details of the
subproofs they introduce. Try them out!
- We can now say what value should be plugged in for b to prove
the goal. Looking at the givens, you should see that the right choice is
b = X. So select the goal variant bG(ab)
and choose Existence from the Strategy menu. A dialog box will appear,
asking you what value should be plugged in for b to make the goal
true. Choose the "Use this value" option (it should already be selected),
type in X, and click the OK button. The proof will get updated.
There are now two gaps in the proof, because you have to prove two
statements to complete the proof. In the first gap, your goal is to prove
XG, and in the second, you
must prove aX. You can
work on the gaps in either order.
- Fortunately, we already know aX, so let's deal with the second gap first. The goal
of this gap is already among the givens, so there is nothing more to prove,
but Proof Designer does not recognize this automatically. You must tell
Proof Designer that the goal has been achieved. To do this, select the
given aX in the second gap
and give the Finish command from the Edit menu. The second gap will
- We will have to do a few more steps to prove the goal of the other
gap, XG. Of course, it
will follow from the givens XF and FG. Click on the given FG and use the Apply Definition button in the Reexpress
dialog box to write it out as b(bFbG).
- Select the new given variant
b(bFbG) and choose the Universal
Instantiation command in the Infer menu. This command lets you plug in
anything you want for b in the statement bFbG. A dialog box will appear, asking
what you would like to substitute for b. In this case you want to
substitute X for b, so choose the "Use this value" option (as
before, it should already be selected), type in X, and click the OK
button. The new given XFXG will appear in the givens list.
- Click on the new given XFXG to select it, and then
shift-click (i.e., hold down the shift key on the keyboard while
clicking with the mouse) on the given XF to select it as well. Choose Modus Ponens from the
Infer menu. Proof Designer will draw the inference XG.
- The proof is now complete, since the desired goal,
XG, was just inferred in
the last step. Select the given XG and choose Finish from the Edit menu. The last gap
in the proof will disappear, and Proof Designer will congratulate you on
finishing the proof. Notice that the backgrounds of the buttons
introducing subproofs change from gray to white. Subproof buttons always
change from gray to white when their subproofs are completed.
- If you want to print your proof, try giving one of the Export HTML
commands in the Edit menu. This doesn't work on all browsers; for further
information, see the instructions for the Export HTML
You should now have a pretty good idea of what Proof Designer does.
For another example that illustrates some of the more advanced features of
Proof Designer, click here.