Règle d'introduction (logique)

Les règles d'introduction des connecteurs (disjonction, conjonction, implication, négation, etc.) sont des règles d'inférence que l'on trouve dans le calcul des séquents et la déduction naturelle. Elles jouent un rôle fondamental dans la description de ces systèmes, car elles permettent d'expliquer comment les connecteurs sont « introduits » dans le cours d'une démonstration. En dehors des règles structurelles, le calcul des séquents ne contient que des règles d'introduction et aucune règle d'élimination.

Les règles d'introduction 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 « Einführung », qui veut précisément dire introduction.

Présentation des règles[modifier | modifier le code]

Un séquent Γ ⊢ Δ est une expression logique qui se lit « du multiensemble Γ de formules on déduit le multiensemble Δ de formules ». rappelons qu'une règle d'inférence explique comment d'une famille de séquents (les prémisses) on peut déduire un séquent (la conclusion). Les règles d'introduction ont pour but de « complexifier » les formules de base, pour démontrer les propositions les plus générales.

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

Soit un connecteur ★, une règle d'introduction de ★ se présente sous la forme suivante. C'est en particulier la forme qu'elle a en (déduction naturelle):

{\frac {\vdots }{A\star B}}

Les points $\vdots$ représentent une ou plusieurs démonstrations de propositions et ces propositions sont, soit A, soit B et ne sont pas, a priori, la proposition A ★ B, qui doit être « introduite ».

Introduction à droite[modifier | modifier le code]

En calcul des séquents, on peut introduire le nouveau connecteur, soit à droite, soit à gauche du symbole ⊢. Par exemple, étant donné un connecteur ★, la règle d'inférence d'introduction à droite de ★ a la forme

{\frac {...}{\Gamma \vdash \Delta ,A\star B}}

où les antécédents de la règle sont constitués de séquents qui contiennent les propositions de Γ et de Δ ainsi que la proposition A et la proposition B.

Introduction à gauche[modifier | modifier le code]

En calcul des séquents, l'introduction à gauche se présente ainsi:

{\frac {...}{\Gamma ,A\star B\vdash \Delta }}

Exemples de règles d'introduction en déduction naturelle[modifier | modifier le code]

{\frac {A\qquad B}{A\wedge B}}\qquad {\frac {A}{A\vee B}}\qquad {\frac {B}{A\vee B}}\qquad {{[A] \atop \vdots } \atop {\frac {B}{A\Rightarrow B}}}\qquad {\frac {\Gamma ,A\vdash \perp }{\Gamma \vdash \neg A}}

Ces règles ont toutes une justification par une proposition logique valide, ainsi l'introduction du ∧ se justifie par la proposition $A\wedge B\Rightarrow A\wedge B$ , tandis que les introduction du ∨ se justifient par les propositions $A\Rightarrow A\vee B$ et $B\Rightarrow A\vee B$ .

Exemples de règles d'introduction en calcul des séquents[modifier | modifier le code]

Pour la conjonction[modifier | modifier le code]

{\frac {\Gamma \vdash \Delta ,A\qquad \Gamma \vdash \Delta ,B}{\Gamma \vdash \Delta ,A\wedge B}}\qquad {\frac {\Gamma ,A\vdash \Delta }{\Gamma ,A\wedge B\vdash \Delta }}\qquad {\frac {\Gamma ,B\vdash \Delta }{\Gamma ,A\wedge B\vdash \Delta }}\qquad

Autrement dit la conjonction a une règle d'introduction à droite et deux règles d'introduction à gauche. La première règle pourrait se lire si « de Γ je déduis Δ ou A » et « de Γ je déduis Δ ou B » alors « de Γ je déduis Δ ou A v B ». La deuxième règle pourrait se lire si « de Γ ou A je déduis Δ » alors « de Γ ou A ∧ B je déduis Δ »

Pour la disjonction[modifier | modifier le code]

{\frac {\Gamma \vdash \Delta ,A}{\Gamma \vdash \Delta ,A\vee B}}\qquad {\frac {\Gamma \vdash \Delta ,B}{\Gamma \vdash \Delta ,A\vee B}}\qquad {\frac {\Gamma ,A\vdash \Delta \qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\vee B\vdash \Delta }}\qquad

La disjonction a deux règles d'introduction à droite et une règle d'introduction à gauche.

Pour l'implication[modifier | modifier le code]

{\frac {\Gamma ,A\vdash \Delta ,B}{\Gamma \vdash \Delta ,A\Rightarrow B}}\qquad {\frac {\Gamma \vdash \Delta ,A\qquad \Gamma ,B\vdash \Delta }{\Gamma ,A\Rightarrow B\vdash \Delta }}\qquad

L'implication a une règle d'introduction à droite et une règle d'introduction à gauche.

Pour la négation[modifier | modifier le code]

{\frac {\Gamma \vdash \Delta ,A}{\Gamma ,\neg A\vdash \Delta }}\qquad

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

Une proposition dans une partie du séquent correspond à la même proposition niée dans l'autre partie du séquent.

Règle d'introduction de quantificateurs[modifier | modifier le code]

Au-delà des connecteurs, il y a aussi des règles d'introduction pour les quantificateurs. Ainsi, pour l'introduction du quantificateur universel on a la règle:

{\frac {\Gamma \vdash \Delta ,P(a)}{\Gamma \vdash \Delta ,\forall x\cdot P(x)}}

Voir aussi[modifier | modifier le code]

Jean-Yves Girard, Le Point aveugle, Tome I, chapitre 3 : « Les séquents classiques : LK », pp. 45-74. Éd. Hermann, mai 2006
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

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é

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]