Infer Menu:

Disjunctive Syllogism Command

If you have givens of the forms PQ and P, then you may infer Q. More generally, if you have a given of the form P₁P₂...P_n and you also have the negations of some of the statements P₁, P₂, ..., P_n as givens, then you can infer that one of the other statements in the list must be true. Select all of the givens involved in the inference and give the Disjunctive Syllogism command, and Proof Designer will make the inference.

You can also use this command to work backwards from your goal. If you have a given of the form P₁P₂...P_n and your goal is the disjunction of some of the statements P₁, P₂, ..., P_n, then you could complete the proof by first proving the negations of the other statements in the list and then using the disjunctive syllogism rule. Select the given P₁P₂...P_n and the goal and give the Disjunctive Syllogism command. Proof Designer will say that you now have to prove the negations of those statements in the list P₁, P₂, ..., P_n that don't appear in the goal, and it will say that once these have been proven, they can be used, together with the statement P₁P₂...P_n, to infer the goal. If you already have some of these negations in your givens list, then you can select them too before giving the Disjunctive Syllogism command. Proof Designer will then require you to prove only those negations that are not already in your givens list.

Parentheses in your given can affect how the Disjunctive Syllogism command works. For example, suppose you have a given of the form PQR and your goal is P. If you select this given and goal and give the Disjunctive Syllogism command, then Proof Designer will say that you must prove both Q and R in order to complete the proof. But if the given is P(QR), then Proof Designer will say that you must prove (QR). Thus, you may want to add or remove parentheses in your given before using the Disjunctive Syllogism command. Too add or remove parentheses, use the Reexpress command.