Voir la source de Élimination de la conjonction

{{à recycler |date=novembre 2016|thème=logique}}
En [[calcul des propositions]], l'<nowiki/>'''élimination de la conjonction '''(aussi appelé '''élimination du ''et''''', '''élimination du''' '''∧'''<ref>{{Ouvrage|langue=en|auteur1=David A. Duffy|titre=Principles of Automated Theorem Proving|lieu=New York|éditeur=[[John Wiley & Sons|Wiley]]|année=1991|isbn=}} Sect.3.1.2.1, p.46</ref>, ou '''simplification''')<ref>Copi and Cohen
{{Citation nécessaire|date=février 2014}}</ref>{{,}}<ref>Moore and Parker
{{Citation nécessaire|date=février 2014}}</ref>{{,}}<ref>Hurley
{{Citation nécessaire|date=février 2014}}</ref> est une {{quoi | [[inférence immédiate]]}} [[Validité (logique)|valide]], {{pas clair | 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émonstration formelle|démonstrations]] en dérivant l'un des {{quoi | conjontifs}} d'une conjonction {{quoi | sur une ligne}} par lui-même.

La règle est composée de deux {{quoi |sous-règles}} distinctes, qui peuvent être exprimées en {{comment | [[langage formel]]}}:
: <math>\frac{P \land Q}{\therefore P}</math>
et
: <math>\frac{P \land Q}{\therefore Q}</math>
Les deux sous-règles signifient en même temps que, chaque fois qu'une instance "<math>P \land Q</math>" apparaît sur une {{quoi | ligne}} d'une démonstration, soit "<math>P</math>", soit "<math>Q</math>" peut être placé sur une ligne {{quoi |subséquente}} par {{qui | lui-même}}.

== {{pourquoi | Notation formelle}} ==
Les {{quoi | sous-règles}} de l'''élimination de la conjonction ''peuvent être écrites en notation {{quoi | séquent}}:
: <math>(P \land Q) \vdash P</math>
et
: <math>(P \land Q) \vdash Q</math>
où <math>\vdash</math> est un {{pas clair | symbole [[métalogique]]}} qui signifie que <math>P</math> est une [[déduction logique]] de <math>P \land Q</math> et <math>Q</math> est également une conséquence de <math>P \land Q</math>

et exprimée en {{quoi | [[Tautologie (logique)|tautologie]]s}} ou en [[théorèmes]] de la logique propositionnelle:
: <math>(P \land Q) \to P</math>
et
: <math>(P \land Q) \to Q</math>
où <math>P</math> et <math>Q</math> sont des propositions exprimées dans un {{lequel | [[système formel]]}}.

== Références ==
{{Traduction/Référence|lang1=en|art1=Conjunction elimination|id1=662661702}}
{{Références}}

{{Palette|Règles de transformation}}

{{Portail|logique}}

[[Catégorie:Théorème de logique mathématique]]