Modus ponens

Un article de Wikipédia, l'encyclopédie libre.

Le modus ponens est un type de raisonnement logique consistant à affirmer une implication (« si p alors q ») et à poser ensuite l'antécédent (« or, p ») pour en déduire la vérité du conséquent (« donc q »). Les termes modus ponens (ou plus exactement modus ponendo ponens) viennent du fait qu'on pose "p" ("ponens" en latin) afin de tirer la conclusion.

Dans les systèmes de déduction à la Hilbert, le modus ponens est l'unique règle d'inférence du calcul des propositions ; c'est un cas particulier de la règle de coupure :

de (A ou B) et de (non A ou C) on peut en déduire (B ou C) (le « ou » étant non exclusif).

L'important résultat d'élimination des coupures de Gentzen montre que dans une présentation du calcul propositionnel comme le calcul des séquents, cette règle de coupure et par conséquent le modus ponens ne sont pas nécessaires. C'est-à-dire que toute démonstration utilisant une application de la règle de coupure (ou du modus ponens) peut être transformée en une démonstration ne l'utilisant pas.