Strategy Menu:

Arbitrary Object Command

The Arbitrary Object command can only be used when you have a goal of the form xP(x). Use the Arbitrary Object command if you want to prove this goal by letting x stand for an arbitrary object and then proving P(x).

If you select a goal of the form xP(x) and give the Arbitrary Object command, then a dialog box will open, asking you what variable you want to use to stand for the arbitrary object. A default value 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. When you click OK, Proof Designer will create a subproof in which you must prove that P is true for an arbitrary object named by the variable you chose.

If your goal starts with several universal quantifiers in a row, then you can introduce several arbitrary objects in one step. Choose a variable to stand for the first arbitrary object, 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 arbitrary object. Once you have chosen a name for the last arbitrary object you want to introduce, click OK.