Élimination de la conjonction

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

Une réorganisation et une clarification du contenu paraissent nécessaires. Améliorez-le, discutez des points à améliorer ou précisez les sections à recycler en utilisant {{section à recycler}}.

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.

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 ?].

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

${\displaystyle (P\land Q)\vdash P}$

et

${\displaystyle (P\land Q)\vdash Q}$

où ${\displaystyle \vdash }$ est un symbole métalogique^[pas clair] qui signifie que ${\displaystyle P}$ est une déduction logique de ${\displaystyle P\land Q}$ et ${\displaystyle Q}$ est également une conséquence de ${\displaystyle P\land Q}$

et exprimée en tautologies^[Quoi ?] ou en théorèmes de la logique propositionnelle:

${\displaystyle (P\land Q)\to P}$

et

${\displaystyle (P\land Q)\to Q}$

où ${\displaystyle P}$ et ${\displaystyle Q}$ sont des propositions exprimées dans un système formel^[Lequel ?].

• (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).

• Portail de la logique