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 U⊈V then ∀X(X⊆V→U⊈X).
Choose New Theorem from the File menu in the Proof Designer window. A dialog box will open, asking you to type in the hypotheses and conclusion of the theorem you want to prove. Type U⊈V (to type the “not a subset” symbol, click on the ⊈ button in the symbol palette at the top of the dialog box). Click the Add Hypothesis button, and the statement U⊈V will appear in the list of hypotheses. Now type ∀X(X⊆V→U⊈X) and click on the Set Conclusion button. When you have the hypothesis and conclusion entered correctly, click OK.
The statement of the theorem will appear in the Proof Designer window, followed by the word “Proof:” and then a summary of what you know (“Givens”) 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, it has a pink background, 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 pink boxes with a ? button in the upper left corner.
Note: There are keystrokes you can use to type mathematical symbols, rather than using the buttons on the symbol palette. You can find a complete list of these keystrokes here. If you enter the hypothesis incorrectly, you can click on it to select it, click the Cut Hypothesis button, and then enter the hypothesis correctly. If you enter the conclusion incorrectly, just enter the correct one and click the Set Conclusion button again; the new conclusion will replace the old one.
Since the goal starts with ∀X, the best way to proceed is to let X stand for an arbitrary object. Click on the statement ∀X(X⊆V→U⊈X) under the heading “Goal” to select it. Now choose the Arbitrary Object command from the Goal menu. A dialog box will appear, asking what name you would like to use for the arbitrary object. The default choice X will already be filled in. Click OK.
Note: When an instruction tells you to select a statement, be sure to select only that statement and no others. If you accidentally select the wrong statement, or you select an extra statement in addition to the right one, you can click on the mistakenly selected statement again to deselect it.
The window containing the proof will get updated. Proof Designer will create a subproof in which X is introduced as an arbitrary object. To finish the subproof, you must prove the statement X⊆V→U⊈X. The declaration of X as an arbitrary object only applies to steps inside the subproof; outside the subproof, X 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 X was arbitrary, we can conclude that ∀X(X⊆V→U⊈X).
Note: If you make a mistake, you can use the Undo command in the Edit Menu.
The goal is now an if-then statement. We'll prove it using a direct proof. Select the goal and choose Direct from the Goal menu. Proof Designer will introduce another subproof, nested inside the first, in which it is assumed that X⊆V, and you must prove that U⊈X. This subproof justifies the conclusion that X⊆V→U⊈X. The subproof is set off from the rest of the proof to indicate that the assumption X⊆V only applies within the subproof.
To proceed further, we need to work out the logical form of the goal. Select the goal U⊈X and 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∈U→a∈X) (applying the definition of ⊈, of course). This is a negative statement, and it will be easier to work with it if we reepxress it as a positive statement, so click on the Reexpress Negative button, and the statement will be reexpressed again as ∃a¬(a∈U→a∈X). The subexpression ¬(a∈U→a∈X) will be highlighted, and this is another negative statement, so you can click the Reexpress Negative button again to rewrite the statement as ∃a(a∈U∧a∉X). Click OK.
The final reexpression ∃a(a∈U∧a∉X) will be listed as a variant of the original goal U⊈X. 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.
Note: In the Reexpress dialog box, you can apply reexpressions to any meaningful subexpression of the statement. Just select the subexpression you want to reexpress by dragging your mouse over it and then click the appropriate button.
Since the new variant of the goal starts with ∃a, we will try to prove it by finding a value to plug in for a. To do this we will have to look more closely at the givens. The best one to start with is U⊈V, since it can also be reexpressed as a statement starting with ∃, and it is always best to use a given that starts with ∃ immediately. So select the given U⊈V and imitate the procedure from the last step to reexpress it in the form ∃a(a∈U∧a∉V).
Shortcut: double-clicking on a statement is equivalent to selecting it and choosing the Reexpress command.
When you know something exists, you should always give it a name. So click on the new given variant ∃a(a∈U∧a∉V) to select it and choose Existential Instantiation from the Infer menu. A dialog box will appear, asking what name you want to give to the object that is asserted to exist. It might be best to use something other than a, to avoid confusion with the other uses of the letter a in the proof, so let's use c. Enter c in the dialog box, and then click the OK button. The statement c∈U∧c∉V will get added to the givens list.
Select the new given c∈U∧c∉V and choose Split Up from the Infer menu. Proof Designer will split this statement into the two statements c∈U and c∉V, both of which will appear in 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 a to prove the goal. Looking at the givens, you might see that the right choice is a=c. So select the goal variant ∃a(a∈U∧a∉X) and choose Existence from the Goal menu. A dialog box will appear, asking you what value should be plugged in for a to make the goal true. Choose the "Use this value" option (it will already be selected), type in c, and click the OK button. The proof will get updated to say that you now have to prove c∈U∧c∉X.
The goal is now a conjunction. To prove it, select the goal c∈U∧c∉X and choose Conjunction from the Goal menu. Proof Designer will create two gaps, because you have to prove two statements to complete the proof. In the first gap, your goal is to prove c∈U, and in the second, you must prove c∉X. You can work on the gaps in either order.
Fortunately, we already know c∈U, so let's deal with the first 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 c∈U in the first gap and give the Finish command from the Edit menu. The first gap will disappear.
We will have to do a few more steps to prove the goal of the other gap, c∉X. Of course, it will follow from the givens X⊆V and c∉V. Click on the given X⊆V and use the Apply Definition button in the Reexpress dialog box to write it out as ∀a(a∈X→a∈V).
Select the new given variant ∀a(a∈X→a∈V) and choose the Universal Instantiation command in the Infer menu. This command lets you plug in anything you want for a in the statement a∈X→a∈V. A dialog box will appear, asking what you would like to substitute for a. In this case you want to substitute c for a, so choose the "Use this value" option, type in c, and click the OK button. The new given c∈X→c∈V will appear in the givens list.
Click on the new given c∈X→c∈V to select it, and then click on the given c∉V to select it as well. Choose Modus Tollens from the Infer menu. Proof Designer will draw the inference c∉X.
Note: When selecting two statements, you can click on them in either order.
The proof is now complete, since the desired goal, c∉X, was just inferred in the last step. Select the given c∉X 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.
Note: If you want to print your proof, you can use your browser's Print command.
Let's try doing the end of the proof a different way. Undo your last two steps by choosing first Undo Finish and then Undo Modus Tollens from the Edit menu. You should be back to the point where your goal was to prove c∉X.
Since your goal is a negative statement, a natural way to proceed is to use proof by contradiction. Select the goal c∉X and choose Contradiction from the Strategy menu. Proof Designer will create a subproof in which it is assumed that c∈X and you must derive a contradiction.
Select the givens c∈X→c∈V and c∈X and choose Modus Ponens from the Infer menu. Proof Designer will infer c∈V.
The proof is now complete, because you have two givens that contradict each other. Select the givens c∈V and c∉V and choose Finish from the Edit menu.
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.