[Math] How to prove Disjunction Elimination rule of inference

logicproof-writingpropositional-calculus

I've looked at the tableau proofs of many rules of inference (double-negation, disjunction is commutative, modus tollendo ponens, and others), and they all seem to use the so-called "or-elimination" (Disjunction Elimination) rule:

$$(P\vdash R), (Q\vdash R), (P \lor Q) \vdash R$$

(If $P\implies R$ and $Q\implies R$, and either $P$ or $Q$ (or both) are true, then $R$ must be true.)

It's often called the "proof by cases" rule, it makes sense, and I've seen the principle used in many mathematical proofs.

I'm trying to figure out how to logically prove this rule (using other rules of inference and/or replacement), however the proof offered is self-reliant! Is this an axiom?

(There's also the Constructive Dilemma rule, which looks like a more generalized version of Disjunction Elimination. Maybe the proof of D.E. depends on C.D.? or maybe C.D. is an extension of D.E.?)

Best Answer

I agree that the link you provide to the proof offered by Proof Wiki is "self-reliant", and seems, to me at least, to invoke the very rule in which we are interested. In a sense, it can be seen as a "model" proof exemplifying the general case of invocation of Disjunction Elimination, $\lor \mathcal E$.

So, yes, this can sort of be thought of as an "axiom": a basic rule of inference we take to be valid, and from which other rules of inference may be derived. It does rely on modus ponens, twice. But the principle that, if, given the truth of $p \lor q$, and some conclusion $r$ follows from $p$, and the same conclusion $r$ follows from $q$, then we can conclude that $r$ is true.

It might be reassuring to note that the argument characterizing "Disjunction Elimination" can be expressed as follows:

$$(((P \to Q) \land (R \to Q)) \land (P \lor R)) \to Q\tag{Tautology}$$

which proves to be tautologically (necessarily) true $(\dagger)$, and so we have very good reason to accept the rule of inference as valid.

$(\dagger)$: Exercise - Confirm, using a truth-table, that the given tautology is, in fact, tautologically true.