Is disjunction elimination a more general form of modus ponens?

Question

It seems to me that disjunction introduction and disjunction elimination implies modus ponens. To be clear, I'm defining disjunction introduction as: $$p\vdash (p\lor q)$$

disjunction elimination as: $${\displaystyle \{p\lor q,p\to r,q\to r\}\vdash r}$$

and modus ponens as:

$$\{p,p\to q\}\vdash q$$

The proof of modus ponens ($\{A, A\to B\} \vdash B$) would be as follows:

1. $A$ (Premise)
2. $A \lor A$ (From (1) by disjunction introduction)
3. $A \to B$ (Premise)
4. $B$ (From (2) and (3) by disjunction elimination)

Am I missing something? Isn't modus ponens just a special case of disjunction elimination where $p = q$?

Answer 1

Your reasoning is fine, but you are using a nonstandard form of disjunction elimination. The usual natural deduction formulation is:

From $\vdash p\lor q$ and $p\vdash r$ and $q\vdash r$ infer $\vdash r$.

Compared to yours, this formulation uses the derivability relation $\vdash$ instead of the logical implication $\rightarrow$. It is an easy exercise to see that your version of disjunction elimination derives the standard one using the rule of $\rightarrow$-introduction.

Conversely, here is a derivation of your disjunction elimination from the standard one:

1. $\vdash p\lor q$ (premise)
2. $\vdash p\rightarrow r$ (premise)
3. $\vdash q\rightarrow r$ (premise)
4. $p,p\rightarrow r\vdash r$ (MP)
5. $p\vdash r$ (from (2) and (4) by cut)
6. $q,q\rightarrow r\vdash r$ (MP)
7. $q\vdash r$ (from (3) and (6) by cut)
8. $\vdash r$ (from (1), (5) and (7) using standard disjunction elimination)

Crucially, this derivation makes use of the modus ponens rule. So one could say that your version of disjunction elimination has some built-in modus ponens, and therefore your initial observation is not surprising.

On the other hand it is not possible to derive modus ponens from the standard disjunction elimination rule. Indeed, if your only rule involving $\rightarrow$ is the $\rightarrow$-introduction rule

From $p\vdash q$ infer $\vdash p\rightarrow q$

then the meaning of $\rightarrow$ is underspecified: you cannot rule out that the interpretation of $p\rightarrow q$ is something silly like a fixed tautology $\top$.