Proof by Cases
Sequent
Proof by cases is a valid argument in types of logic dealing with disjunctions $\lor$.
This includes propositional logic and predicate logic, and in particular natural deduction.
Proof Rule
- If we can conclude $\phi \lor \psi$, and:
- $(1): \quad$ By making the assumption $\phi$, we can conclude $\chi$
- $(2): \quad$ By making the assumption $\psi$, we can conclude $\chi$
- then we may infer $\chi$.
Sequent Form
Proof by Cases can be symbolised by the sequent:
- $p \lor q, \paren {p \vdash r}, \paren {q \vdash r} \vdash r$
Variants
The following forms can be used as variants of this theorem:
Formulation 1
- $\left({p \implies r}\right) \land \left({q \implies r}\right) \dashv \vdash \left({p \lor q}\right) \implies r$
Formulation 2
- $\vdash \paren {\paren {p \implies r} \land \paren {q \implies r} } \iff \paren {\paren {p \lor q} \implies r}$
Formulation 3
- $\vdash \paren {\paren {p \lor q} \land \paren {p \implies r} \land \paren {q \implies r} } \implies r$
Explanation
Proof by Cases can be expressed in natural language as follows:
We are given that either $\phi$ is true, or $\psi$ is true, or both.
Suppose we make the assumption that $\phi$ is true, and from that deduce that $\chi$ has to be true.
Then suppose we make the assumption that $\psi$ is true, and from that deduce that $\chi$ has to be true.
Therefore, it has to follow that the truth of $\chi$ follows from the fact of the truth of either $\phi$ or $\psi$.
Thus a disjunction is eliminated from a sequent.
Also known as
Proof by Cases is also known as the rule of or-elimination.