View source for Modus ponens

''law of detachment, rule of detachment''

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

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645701.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645702.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645703.png" /> denote formulas in a formal logical system, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645704.png" /> is the logical connective of [[Implication|implication]]. Modus ponens allows one to deduce <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645705.png" /> from the premise <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645706.png" /> (the minor premise) and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645707.png" /> (the major premise). If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645708.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m0645709.png" /> are true in some interpretation of the formal system, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457010.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457011.png" /> as the least class that contains the formulas from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457012.png" /> 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457013.png" /> from the derivation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457014.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457015.png" /> and the derivation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457016.png" /> of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457017.png" />.



====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

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457018.png" /></td> </tr></table>

where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457019.png" /> stands for negation and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/m/m064/m064570/m06457020.png" /> denotes the logical  "or" .

====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  P. Suppes,   "Introduction to logic" , v. Nostrand  (1957)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  A. Grzegorczyk,   "An outline of mathematical logic" , Reidel  (1974)</TD></TR></table>