The Existence command can only be used when you
have a goal of the form ∃*x* *P*(*x*).
If you select a goal
of this form and give the Existence command, then a dialog box will
open, asking you what value should be substituted for *x* to make
*P*(*x*) true. If you know what value you want to use for
*x*, type it into the “Use this value” box and click OK. Proof
Designer will then say that you must prove *P*(*x*) for this
value of *x* in order to complete the proof.

If you don't know what
value you want to use for *x*, you can use the “Use this new
variable, whose definition will be inserted later” box. A default
variable may be filled in already, but you can change it if
you want to. You must choose a variable that is not already in use in the
proof to stand for something else. If you choose this option, then Proof
Designer will insert a new gap into the proof in which you must give a
definition of the variable you chose, and then it will say that you must
prove that *P* is true of the object named by that variable. Thus,
there will now be *two* gaps in the proof: one for the definition
of the new variable, and one for the proof that *P* is true for the
value assigned to that variable. You can work on these two gaps in either
order. In particular, you may find it useful to work on the proof that
*P* is true until you reach the point where you know what value
should be assigned to the variable, and then go back and fill in the
definition of the variable. Hint: If, in the course of working on the
proof that *P* is true, you decide to make an inference from some of
the givens, you may want to make that inference in the *first* gap;
after all, the inference may turn out to play a role in the definition of
the variable, so you may want it to be available to be used in the gap in
which that definition must be filled in.

If your goal starts with several existential quantifiers in a row, then you can handle as many of them as you want in one step. For each quantifier, you can choose to use either the “Use this value” box or the “Use this new variable” box. Make your choice for the first quantifier, and then click the Next button. Proof Designer will fill in the value or variable you selected and then ask what you want to do for the next quantifier. Once you have made your choice for the last quantifier you want to deal with, click OK.

The instructions above also apply if you have a goal of the form
∃*x*∈*A* *P*(*x*), but in this case there is
also a shortcut you can use. If you have a goal of this
form, and you also have a given of
the form *y*∈*A*, then you may
select both and give the Existence command. No dialog box will open, and
Proof Designer will say that you must prove *P*(*y*)
in order to complete the proof.