The instructions below will lead you through a proof that π«(A)βπ«(B)βAβB. This proof will illustrate some of the more advanced features of Proof Designer.
Choose New Theorem from the File menu. In the dialog box, type π«(A)βπ«(B)βAβB. and click the Set Conclusion button. There are no hypotheses for this theorem. Click OK.
Select the goal π«(A)βπ«(B)βAβB and choose Direct from the Goal menu. Proof Designer will suppose that π«(A)βπ«(B) and it will say that you must now prove that AβB.
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 aβA, writing out the definition of power set. Use the same procedure to write out aβπ«(B) as aβB, and then click OK.
Select the given variant βa(aβAβaβB) 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 AβAβAβB.
Select the given AβAβAβB and the goal AβB 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 AβB by modus ponens from AβAβAβB and AβA, but you must still prove AβA.
Although you could just fill in the proof of AβA 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(xβx) as the statement you want to prove. Click OK.
Proof Designer will insert a new gap in the proof whose goal is to prove that βx(xβx). Note that in the original gap, where you still need to prove that AβA, the statement βx(xβx) is now listed as a given.
It would look better to have the proof of the statement βx(xβx) 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(xβx) 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 Edit 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 xβx as βa(aβxβaβx), let a be arbitrary, and then do a direct proof of aβxβaβx. 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(xβx) to conclude that AβA.
Let's try changing the proof. Click on the final conclusion βTherefore π«(A)βπ«(B)βAβB,β 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)βAβB 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)βAβB and choose Contrapositive from the Goal menu. Proof Designer will suppose that AβB, 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 has now been rewritten as 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 variant βa(aβπ«(A)β§aβπ«(B)) and choose Existence from the Goal 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 aβA. Select aβπ«(B) and click Apply Definition to change it to Β¬(aβB). You can click Reexpress Negative if you want to change this to aβB. Click OK.
Notice now that the goal is aβAβ§aβB, and one of the givens is AβB. 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 aβAβ§aβB and choose Substitute from the Strategy menu. A dialog box will appear. In the dialog box, click on the word βSubstituteβ and a menu will appear, showing what substitutions you can apply. Since we now know that a=A, you can choose to substitute either A for a or a for A. Choose aβA from the menu, indicating that you want to replace a with A, and the substitution will be performed. Click OK.
The goal is now AβAβ§AβB, and you already have AβB in the given column. Select the given AβB and the goal AβAβ§AβB, and choose Conjunction from the Goal menu. Proof Designer will say that you can infer AβAβ§AβB from AβA and AβB, but you still have to prove AβA.
Apply universal instantiation to βx(xβx) to conclude that AβA. 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.