Modus ponendo ponens
[8] Modus ponendo ponens permite eliminar una sentencia condicional de una prueba lógica o argumento (los antecedentes) y por lo tanto no llevar estos antecedentes adelante en una cadena alargada y constante de símbolos.Por esta razón, el modus ponendo ponens a veces se denomina regla de la separación.[9] Enderton, por ejemplo, observó que «el modus ponendo ponens puede producir fórmulas más cortas de las más largas»,[10] y Russell señaló que «el proceso de la inferencia no puede reducirse a los símbolos.La regla del modus ponendo ponens puede escribirse en subsiguiente notación: donde ⊢ es un símbolo metalógico que significa que Q es una consecuencia sintáctica de P → Q y P en algún sistema lógico; o como la afirmación de una tautología verdad-funcional o teorema de la lógica proposicional: donde P, y Q son proposiciones expresadas en algún sistema formal.La primera premisa es la «si-entonces» o reclamación de condicional, a saber: que P implica Q.En inteligencia artificial, el modus ponens usualmente se lo denomina encadenamiento hacia adelante.Para que modus ponens sea un argumento sólido además de válido las premisas deberán ser verdaderas.