Une règle d’inférence permettant d’inférer chacun des conjoncts à partir d’une conjonction A ∧ B ; formellement de A ∧ B on dérive A (et symétriquement B).

Principe

Une conjonction affirme simultanément ses deux conjoncts ; par conséquent chaque conjonct est individuellement impliqué par la conjonction comme prémisse dans une preuve.

Démonstration

À partir d’une dérivation de A ∧ B, appliquer l’élimination de la conjonction pour obtenir A. Exemple : de « Il pleut ∧ le sol est mouillé » dériver « Il pleut ».

Mauvaise application

Appliquer l’élimination de la conjonction à une formule qui n’est pas une vraie conjonction (par ex. à une implication matérielle ou à une disjonction), ou supposer que l’élimination peut produire des conjoncts qui n’étaient pas présents (par ex. inférer B à partir de A seul).

Conséquence

Permet d’extraire et d’utiliser localement des faits spécifiques contenus dans une assertion composée, facilitant le raisonnement modulaire et les sous-preuves ciblées.

Inversion

L’opération inverse est l’introduction de la conjonction (composition) : tandis que l’élimination divise un composé en parties, l’introduction compose des parties en un composé ; les confondre mène à des inférences non fondées.

Limite

Valide en logique classique, intuitionniste et dans la plupart des systèmes déductifs standards ; elle peut être restreinte dans des logiques où la conjonction a un sens différent (par ex. la logique linéaire avec gestion des ressources) ou quand la conjonction est définie extensionnellement plutôt que proof-théoriquement.

Tension sémantique

La tension apparaît avec la distribution ou avec des connecteurs composés dont la syntaxe ressemble à une conjonction mais possèdent une structure supplémentaire ; décider de la validité de l’élimination exige d’examiner la sémantique du connecteur.

Synthèse

L’élimination de la conjonction est la règle qui permet aux preuves d’accéder aux composants individuels garantis par une conjonction, transformant une assertion conjointe en prémisses individuelles exploitables pour le raisonnement ultérieur.