Proof by Cases

From ProofWiki
Jump to navigation Jump to search

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.


Also see