El modus ponens , o desapego , es una figura del razonamiento lógico sobre la implicación . Consiste en afirmar una implicación (“si A entonces B ”) y luego establecer el antecedente (“o A ”) para deducir el consecuente (“luego B ”). El término modus ponens es una abreviatura del latín modus ponendo ponens que significa el modo que, al posar, posa . Viene del hecho de que por que presenta (afirmando) A , nos planteamos (affirm) B ( ponendo es el gerundio del verbo ponere que significa plantean , y ponens es su participio presente). El silogismo es una forma de aplicación del modus ponens.
La regla del modus ponens o desapego es una regla primitiva de razonamiento. Lo escribimos formalmente (según el contexto):
o
y podemos leer: “de A y A ⇒ B deducimos B ”, o incluso “ A y A ⇒ B luego B ”, es decir que afirmamos A y A ⇒ B , y deducimos que podemos decir B .
Aunque la implicación del conector (generalmente denotada "⇒" o "→") y la relación de deducción (denotada "⊢") están fuertemente relacionadas, no son de la misma naturaleza y no pueden identificarse, esta distinción es necesaria para formalizar el razonamiento. Así, la tautología proposicional [ A ∧ ( A ⇒ B )] ⇒ B no es una regla, y no puede representar el modus ponens, para el conector implicativo designado por “⇒”. En este sentido, el modus ponens puede verse como la regla que indica cómo utilizar una implicación durante una demostración .
A menudo (pero no necesariamente) es la única regla de inferencia para el cálculo de proposiciones , en sistemas de deducción a la de Hilbert , porque las reglas primitivas de los otros conectores se expresan a partir de axiomas bien elegidos y del modus ponens. Por ejemplo, la regla de la conjunción "de A ∧ B deducimos A " se deriva de los modus ponens y el axioma ( A ∧ B ) ⇒ A . Es también el modus ponens el que permite llegar al principio de explosión o razonamiento por el absurdo de la lógica clásica .
Esta regla es esencial, en sistemas à la Hilbert : tal reducción no es posible para el modus ponens en sí, para deducirla por ejemplo de [ A ∧ ( A ⇒ B )] ⇒ B , sería necesario d 'otros axiomas ... y varias aplicaciones del propio modus ponens.
Encontramos una forma de modus ponens en los sistemas de deducción natural bajo el nombre de regla de eliminación de implicación , donde necesariamente tiene una forma más general, en el sentido de que necesitamos usarla en presencia de hipótesis. Esta generalización no es necesaria en sistemas a la de Hilbert , en los que la regla simétrica introductoria, "de A ⊢ B deducimos A ⇒ B ", es una regla derivada, conocida como teorema de deducción , que nuevamente se demuestra a partir de la única regla de modus ponens y axiomas adecuados, pero de una manera más compleja, utilizando una recurrencia sobre la longitud de la deducción (la traducción depende por tanto de la deducción).
El cálculo de los secuentes , debido como la deducción natural a Gerhard Gentzen , no tiene directamente una regla de modus ponens. Esto puede derivarse de la regla de corte, que es un modus ponens al nivel de la deducción, esencialmente cuando tenemos ⊢ A y A ⊢ B tenemos ⊢ B estas deducciones se hacen en un contexto determinado, y la participación de la regla izquierda que pueden demostrar la Sist A , A ⇒ B ⊢ B . Gentzen demostró que la regla de corte podría eliminarse en el cálculo de secuentes para el cálculo de predicados puros (sin igualdad, y fuera del marco de una teoría axiomática ), y que en este contexto, la demostración de una fórmula solo podría utilizar sub-fórmulas de la misma. Esto no es posible en un sistema a la Hilbert, donde, en cuanto se invoca el modus ponens, se introduce una fórmula más compleja que la fórmula que se pretende demostrar.
Como deducción natural, la propiedad de normalización, que corresponde a la eliminación de cortes en el cálculo de secuentes, muestra que es posible (aún en el cálculo de predicados puros) restringir el uso de modus ponens a las subfórmulas de la fórmula para demostrar.
La propiedad de la subfórmula para estos dos sistemas (deducción natural y cálculo de secuentes) tiene como contrapartida la introducción de un nivel adicional, el de secuentes, donde la deducción de sistemas a la Hilbert se ocupa únicamente de fórmulas.