Élimination de la conjonction

En calcul des propositions, l'élimination de la conjonction (aussi appelé élimination du et, élimination du ∧^[1], ou simplification)^[2],[3],[4] est une inférence immédiate^[Quoi ?] valide, sous forme d'argument et de règle d'inférence qui rend la conclusion selon laquelle, si la conjonction A et B est vrai, alors A est vrai et B est vrai.^[pas clair] La règle permet de raccourcir les démonstrations en dérivant l'un des conjontifs^[Quoi ?] d'une conjonction sur une ligne^[Quoi ?] par lui-même.

Cet article doit être recyclé (novembre 2016).

La règle est composée de deux sous-règles^[Quoi ?] distinctes, qui peuvent être exprimées en langage formel^[Comment ?]:

${\displaystyle {\frac {P\land Q}{\therefore P}}}$

et

${\displaystyle {\frac {P\land Q}{\therefore Q}}}$

Les deux sous-règles signifient en même temps que, chaque fois qu'une instance "${\displaystyle P\land Q}$" apparaît sur une ligne^[Quoi ?] d'une démonstration, soit "${\displaystyle P}$", soit "${\displaystyle Q}$" peut être placé sur une ligne subséquente^[Quoi ?] par lui-même^[Qui ?].