Advanced Features of Proof Designer

The instructions below will lead you through a proof that (A)(B)AB. This proof will illustrate some of the more advanced features of Proof Designer.

Click on the Write a Proof button in the main Proof Designer window. In the dialog box, type (A)(B)AB and click the Set Conclusion button. (To type the power set symbol , type alt-shift-P (Windows) or option-shift-P (Macintosh), or use the symbol palette. To type the arrow , type alt-C (Windows) or option-C (Macintosh), or use the symbol palette.) There are no hypotheses for this theorem. Click OK.
Select the goal (A)(B)AB and choose Direct from the Strategy menu. Proof Designer will suppose that (A)(B) and it will say that you must now prove that AB.
Select the given (A)(B) and choose Reexpress from the Strategy menu. Click on the Apply Definition button, but don't click on OK yet. Proof Designer will rewrite the statement as a(a(A)a(B)). Now use the mouse to select the statement a(A), which appears before the . (You do this just the way you would do it in a word processing program, by dragging the mouse across what you want to select.) Click Apply Definition again and Proof Designer will change a(A) to aA, writing out the definition of power set. Use the same procedure to write out a(B) as aB, and then click OK.
Select the given variant a(aAaB) and choose Universal Instantiation from the Infer menu. When the dialog box appears, say that you want to substitute A for a. Proof Designer will infer AAAB.
Select the given AAAB, shift-click to select the goal AB as well, and choose Modus Ponens from the Infer menu. Proof Designer will use the modus ponens inference rule to work backwards from the goal. Proof Designer will say that you can infer the goal AB by modus ponens from AAAB and AA, but you must still prove AA.
Although you could just fill in the proof of AA where Proof Designer says it is needed, it might be better to indicate somehow that this is a general fact about all sets, and not a fact about this specific set A. To do this, click on the sentence “Suppose (A)(B)” at the beginning of the proof. This selects the entire subproof that is introduced by this sentence, along with the conclusion it justifies. (You can also do this by clicking in the margin to the left of this subproof, or on the conclusion it justifies.) Choose Insert from the Edit menu. This will allow you to insert some new steps before the subproof you have just selected. A dialog box will appear, asking what goal you want to achieve with these additional steps. Click on the choice saying that you want to prove something, and type in x(xx) as the statement you want to prove. (To type , you can type alt-shift-A (Windows) or option-shift-A (Macintosh) or use the symbol palette.) Click OK. Proof Designer will insert a new gap in the proof, whose goal is to prove that x(xx). Note that in the original gap, where you still need to prove that AA, the statement x(xx) is now listed as a given.
It would look better to have the proof of the statement x(xx) set off from the rest of the proof as a lemma. (A lemma is a small theorem that is used to prove another theorem.) To do this, click on the sentence “Proof of x(xx) goes here” at the beginning of the new proof gap. This selects the entire gap. (You can also do this by clicking in the margin to the left of the gap.) Now choose Lemma from the Strategy menu.
You now have two gaps to complete. You can do them in either order. To prove the lemma, you can let x be arbitrary, reexpress xx as a(axax), let a be arbitrary, and then do a direct proof of axax. Note that after you give the Direct command, your goal will already be listed as a given, so you can select the given and give the Finish command. To fill in the second gap, you can apply universal instantiation to the given x(xx) to conclude that AA.
Let's try changing the proof. Click on the final conclusion “Therefore (A)(B)AB”, which selects this conclusion and the subproof that justifies it. Choose Rejustify from the Edit menu. The subproof and conclusion will disappear, and be replaced by a gap that says “Proof of (A)(B)AB goes here”. We can now redo the proof a different way. (Leave the lemma there—we'll need it in this version of the proof too. If you want, you can hide the details of its proof.)
Select the goal (A)(B)AB and choose Contrapositive from the Strategy menu. Proof Designer will suppose that AB, and it will say that you must prove that (A)(B).
Select the goal (A)(B) and choose Reexpress from the Strategy menu. Click on Apply Definition, but don't click OK yet. Proof Designer will reexpress the goal as a(a(A)a(B)). Now click Reexpress Negative and Proof Designer will change this to a(a(A)a(B)). Note that now only (a(A)a(B)) is selected, so you can click Reexpress Negative again to change the statement to a(a(A)a(B)). Click OK.
The goal is now the existential statement a(a(A)a(B)), so you should probably try to prove it by finding an example of a set which is an element of (A) but not (B), but it may not be clear at first what set to use. Here's how you can deal with this situation: Select the goal a(a(A)a(B)) and choose Existence from the Strategy menu. A dialog box will appear, asking what value you want to substitute for a in the goal. Click on the “Use this new variable, whose definition will be inserted later” option. The default choice for the new variable is a, but if you want to use a different name you can just type it in. Click OK. You will now have two gaps in the proof, one labeled “Definition of a goes here”, followed by one labeled “Proof of a(A)a(B) goes here”. As usual, you can work on these gaps in either order. In particular, even before defining a you can start in on the proof that a(A)a(B). When you get far enough in the proof that you can tell what a should be, you can go back and fill in the definition of a.
Select the goal a(A)a(B) and give the Reexpress command from the Strategy menu. Select the statement a(A) and click Apply Definition to change this to aA. Select a(B) and click Apply Definition to change it to aB. You can click Reexpress Negative if you want to change this to aB. Click OK.
Notice now that the goal is aAaB, and one of the givens is AB. This suggests that perhaps you should have defined a to be equal to A. Go back to the gap labeled “Definition of a goes here”, select the goal a = ?, and choose Define from the Strategy menu. A dialog box will appear, containing the statement “Let ___ = ___”. The first blank will already be filled in with the default value a. Fill in the second with A and click OK. The definition of a will be added to the proof, and the gap labeled “Definition of a goes here” will disappear.
Select the goal variant aAaB, pull down the Strategy menu, and move the mouse down to the Substitute command, but don't release the mouse button. A submenu will appear, showing you what substitutions can now be applied. Since we now know that a = A, you can choose to substitute either A for a or a for A. Choose aA from the submenu, indicating that you want to replace a with A. A dialog box will appear. Click on the Substitute button and the substitution will be performed. Click OK.
The goal is now AAAB, and you already have AB in the given column. Select the given AB and the goal AAAB, and choose Conjunction from the Infer menu. Proof Designer will use the conjunction rule of inference to work backwards from the goal. Proof Designer will say that you can infer AAAB from AA and AB, but you still have to prove AA.
Apply universal instantiation to x(xx) to conclude that AA. This is your goal, so you can now use the Finish command to complete the proof.

Note that we introduced the variable a into this proof only because, at the time we introduced it, we didn't know it would turn out to be equal to A. Now that the proof is done, we could improve on it by eliminating all mention of a, and only talking about A. Often you will be able to improve on the proof outline written by Proof Designer. You should use Proof Designer to work out an outline of a correct proof, and then try to improve on it when you write up the final proof.