# Proof by Cases

## Sequent

**Proof by cases** is a valid deduction sequent in propositional logic.

### 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**.