Modus ponens

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.

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.