The Disjunction command can only be used when you
have a goal of the form P1
P2...Pn. 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 P1,
P2, ..., Pn 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
PQR 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(QR), then you
will be asked to choose between P and QR. 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.