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)