Modus Ponendo Ponens

From ProofWiki
Jump to navigation Jump to search

Proof Rule

The modus ponendo ponens is a valid deduction sequent in propositional logic.

Proof Rule

If we can conclude $\phi \implies \psi$, and we can also conclude $\phi$, then we may infer $\psi$.

Sequent Form

\(\ds p\) \(\implies\) \(\ds q\)
\(\ds p\) \(\) \(\ds \)
\(\ds \vdash \ \ \) \(\ds q\) \(\) \(\ds \)


The following forms can be used as variants of this theorem:

Variant 1

$p \vdash \left({p \implies q}\right) \implies q$

Variant 2

$\vdash p \implies \paren {\paren {p \implies q} \implies q}$

Variant 3

$\vdash \paren {\paren {p \implies q} \land p} \implies q$

Also known as

Modus Ponendo Ponens is also known as:

  • Modus ponens, abbreviated M.P.
  • The rule of implies-elimination
  • The rule of arrow-elimination
  • The rule of (material) detachment
  • The process of inference

Linguistic Note

Modus Ponendo Ponens is Latin for mode that by affirming, affirms.

The shorter form Modus Ponens means mode that affirms.

Also see

The following are related argument forms: