## Goal 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.

If one of the statements *P*_{1},
*P*_{2}, …,
*P*_{n} is among your givens, you can
select it as well. When you give the Disjunction command, no dialog box will open,
and Proof Designer will simply infer the goal from the given.

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.