Modus ponens

law of detachment, rule of detachment

A derivation rule in formal logical systems. The rule of modus ponens is written as a scheme

$$\frac{A \ A \supset B }{B} ,$$

where $A$ and $B$ denote formulas in a formal logical system, and $\supset$ is the logical connective of implication. Modus ponens allows one to deduce $B$ from the premise $A$( the minor premise) and $A \supset B$( the major premise). If $A$ and $A \supset B$ are true in some interpretation of the formal system, then $B$ is true. Modus ponens, together with other derivation rules and axioms of a formal system, determines the class of formulas that are derivable from a set of formulas $M$ as the least class that contains the formulas from $M$ and the axioms, and closed with respect to the derivation rules.

Modus ponens can be considered as an operation on the derivations of a given formal system, allowing one to form the derivation of a given formula $B$ from the derivation $\alpha$ of $A$ and the derivation $\beta$ of $A \supset B$.

Comments

The more precise Latin name of the law of detachment is modus ponendo ponens. In addition there is modus tollendo ponens, which is written as the scheme

$$\frac{\neg B \ A \lor B }{A} ,$$

where $\neg$ stands for negation and $\lor$ denotes the logical "or" .

References

[a1]	P. Suppes, "Introduction to logic" , v. Nostrand (1957)
[a2]	A. Grzegorczyk, "An outline of mathematical logic" , Reidel (1974)