Modus ponens

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.

Sommaire

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
\frac{A \Rightarrow B\ \  A}{B}.

et on peut lire : « de A et de AB on déduit B », ou encore « A et AB donc B », c'est-à-dire que l'on affirme A et AB, 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 ∧ (AB)] ⇒ 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 AB on déduit A », se déduit du modus ponens et de l'axiome (AB) ⇒ 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 ∧ (AB)] ⇒ 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 AB», 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, AB |- 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

Bibliographie

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

Wikimedia Foundation. 2010.

Contenu soumis à la licence CC-BY-SA. Source : Article Modus ponens de Wikipédia en français (auteurs)

Игры ⚽ Поможем решить контрольную работу

Regardez d'autres dictionnaires:

  • 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… …   Wikipédia en Français

  • modus ponens — [mɔdyspɔnɛ̃s] n. m. ÉTYM. Loc. lat., littéralement « mode qui pose ». ❖ ♦ Log. Règle de déduction selon laquelle, si une proposition A implique une proposition B, on peut déduire, A étant vraie, que B l est également. (On dit aussi règle de… …   Encyclopédie Universelle

  • Modus ponens — («правило вывода»): если A и A→B  выводимые формулы, то B также выводима. Форма записи: , где A, B  любые формулы. Правило вывода модус поненс, обычно называемое правилом отделения или гипотетическим силлогизмом, позволяет от… …   Википедия

  • Modus Ponens —  ♦ Modus Ponens    Верное заключение, состоящее в переходе от истинности посылки к истинности ее необходимого следствия. Modus ponens принимает форму: если р, то q; однако р, следовательно, q (например: если Сократ человек, то он смертен; однако… …   Философский словарь Спонвиля

  • Modus ponens — (Latín: modo que afirma) es una regla de inferencia simple: Si P, entonces Q. P. Entonces, Q. Expresado en la notación de operadores lógicos: donde representa la aserción lógica …   Enciclopedia Universal

  • Modus ponens — Rules of inference Propositional calculus Modus ponens (A→B, A ⊢ B) Modus tollens (A→B, ¬B ⊢ ¬A) …   Wikipedia

  • Modus Ponens — Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen Systemen (siehe Logik, Kalkül) als Schlussregel verwendet wird. Der Modus ponens erlaubt es, aus zwei Aussagen der Form Wenn A, dann B und A (den …   Deutsch Wikipedia

  • Modus ponens — Der Modus ponens ist eine schon in der antiken Logik geläufige Schlussfigur, die in vielen logischen Systemen (siehe Logik, Kalkül) als Schlussregel verwendet wird. Der Modus ponens erlaubt es, aus zwei Aussagen der Form Wenn A, dann B und A (den …   Deutsch Wikipedia

  • modus ponens — noun A valid form of argument in which the antecedent of a conditional proposition is affirmed, thereby entailing the affirmation of the consequent. Modus ponens has the form: 1. If P, then Q. See Also: modus tollens …   Wiktionary

  • modus ponens and modus tollens — (Latin: method of affirming and method of denying ) In logic, two types of inference that can be drawn using a hypothetical proposition i. e., from a proposition of the form If p, then q (symbolically p ⊃ q). Modus ponens refers to inferences of… …   Universalium

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”