Introduction de la disjonction
# Introduction de la disjonction

L'introduction de la disjonction ou addition (aussi appelé introduction du $ou)^,^,$ 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 dans une démonstration. Elle est l'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 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 logiques paracohérentes car en combinaison avec d'autres règles logique, elle conduit à une 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 séquente :

    $P\vdash (P\lor Q)$

où $\vdash$ est un symbole métalogique qui signifie que $P\lor Q$ est une conséquence syntaxique de $P$ dans un système logique ;

et exprimée en tautologie ou en théorème de logique propositionnelle:

    $P\to (P\lor Q)$

où $P$ et $Q$ 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.

    ${\frac {P}{\therefore P\lor Q}}$

Autrement dit, chaque fois qu'une formule $P$ apparaît sur une ligne d'une démonstration, $P\lor Q$ (avec Q également une formule quelconque) peut être placé sur une ligne subséquente.

