If you have a given of the form ∀x P(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∈A P(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).