How to prove Disjunction Elimination rule of inference

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.


In a standardly set up natural deduction system, with an introduction and an elimination rule for each connective, the rules are independent: you can't in particular, show that the $\lor$E rule follows from the other rules.

What you can do, however, as Gentzen noted, is to argue (outside the system) that the $\lor$E rule is in harmony with the introduction rule $\lor$I in the following sense: what the application of the elimination rule allows you to extract from a disjunction is no more than what you must have already been entitled to in order to assert the disjunction on the basis of $\lor$I in the first place.

Roughly: Suppose, as fixed background, that we have a proof from $P$ to $R$ and a proof from $Q$ to $R$. If you now put into play the disjunction $P \lor Q$, then this will canonically be on the basis that you are already entitled to $P$ (and hence, in the circumstances, to $R$) or you are already entitled to $Q$ (and hence, in the circumstances, to $R$). So we can infer $R$. As $\lor$E says.