É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 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}}

{\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

(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

(P\land Q)\to Q

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

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

(en) David A. Duffy, Principles of Automated Theorem Proving, New York, Wiley, 1991 Sect.3.1.2.1, p.46
Copi and Cohen
Moore and Parker
Hurley

Cet article est issu de wikipedia. Text licence: CC BY-SA 4.0, Des conditions supplémentaires peuvent s’appliquer aux fichiers multimédias.