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 est une abréviation du latin modus ponendo ponens qui signifie « le mode qui, en posant, pose ». Il vient de ce qu'en posant (affirmant) A, on pose (affirme) B (ponendo est le gérondif du verbe ponere qui signifie poser, et ponens en est le participe présent).

Le syllogisme est une forme d'application du modus ponens.

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) :

$A,\ A\Rightarrow B\vdash B$
ou

$\left({\begin{array}{c}A\rightarrow B\\A\\\hline B\end{array}}\right)$

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 le connecteur implication (notée généralement « ⇒ » ou « → ») et la relation de déduction (notée « ⊢ ») soient fortement liées, elles ne sont pas de même nature et ne peuvent s'identifier, cette 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 « ⇒ ». Le modus ponens peut en ce sens être vu comme la règle indiquant comment utiliser une implication lors d'une démonstration.

Les assistants de preuve comportent souvent dans leurs librairies un encodage du modus ponens sous forme d'une règle d'inférence. Par exemple en metamath:

min $e ⊢ φ
maj $e ⊢ ( φ → ψ )
ax-mp $a ⊢ ψ

Exemples

La phrase suivante constitue un modus ponens : "si x est un nombre dont la somme des chiffres est divisible par 3, alors x est divisible par 3. La somme des chiffres de 31782 est divisible par 3. Donc 31782 est divisible par 3".

Systèmes de déduction

À la Hilbert

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'axiomes bien choisis 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. C'est également le modus ponens qui permet d'aboutir au principe d'explosion ou au raisonnement par l'absurde de la logique classique.

Cette règle est indispensable, dans les systèmes à la Hilbert : 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.

Déduction naturelle

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).

Calcul des séquents

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 de résolution (généralise le modus ponens)
• Règle d'inférence
• Règle de coupure
• 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]