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.

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

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

où C est soit A, soit B, et les points ${\displaystyle \vdots }$ et ${\displaystyle \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 :

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

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

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

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

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

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

${\displaystyle {\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 :

${\displaystyle (A\land B)\Rightarrow A}$

et

${\displaystyle (A\land B)\Rightarrow B}$

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

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

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

${\displaystyle {\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 :

${\displaystyle ((A\lor B)\land (A\Rightarrow C)\land (B\Rightarrow C))\Rightarrow C.}$

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

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

et sa forme en séquents :

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

Elle est justifiée par l'implication valide :

${\displaystyle ((A\Rightarrow B)\wedge A)\Rightarrow B.}$

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

${\displaystyle {\frac {\bot }{A}}}$

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

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

Elle est justifiée par l'implication valide :

${\displaystyle \bot \Rightarrow A.}$

Sa forme avec séquents est :

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

Elle est justifiée par l'implication valide :

${\displaystyle \neg A\Rightarrow (A\Rightarrow \bot ).}$

• Calcul des séquents
• Modus ponens
• Ex falso quodlibet
• Règle d'introduction (logique)

• 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