Voir la source de Introduction de la disjonction

<code></code>
{{À sourcer|date=septembre 2016}}{{Article court|Règle d'introduction (logique) | disjonction|calcul des séquents | déduction naturelle}}

L''''introduction de la disjonction '''ou '''addition''' (aussi appelé '''introduction du ou''')<ref>{{ouvrage|langue=en|titre=A Concise Introduction to Logic 4th edition |nom=Hurley |prénom=Patrick |lien auteur= |coauteurs= |année=1991 |éditeur=Wadsworth Publishing |lieu= |isbn= |page= |pages=346–51 |url= |consulté le=}}</ref>{{,}}<ref>Moore et Parker</ref>{{,}}<ref>Copi et Cohen</ref> est une règle de déduction de la plupart des logiques formelles. Comme son nom l'indique, elle permet d'introduire le connecteur logique de la [[Disjonction logique|disjonction]] dans une [[Démonstration formelle|démonstration]]. Elle est l'[[inférence (logique)|inférence]] selon laquelle si ''P ''est vrai, alors ''P ou Q'' doit être vrai. Un exemple informel : à partir de ''Socrate est un homme'' en appliquant la règle d'introduction de la disjonction on peut déduire ''Socrate est un homme ou des cochons volent en formation au-dessus de la Manche''.
C'est une règle ''immédiate'', c'est-à-dire qu'elle est appliqué à partir d'une seule proposition. Elle se doit d'être [[Validité (logique)|valide]] pour être une [[règle d'inférence]], c'est-à-dire qu'elle ne peut déduire des propositions fausses à partir de propositions vraies, et elle l'est : si la [[prémisse]], ''Socrate est un homme'' dans notre exemple, est vraie, ''"Socrate est un homme'' ou Q" sera vraie aussi indépendamment de la valeur de Q par la définition du "ou". En effet une formule logique de la forme "A ou B" est vraie si au moins une des propositions A, B est vraie. 

L'introduction de la disjonction n'existe pas dans certaines logiques, comme certaines [[logique paracohérente|logiques paracohérentes]] car en combinaison avec d'autres règles logique, elle conduit à une [[Principe d'explosion|explosion]] (à savoir, tout devient démontrable). Ces logiques cherchant à éviter cette explosion pour tolérer certaines contradiction dans le raisonnement, et une des solutions consiste à introduire la disjonction d'autres manières.

== Notations formelles ==
La règle d'''introduction de la disjonction'' peut être écrite en notation [[Calcul des séquents|séquente]] :
: <math>P \vdash (P \lor Q)</math>
où <math>\vdash</math> est un symbole [[métalogique]] qui signifie que <math>P \lor Q</math> est une [[Déduction logique|conséquence syntaxique]] de <math>P</math> dans un [[système logique]] ;

et exprimée en [[tautologie (logique)|tautologie]] ou en [[théorème]] de [[logique propositionnelle]]:
: <math>P \to (P \lor Q)</math>
où <math>P</math> et <math>Q</math> sont des propositions exprimées dans un [[système formel]].

La règle est aussi parfois exprimée sous une forme similaire à celle-ci, où on peut lire au-dessus de la ligne verticale la prémisse à l'application de la règle et au-dessous un schéma de formule qu'on peut inférer. 
: <math>\frac{P}{\therefore P \lor Q}</math>
Autrement dit, chaque fois qu'une formule <math>P</math> apparaît sur une ligne d'une démonstration, <math>P \lor Q</math> (avec Q également une formule quelconque) peut être placé sur une ligne subséquente.

== Références ==
{{Traduction/Référence|lang1=en|art1=Disjonction introduction}}
{{Reflist}}

{{Palette Règles de transformation}}

{{Portail|logique}}

[[Catégorie:Logique propositionnelle]]