Règle d'élimination (logique)

Les règles d'élimination des connecteurs (à savoir, la disjonction, la conjonction, l'implication, la négation, etc.) sont des règles d'inférence que l'on trouve en déduction naturelle.

Les règles d'élimination ont été présentées pour la première fois par Gentzen en 1934 dans son article fondateur Recherches sur la déduction logique^[1] sous le nom allemand « Beseitigung », qui veut précisément dire élimination.

Forme générale[modifier | modifier le code]

Soit un connecteur ★ binaire, une règle d'élimination de ★ se présente sous la forme suivante :

{\frac {{\frac {\vdots }{A\star B}}~~~\dots }{C}}

où C est soit A, soit B, et les points $\vdots$ et $\dots$ représentent une ou plusieurs démonstrations de propositions.

La déduction naturelle peut aussi se présenter à base de séquents de la forme Γ ⊢ A où A est une proposition et Γ est un multiensemble de propositions, qui peut se lire « du multiensemble de propositions Γ on déduit la proposition A ». Une règle d'élimination de ★ binaire se présente alors sous la forme d'une règle d'inférence :

{\frac {\Delta \vdash A\star B~~~~s_{1}\dots s_{n}}{\Gamma \vdash C}}

où C est aussi soit A, soit B et $s_{1}\dots s_{n}$ sont des séquents. Par exemple le modus ponens est la règle d'élimination de l'implication :

{\frac {\Gamma \vdash A\Rightarrow B~~~~~~\Gamma \vdash A}{\Gamma \vdash B}}

Exemples de règles d'élimination[modifier | modifier le code]

Élimination de la conjonction[modifier | modifier le code]

Article détaillé : Élimination de la conjonction.

Il y a deux règles d’élimination de la conjonction :

{\frac {A\wedge B}{A}}~~~~~~~~~~~~~~~~~~~~~~~~{\frac {A\wedge B}{B}}

qui s'écrivent sous forme de séquents :

{\frac {\Gamma \vdash A\wedge B}{\Gamma \vdash A}}~~~~~~~~~~~~~~~~~~~~~~~~{\frac {\Gamma \vdash A\wedge B}{\Gamma \vdash B}}

Ces règles sont justifiées par les implications valides suivantes :

(A\land B)\Rightarrow A

et

(A\land B)\Rightarrow B

Élimination de la disjonction[modifier | modifier le code]

Article détaillé : Élimination de la disjonction.

Il y a une règle d'élimination de la disjonction :

{\frac {{~ \atop A\vee B}~~~~~{{[A] \atop \vdots } \atop C}~~~~~{{[B] \atop \vdots } \atop C}}{C}}

qui s'écrit sous forme de séquent :

{\frac {\Gamma \vdash A\vee B~~~~~~\Gamma ,A\vdash C~~~~~~\Gamma ,B\vdash C}{\Gamma \vdash C}}

Cette règle est justifiée par l'implication valide suivante :

((A\lor B)\land (A\Rightarrow C)\land (B\Rightarrow C))\Rightarrow C.

Élimination de l'implication[modifier | modifier le code]

Le modus ponens est la règle de l'élimination de l'implication.

{\frac {A\Rightarrow B~~~~~A}{B}}

et sa forme en séquents :

{\frac {\Gamma \vdash A\Rightarrow B~~~~~~\Gamma \vdash A}{\Gamma \vdash B}}

Elle est justifiée par l'implication valide :

((A\Rightarrow B)\wedge A)\Rightarrow B.

Élimination du faux[modifier | modifier le code]

La règle ex falso quodlibet est l'élimination du faux (⊥) :

{\frac {\bot }{A}}

où $A$ est n'importe quelle proposition. On remarque que ⊥ est ici nullaire, c'est-à-dire une constante. Sa forme avec séquents est :

{\frac {\Gamma \vdash \bot }{\Gamma \vdash A}}

Elle est justifiée par l'implication valide :

\bot \Rightarrow A.

Élimination de la négation[modifier | modifier le code]

Sa forme avec séquents est :

{\frac {\Gamma \vdash \neg A}{\Gamma ,A\vdash \bot }}

Elle est justifiée par l'implication valide :

\neg A\Rightarrow (A\Rightarrow \bot ).

Articles connexes[modifier | modifier le code]

Références[modifier | modifier le code]

↑ Gerhard Gentzen (trad. R. Feys et J. Ladrière), Recherches sur la déduction logique [« Untersuchungen über das logische schließen »], Presses Universitaires de France, 1955, p. 4-5.
Traduit et commenté

Bibliographie[modifier | modifier le code]

René David, Karim Nour, Christophe Raffali, Introduction à la logique, théorie de la démonstration 2001, Dunod, (ISBN 2100067966), chap. 5
Stephen Cole Kleene, Mathematical logic, Dover, 1967 — Réimpression Dover reprint, 2001, (ISBN 0-486-42533-9). Traduction française, Logique mathématique, Armand Colin, 1971 ou Gabay 1987 (ISBN 2-87647-005-5).
René Lalement, Logique, réduction, résolution, Masson, 1990

Portail de la logique

[1] Gerhard Gentzen (trad. R. Feys et J. Ladrière), Recherches sur la déduction logique [« Untersuchungen über das logische schließen »], Presses Universitaires de France, 1955, p. 4-5.
Traduit et commenté

[1]