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 sous le nom allemand « Modèle:Langue », qui veut précisément dire élimination.

Forme générale

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

$\frac{\frac{⋮}{A\star B}\dots }{C}$

où C est soit A, soit B, et les points $⋮$ 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{\mathrm{\Delta }⊢A\star B{s}_1\dots s_n}{\mathrm{\Gamma }⊢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{\mathrm{\Gamma }⊢A\Rightarrow B\mathrm{\Gamma }⊢A}{\mathrm{\Gamma }⊢B}$

Exemples de règles d'élimination

É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{\mathrm{\Gamma }⊢A\wedge B}{\mathrm{\Gamma }⊢A}\frac{\mathrm{\Gamma }⊢A\wedge B}{\mathrm{\Gamma }⊢B}$

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

$(A\wedge B)\Rightarrow A$

et

$(A\wedge B)\Rightarrow B$

Élimination de la disjonction

Modèle:Article détaillé Il y a une règle d'élimination de la disjonction :

$\frac{\genfrac{}{}{0ex}{}{}{A\vee B}\genfrac{}{}{0ex}{}{\genfrac{}{}{0ex}{}{[A]}{⋮}}{C}\genfrac{}{}{0ex}{}{\genfrac{}{}{0ex}{}{[B]}{⋮}}{C}}{C}$

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

$\frac{\mathrm{\Gamma }⊢A\vee B\mathrm{\Gamma },A⊢C\mathrm{\Gamma },B⊢C}{\mathrm{\Gamma }⊢C}$

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

$((A\vee B)\wedge (A\Rightarrow C)\wedge (B\Rightarrow C))\Rightarrow C.$

Élimination de l'implication

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

$\frac{A\Rightarrow BA}{B}$

et sa forme en séquents :

$\frac{\mathrm{\Gamma }⊢A\Rightarrow B\mathrm{\Gamma }⊢A}{\mathrm{\Gamma }⊢B}$

Elle est justifiée par l'implication valide :

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

Élimination du faux

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

$\frac{\mathrm{\perp }}{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{\mathrm{\Gamma }⊢\mathrm{\perp }}{\mathrm{\Gamma }⊢A}$

Elle est justifiée par l'implication valide :

$\mathrm{\perp }\Rightarrow A.$

Élimination de la négation

Sa forme avec séquents est :

$\frac{\mathrm{\Gamma }⊢\mathrm{\neg }A}{\mathrm{\Gamma },A⊢\mathrm{\perp }}$

Elle est justifiée par l'implication valide :

$\mathrm{\neg }A\Rightarrow (A\Rightarrow \mathrm{\perp }).$

Articles connexes

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

Bibliographie

• René David, Karim Nour, Christophe Raffali, Introduction à la logique, théorie de la démonstration 2001, Dunod, Modèle:ISBN, chap. 5
• Modèle:Ouvrage — Réimpression Dover reprint, 2001, Modèle:ISBN. Traduction française, Logique mathématique, Armand Colin, 1971 ou Gabay 1987 Modèle:ISBN.
• Modèle:Ouvrage