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.