Proof by Cases

Theorem

$p \implies r, q \implies r \dashv \vdash p \lor q \implies r$

If both of two alternative cases imply the conclusion, then either one being true is enough to prove the conclusion true.

Its abbreviation in a tableau proof is $\textrm{PBC}$.

It is sometimes known as the derived rule of separation of cases.

A special case of PBC is as follows:

$p \implies q, \neg p \implies q \dashv \vdash q$

However, this one depends on the Law of the Excluded Middle, which is disallowed by the intuitionist school .

It is also known as the Principle of Dilemma.

Alternative rendition

These can alternatively be rendered as:

• $\vdash \left({\left({p \implies r}\right) \land \left({q \implies r}\right)}\right) \iff \left({\left({p \lor q}\right) \implies r}\right)$

• $\vdash \left({\left({p \lor q}\right) \land \left({p \implies r}\right) \land \left({q \implies r}\right)}\right) \implies r$

• $\vdash \left({\left({p \implies q}\right) \land \left({\neg p \implies q}\right)}\right) \iff q$

They can be seen to be logically equivalent to the forms above.

Proof

Proof by Natural deduction

By the Tableau method:

$p \implies r, q \implies r \vdash p \lor q \implies r$

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$p \implies r$	P	(None)
2		2	$q \implies r$	P	(None)
3		1, 2	$p \lor q \implies r \lor r$	Constructive Dilemma	1, 2	Most of the work's done now
4		4	$p \lor q$	A	(None)	Assume $p \lor q$ ...
5		1, 2, 4	$r \lor r$	Modus Ponendo Ponens	3, 4	... and derive $r \lor r$ ...
6		1, 2, 4	$r$	Rule of Idempotence	5
7		1, 2	$p \lor q \implies r$	Rule of Implication	4, 6	The assumption of $p \lor q$ has been discharged, so the proof rests just on 1 and 2.

$\blacksquare$

$p \implies q, \neg p \implies q \vdash q$

Line		Pool	Formula	Rule	Depends upon	Notes
1		1	$p \implies q$	P	(None)
2		2	$\neg p \implies q$	P	(None)
3			$p \lor \neg p$	Law of Excluded Middle	(None)
4		4	$p$	A	(None)	Assume $p$ ...
5		1, 4	$q$	$\implies \mathcal E$	4, 1	... and derive $q$ ...
6		6	$\neg p$	A	(None)	Assume $\neg p$ ...
7		2, 6	$q$	$\implies \mathcal E$	6, 2	... and derive $q$ ...
8		1, 2	$q$	$\lor \mathcal E$	3, 4-5, 6-7	Assumptions 4 and 6 have been discharged

$\blacksquare$

Quick proof

From the Constructive Dilemma we have:

$p \implies q, r \implies s \vdash p \lor r \implies q \lor s$

from which, changing the names of letters strategically:

$p \implies r, q \implies r \vdash p \lor q \implies r \lor r$

From the Rule of Idempotence we have:

$r \lor r \vdash r$

and the result follows by Hypothetical Syllogism.

$\blacksquare$

From the Constructive Dilemma we have:

$p \implies q, r \implies s \vdash p \lor r \implies q \lor s$

from which, changing the names of letters strategically:

$p \implies q, \neg p \implies q \vdash p \lor \neg p \implies q \lor q$

From the Law of Excluded Middle, we have:

$\vdash p \lor \neg p$

From the Rule of Idempotence we have:

$q \lor q \vdash q$

and the result follows by Hypothetical Syllogism.

$\blacksquare$

---

Proof by Truth Table

We apply the Method of Truth Tables to the propositions in turn.

As can be seen by inspection, the truth values under the main connectives match for all models.

$\begin{array}{|ccccccc||ccccc|} \hline (p & \implies & r) & \land & (q & \implies & r) & (p & \lor & q) & \implies & r \\ \hline F & T & F & T & F & T & F & F & F & F & T & F \\ F & T & T & T & F & T & T & F & F & F & T & T \\ F & T & F & F & T & F & F & F & T & T & F & F \\ F & T & T & T & T & T & T & F & T & T & T & T \\ T & F & F & F & F & T & F & T & T & F & F & F \\ T & T & T & T & F & T & T & T & T & F & T & T \\ T & F & F & F & T & F & F & T & T & T & F & F \\ T & T & T & T & T & T & T & T & T & T & T & T \\ \hline \end{array}$

$\blacksquare$

$\begin{array}{|cccccccc||c|} \hline (p & \implies & q) & \land & (\neg & p & \implies & q) & q \\ \hline F & T & F & F & T & F & F & F & F \\ F & T & T & T & T & F & T & T & T \\ T & F & F & F & F & T & T & F & F \\ T & T & T & T & F & T & T & T & T \\ \hline \end{array}$

$\blacksquare$

Sources

• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{I}: \S 3$: Exercises, Group $\text{I}: 15$
• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 3$: Theorem $\text{T33}$
• Donald Kalish and Richard Montague: Logic: Techniques of Formal Reasoning (1964): $\text{II}: \S 5$: Theorem $\text{T49}, \ \text{T50}$
• H. Jerome Keisler and Joel Robbin: Mathematical Logic and Computability (1996): $\S 1.12, \ \S 1.13$