## Goal Menu:

# Arbitrary Object Command

The Arbitrary Object command can only be used when you
have a goal of the form
∀*x* *P*(*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
∀*x* *P*(*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.