## Infer Menu:

# Existential Instantiation Command

If you have a given of the form *xP*(*x*), then
you can introduce a new variable into the proof to stand for a value of
*x* for which *P*(*x*) is true. Select the given and give
the Existential Instantiation command,
and a dialog box will open asking
what variable you would like to use to stand for the object that is
asserted to exist. You must choose a variable that is not already in use
in the proof to stand for something else. When you click OK, Proof
Designer will add a step to the proof asserting that *P* is true of
the variable you chose.

If the given starts with several existential quantifiers in a row, then you can
introduce several new variables in one step. Choose a variable to
stand for the first object asserted to exist, and then click the Next button.
Proof Designer will fill in the variable you selected and then ask what
name you would like to use for the next object. Once you have
chosen a name for the last object you want to introduce, click
OK.

If your goal is to define some variable, and that variable gets defined
as a result of the Existential Instantiation command, then Proof Designer
will recognize that you have achieved your goal and remove the gap from the
proof.