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.