É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^[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.

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

${\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^[Quoi ?] d'une démonstration, soit "$P$", soit "$Q$" peut être placé sur une ligne subséquente^[Quoi ?] par lui-même^[Qui ?].

Notation formelle^{[pourquoi ?]}

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

$(P\land Q)\vdash P$

et

$(P\land Q)\vdash Q$

où $\vdash$ est un symbole métalogique^[pas clair] 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^[Quoi ?] 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^[Lequel ?].

Références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Conjunction elimination » (voir la liste des auteurs).