Quick Start

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 F⊂G then ∪F⊂∪G. You might find it easiest to print these instructions out and then refer to them while you work through this example.

  1. 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 F⊂G 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 F⊂G will appear in the list of hypotheses. Now type ∪F⊂∪G 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.
  2. Click on the statement ∪F⊂∪G 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(a∈∪F→a∈∪G) (applying the definition of ⊂, of course). Click OK. The statement ∀a(a∈∪F→a∈∪G) will be listed as a variant of the original goal ∪F⊂∪G. 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.
  3. 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 a∈∪F→a∈∪G. 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 ∪F⊂∪G.
  4. 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 a∈∪F, and you must prove that a∈∪G. This subproof justifies the conclusion that a∈∪F→a∈∪G. The subproof is set off from the rest of the proof to indicate that the assumption a∈∪F only applies within the subproof.
  5. Click on the goal a∈∪G 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 ∃b∈G(a∈b). Click OK.
  6. 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 a∈∪F, 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 a∈∪F and use the Apply Definition button in the Reexpress dialog box to rewrite it as ∃b∈F(a∈b).
  7. When you know something exists, you should always give it a name. So select the new given variant ∃b∈F(a∈b) 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 a∈X and X∈F will get added to the givens list.
  8. 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!
  9. 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 ∃b∈G(a∈b) 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 X∈G, and in the second, you must prove a∈X. You can work on the gaps in either order.
  10. Fortunately, we already know a∈X, 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 a∈X in the second gap and give the Finish command from the Edit menu. The second gap will disappear.
  11. We will have to do a few more steps to prove the goal of the other gap, X∈G. Of course, it will follow from the givens X∈F and F⊂G. Click on the given F⊂G and use the Apply Definition button in the Reexpress dialog box to write it out as ∀b(b∈F→b∈G).
  12. Select the new given variant ∀b(b∈F→b∈G) and choose the Universal Instantiation command in the Infer menu. This command lets you plug in anything you want for b in the statement b∈F→b∈G. 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 X∈F→X∈G will appear in the givens list.
  13. Click on the new given X∈F→X∈G 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 X∈F to select it as well. Choose Modus Ponens from the Infer menu. Proof Designer will draw the inference X∈G.
  14. The proof is now complete, since the desired goal, X∈G, was just inferred in the last step. Select the given X∈G 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.
  15. 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 commands.

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.