Élimination de la conjonction
# Élimination de la conjonction

En calcul des propositions, l'élimination de la conjonction (aussi appelé élimination du et, élimination du ∧, ou $simplification)^,^,$ est une inférence immédiate 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. La règle permet de raccourcir les démonstrations en dérivant l'un des conjontifs d'une conjonction sur une ligne par lui-même.

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

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

et

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

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

## Notation formelle

Les sous-règles de l'élimination de la conjonction peuvent être écrites en notation séquent:

    $(P\land Q)\vdash P$

et

    $(P\land Q)\vdash Q$

où $\vdash$ est un symbole métalogique qui signifie que $P$ est une déduction logique de $P\land Q$ et $Q$ est également une conséquence de $P\land Q$

et exprimée en tautologies ou en théorèmes de la logique propositionnelle:

    $(P\land Q)\to P$

et

    $(P\land Q)\to Q$

où $P$ et $Q$ sont des propositions exprimées dans un système formel.

