Disjunction elimination
In propositional logic, disjunction elimination, is the valid argument form and rule of inference that allows one to eliminate a disjunctive statement from a logical proof. It is the inference that if a statement implies a statement and a statement also implies, then if either or is true, then has to be true. The reasoning is simple: since at least one of the statements P and R is true, and since either of them would be sufficient to entail Q, Q is certainly true.
An example in English:
It is the rule can be stated as:
where the rule is that whenever instances of "", and "" and "" appear on lines of a proof, "" can be placed on a subsequent line.The disjunction elimination rule may be written in sequent notation:
where is a metalogical symbol meaning that is a syntactic consequence of, and and in some logical system;
and expressed as a truth-functional tautology or theorem of propositional logic:
where,, and are propositions expressed in some formal system.
