## Strategy Menu:

# Disjunction Command

The Disjunction command can only be used when you
have a goal of the form *P*_{1}*P*_{2}...*P*_{n}. If you select a goal of
this form and give the Disjunction command, then a dialog box will open,
asking you which of the statements *P*_{1},
*P*_{2}, ..., *P*_{n} you want to prove. Proof
Designer will then create a subproof in which the negations of all the
other statements are assumed, and you have to prove the statement you
selected. If you don't want to assume the negations of the other
statements, remove the check mark from the “Assume negations of
others” check box before clicking OK.

Parentheses in the goal can affect the list of statements that appear
in the dialog box. For example, if you select a goal of the form
*P**Q**R* and give the Disjunction command, then you will be
asked whether you want to prove *P*, *Q*, or *R*. But if
your goal has the form *P*(*Q**R*), then you
will be asked to choose between *P* and *Q**R*. Thus, you may want to add or remove parentheses in
your goal before using the Disjunction command. Too add or remove
parentheses, use the Reexpress command.