If you have a given of the form *xP*(*x*), then
you can infer that *P*(*x*) is true for any value of *x*
that you choose. Select the given and give the Universal Instantiation
command, and a dialog box will open asking what value
you would like to assign to *x*. 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 infer that *P*(*x*) is true for this
value of *x*.

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 infer 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 goal that you were originally
working on proving. You can work on these two gaps in either
order. In particular, you may find it useful to continue working on
proving your goal 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 of your goal, 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 given starts with several universal 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 given of the form
*x**AP*(*x*), but in this case there is
also a shortcut you can use. If you have a given of this
form, and you also have a given of
the form *y**A*, then you may
select both and give the Universal Instantiation command. No dialog box will
open, and Proof Designer will infer *P*(*y*).