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$?


1 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$.

  • $\begingroup$ Thanks for the response. I was basing my disjunction elimination from the Wikipedia page on Propositional Logic. I wonder if that page is not using your formulation because they want to avoid hypothetical rules (the only hypothetical rule they have is the →-introduction rule). $\endgroup$ Jan 15, 2021 at 17:38

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .