Voir la source de Règle d'introduction (logique)

Les '''règles d'introduction''' des [[Connecteur logique|connecteurs]] (disjonction, conjonction, implication, négation, etc.) sont des [[Règle d'inférence|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 déterminant 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 [[Calcul des séquents#Groupe structurel|règles structurelles]], le calcul des séquents ne contient que des règles d'introduction et aucune [[Déduction naturelle#Notion de règle d'introduction et de règle d'élimination|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''<ref>{{Ouvrage
 | auteur1        = Gerhard Gentzen
 | traducteur     = R. Feys et J. Ladrière
 | titre          = Recherches sur la déduction logique
 | titre original = Untersuchungen über das logische schließen
 | éditeur        = Presses Universitaires de France
 | année          = 1955
 | passage        = 4-5.
 | isbn           = 
}}{{Commentaire biblio|Traduit et commenté}}</ref> sous le nom allemand « ''Einführung'' », qui veut précisément dire ''introduction''.

== Présentation des règles ==
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 ==
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#Déduction naturelle en logique propositionnelle|déduction naturelle]]):
:<math>\frac{\vdots}{A \star B}</math>
Les points <math>\vdots</math>  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 ==
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
: <math>\frac{...}{\Gamma\vdash \Delta,A \star B}</math>
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 ==
En [[calcul des séquents]],  l'introduction à gauche se présente ainsi:
: <math>\frac{...}{\Gamma,A \star B\vdash \Delta}</math>

== Exemples de règles d'introduction en  déduction naturelle == 
: <math>\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}</math> 
Ces règles ont toutes une justification par une proposition logique valide, ainsi l'introduction du ∧ se justifie par la proposition <math>A \wedge B \Rightarrow A \wedge B</math>, tandis que les introduction du ∨ se justifient par les propositions <math>A \Rightarrow A \vee B</math> et <math>B \Rightarrow A \vee B</math>.

== Exemples de règles d'introduction en calcul des séquents ==
=== Pour la conjonction ===
: <math>\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
</math>
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 {{citation |  de Γ je déduis Δ ou A}} et {{citation|  de Γ je déduis Δ ou B}} alors  {{citation|  de Γ je déduis Δ ou A v B}}.  La deuxième règle pourrait se lire si  {{citation|  de Γ ou A je déduis Δ}} alors  {{citation|  de Γ ou A ∧ B   je déduis Δ }}
=== Pour la disjonction ===
:<math>\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
</math>
La disjonction a deux règles d'introduction à droite et une règle d'introduction à gauche.
=== Pour l'implication ===
:<math>\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
</math>
L'implication a une règle d'introduction à droite et une règle d'introduction à gauche.

=== Pour la négation ===
:<math> \frac{\Gamma \vdash \Delta, A}{\Gamma, \neg A \vdash \Delta} \qquad</math> <math> \frac{\Gamma, A \vdash \Delta}{\Gamma \vdash \Delta, \neg A }</math>
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 ==
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:
: <math>\frac{\Gamma\vdash\Delta, P(a)}{\Gamma\vdash\Delta, \forall x \cdot P(x)}</math>

== Voir aussi  ==
* [[Jean-Yves Girard]], ''Le Point aveugle'', Tome I, chapitre 3 : « Les séquents classiques : LK », pp. 45-74. Éd. Hermann, {{date-|mai 2006}}
* René David, Karim Nour, Christophe Raffali, ''Introduction à la logique, théorie de la démonstration'' 2001, [[Éditions Dunod|Dunod]], {{ISBN|2100067966}}, ''chap. 5''
* {{Ouvrage | auteur1=Stephen Cole Kleene | titre=Mathematical logic | éditeur=[[Dover Publications|Dover]] | année=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}}.
* {{Ouvrage|langue=fr|auteur1=René Lalement|titre=Logique, réduction, résolution|éditeur=Masson|année=1990|isbn=}}

== Références ==
{{Références}}

{{Palette Règles de transformation}}

{{Portail|logique}}

[[Catégorie:Logique propositionnelle]]
[[Catégorie:Logique mathématique]]
[[Catégorie:Raisonnement mathématique]]
[[Catégorie:Méthode de démonstration]]
[[Catégorie:Théorie de la démonstration]]