From a given statement P you can infer P∨Q, for any statement Q. Select any given P and give the Addition command, and a dialog box will open asking you to fill in the blank in the statement P∨___ in order to specify what inference you want to make.
You can also use this command to work backwards from your goal. If you select a given P and goal P∨Q and give the Addition command, Proof Designer will infer the goal from the given.
Parentheses in your goal can affect how the Addition command works. For example, if you select a given P and goal P∨Q∨R and give the Addition command, then Proof Designer will infer the goal from the given. But if the goal is (P∨Q)∨R, then the command won't work, because Proof Designer won't consider the selected given to be one of the disjuncts of the goal. Thus, you may want to add or remove parentheses in your goal before using the Addition command. To add or remove parentheses, use the Reexpress command.