In propositional logic, disjunction elimination (sometimes named proof by cases, case analysis, or or 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
P
implies a statement
Q
and a statement
R
also implies
Q
, then if either
P
or
R
is true, then
Q
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.
If I'm inside, I have my wallet on me.
If I'm outside, I have my wallet on me.
It is true that either I'm inside or I'm outside.
Therefore, I have my wallet on me.
It is the rule can be stated as:
P
→
Q
,
R
→
Q
,
P
∨
R
∴
Q
where the rule is that whenever instances of "
P
→
Q
", and "
R
→
Q
" and "
P
∨
R
" appear on lines of a proof, "
Q
" can be placed on a subsequent line.
The disjunction elimination rule may be written in sequent notation:
(
P
→
Q
)
,
(
R
→
Q
)
,
(
P
∨
R
)
⊢
Q
where
⊢
is a metalogical symbol meaning that
Q
is a syntactic consequence of
P
→
Q
, and
R
→
Q
and
P
∨
R
in some logical system;
and expressed as a truth-functional tautology or theorem of propositional logic:
(
(
(
P
→
Q
)
∧
(
R
→
Q
)
)
∧
(
P
∨
R
)
)
→
Q
where
P
,
Q
, and
R
are propositions expressed in some formal system.
