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éraleModifier

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

 

C est soit A, soit B, et les points   et   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 :

 

C est aussi soit A, soit B et   sont des séquents. Par exemple le modus ponens est la règle d'élimination de l'implication :

 

Exemples de règles d'éliminationModifier

Élimination de la conjonctionModifier

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

 

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

 

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

 

et

 

Élimination de la disjonctionModifier

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

 

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

 

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

 

Élimination de l'implicationModifier

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

 

et sa forme en séquents :

 

Elle est justifiée par l'implication valide :

 

Élimination du fauxModifier

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

 

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

 

Elle est justifiée par l'implication valide :

 

Élimination de la négationModifier

Sa forme avec séquents est :

 

Elle est justifiée par l'implication valide :

 

Articles connexesModifier

RéférencesModifier

  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, , p. 4-5.
    Traduit et commenté

BibliographieModifier

  • 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, — 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,