Infer Menu:

Existential Instantiation Command

If you have a given of the form xP(x) or ∃!xP(x), then you can introduce a new variable into the proof to stand for a value (or the unique 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 object named by the variable you chose (and, if appropriate, that it is the only such object).

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 y, and y 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. As a shortcut for this, you can select both an existential given statement xP(x) or ∃!xP(x) and the goal y=? and give the Existential Instantiation command. Proof Designer will use y as the name of the object asserted to exist. Since this step achieves the goal of defining y, Proof Designer will remove the gap from the proof.