Élimination de la conjonction

Si ce bandeau n'est plus pertinent, retirez-le. Cliquez ici pour en savoir plus.

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

{\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 ?]}[modifier | modifier le code]

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[modifier | modifier le code]

(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 ^{[citation nécessaire]}
↑ Moore and Parker ^{[citation nécessaire]}
↑ Hurley ^{[citation nécessaire]}

Portail de la logique

[1] (en) David A. Duffy, Principles of Automated Theorem Proving, New York, Wiley, 1991 Sect.3.1.2.1, p.46

[2] Copi and Cohen ^{[citation nécessaire]}

[3] Moore and Parker ^{[citation nécessaire]}

[4] Hurley ^{[citation nécessaire]}

[1]

[2]

[3]

[4]

Notation formelle[pourquoi ?][modifier | modifier le code]

Références[modifier | modifier le code]

Notation formelle^{[pourquoi ?]}[modifier | modifier le code]