Modus ponens

Le modus ponens, ou détachement, est une figure du raisonnement logique concernant l'implication. Elle consiste à affirmer une implication (« si A alors B ») et à poser ensuite l'antécédent (« or, A ») pour en déduire le conséquent (« donc B »). Le terme modus ponens (ou plus exactement modus ponendo ponens) vient de ce que l'on pose A (ponens est le participe présent de verbe latin ponere, poser) afin d'en tirer la conclusion.

Formalisation

La règle du modus ponens ou de détachement est une règle primitive du raisonnement. On l'écrit formellement (suivant le contexte) :

et on peut lire : « de A et de A ⇒ B on déduit B », ou encore « A et A ⇒ B donc B », c'est-à-dire que l'on affirme A et A ⇒ B, et on en déduit que l'on peut affirmer B.

Bien que l'implication et la déduction soient fortement liées, elles ne s'identifient pas, et la distinction est nécessaire pour formaliser le raisonnement. Ainsi la tautologie propositionnelle [A ∧ (A ⇒ B)] ⇒ B n'est pas une règle, et ne peut représenter le modus ponens, pour le connecteur implicatif désigné par « ⇒ ».

Systèmes de déduction

C'est souvent (mais pas nécessairement) l'unique règle d'inférence du calcul des propositions, dans les systèmes de déduction à la Hilbert, car les règles primitives des autres connecteurs s'expriment à partir d'un axiome bien choisi et du modus ponens. Par exemple la règle de la conjonction « de A ∧ B on déduit A », se déduit du modus ponens et de l'axiome (A ∧ B) ⇒ A.

Une règle est indispensable : une telle réduction n'est pas possible pour le modus ponens lui-même, pour le déduire par exemple de [A ∧ (A ⇒ B)] ⇒ B, il faudrait d'autres axiomes ... et plusieurs applications du modus ponens lui-même.

On retrouve une forme du modus ponens dans les systèmes de déduction naturelle sous le nom de règle d'élimination de l'implication, où elle a nécessairement une forme plus générale, au sens où on a besoin de l'utiliser en présence d'hypothèses annexes. Cette généralisation n'est pas nécessaire dans les systèmes à la Hilbert, dans lesquels la règle symétrique d'introduction, « de "A" |- "B" on déduit A ⇒ B», est une règle dérivée, connue sous le nom de théorème de la déduction, qui à nouveau se démontre à partir de la seule règle de modus ponens et d'axiomes adéquats, mais de façon plus complexe, en utilisant une récurrence sur la longueur de la déduction (la traduction dépend donc de la déduction).

Le calcul des séquents, dû comme la déduction naturelle à Gerhard Gentzen, n'a pas directement de règle de modus ponens. Celle-ci peut se dériver par la règle de coupure qui est un modus ponens au niveau de la déduction — essentiellement quand on a |- A et A |- B on a |- B ces déductions se faisant dans un certain contexte —, et la règle gauche de l'implication qui permet de démontrer le séquent A, A ⇒ B |- B. Gentzen a montré que la règle de coupure pouvait s'éliminer en calcul des séquents pour le calcul des prédicats pur (sans égalité, et hors du cadre d'une théorie axiomatique), et que dans ce cadre, la démonstration d'une formule pouvait n'utiliser que des sous-formules de celle-ci. Ceci n'est pas possible dans un système à la Hilbert, où, dès que l'on fait appel au modus ponens, on introduit une formule plus complexe que la formule à démontrer.

En déduction naturelle la propriété de normalisation, qui correspond à l'élimination des coupures en calcul des séquents, montre qu'il est possible (toujours en calcul des prédicats pur) de restreindre l'utilisation du modus ponens aux sous-formules de la formule à démontrer.

La propriété de la sous-formule pour ces deux systèmes (déduction naturelle et calcul des séquents) a pour contrepartie l'introduction d'un niveau supplémentaire, celui des séquents, là où la déduction des systèmes à la Hilbert ne traite que de formules.

Articles connexes

• Modus tollens
• Raisonnement
• Règle d'inférence
• Syllogisme
• What the Tortoise Said to Achilles, dialogue de Lewis Carroll exposant un paradoxe associé au modus ponens.

Bibliographie

• René Cori et Daniel Lascar, Logique mathématique I. Calcul propositionnel, algèbres de Boole, calcul des prédicats  [détail des éditions]

• Portail de la logique
• Portail de la philosophie