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.
If one of the statements P1, P2, …, Pn 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.