## Infer Menu:

# Disjunctive Syllogism Command

If you have givens of the forms *P*∨*Q*
and ¬*P*, then
you may infer *Q*. More generally, if you have a given of the form
*P*_{1}∨*P*_{2}∨…∨*P*_{n}
and you also have the negations of some of the statements *P*_{1},
*P*_{2}, …, *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*_{1}∨*P*_{2}∨…∨*P*_{n}
and your goal is the
disjunction of some of the statements *P*_{1},
*P*_{2}, …,
*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*_{1}∨*P*_{2}∨…∨*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*_{1},
*P*_{2}, …,
*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*_{1}∨*P*_{2}∨…∨*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
*P*∨*Q*∨*R*
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*∨(*Q*∨*R*),
then Proof Designer will say that you must prove
¬(*Q*∨*R*). 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.