Une règle d’inférence qui permet d’inférer une disjonction A ∨ B à partir d’une preuve de l’un de ses disjoncts (de A inférer A ∨ B, ou de B inférer A ∨ B).

Principe

La preuve qu’un conjonct particulier tient suffit à établir la disjonction en ajoutant une alternative qui peut ou non tenir ; l’introduction de la disjonction préserve la vérité en affaiblissant l’assertion.

Démonstration

À partir d’une dérivation de A, appliquer l’introduction de la disjonction pour obtenir A ∨ B. Exemple : de « Il pleut » inférer « Il pleut ∨ Il neige ».

Mauvaise application

Utiliser l’introduction de la disjonction pour justifier le choix d’un conjonct particulier à partir d’une disjonction (inférer A à partir de A ∨ B), ou introduire des disjoncts irrélevants ou trompeurs qui masquent l’information constructive nécessaire dans un assistant de preuve.

Conséquence

Permet d’élargir les possibilités, préparer des analyses par cas et construire des branches pour une preuve par cas ; en langages de programmation correspond à l’injection d’une valeur dans un type somme (injection gauche ou droite).

Inversion

Se contraste avec l’élimination de la disjonction : l’introduction crée une alternative ambiguë à partir d’un fait certain, tandis que l’élimination exige de résoudre une disjonction par analyses de cas séparées pour en dégager une conséquence commune.

Limite

Valide en logique classique et intuitionniste comme règle structurelle de base ; en contextes constructifs/théorie des types il faut fournir l’injection appropriée (gauche ou droite) comme preuve constructive, et dans certains cadres l’ajout arbitraire de disjoncts peut faire perdre du contenu computationnel.

Tension sémantique

Tension entre le caractère affaiblissant de l’introduction de la disjonction (elle rend l’assertion moins informative) et la nécessité dans les cadres constructifs de préserver la preuve ; elle est correcte mais peut s’avérer peu informative pour des étapes constructives ultérieures.

Synthèse

L’introduction de la disjonction est le mécanisme qui transforme un fait certain en une assertion alternative plus large et vérité-préservante en ajoutant un disjonct possible ; c’est une manière légère de préparer le raisonnement par cas.