{{Short description|Inference rule in logic}} {{Infobox mathematical statement | name = Conjunction elimination | type = Rule of inference | field = Propositional calculus | statement = If the conjunction <math>A</math> and <math>B</math> is true, then <math>A</math> is true, and <math>B</math> is true. | symbolic statement = # <math>\frac{P \land Q}{\therefore P}, \frac{P \land Q}{\therefore Q}</math> # <math>(P \land Q) \vdash P, (P \land Q) \vdash Q</math> # <math> (P \land Q) \to P,(P \land Q) \to Q</math> | conjectured by = | conjecture date = | first stated by = | first stated in = | first proof by = | first proof date = | open problem = | known cases = | implied by = | equivalent to = | generalizations = | consequences = }} {{Transformation rules}}
In propositional logic, '''conjunction elimination''' (also called '''''and''''' '''elimination''', '''∧ elimination''',<ref>{{cite book | author=David A. Duffy | title=Principles of Automated Theorem Proving | location=New York | publisher=Wiley | year=1991 }} Sect.3.1.2.1, p.46</ref> or '''simplification''')<ref>Copi and Cohen{{cn|reason=Without title, this is hardly a useful reference.|date=February 2014}}</ref><ref>Moore and Parker{{cn|date=February 2014}}</ref><ref>Hurley{{cn|date=February 2014}}</ref> is a valid immediate inference, argument form and rule of inference which makes the inference that, if the conjunction ''A and B'' is true, then ''A'' is true, and ''B'' is true. The rule makes it possible to shorten longer proofs by deriving one of the conjuncts of a conjunction on a line by itself.
An example in English: :It's raining and it's pouring. :Therefore it's raining.
The rule consists of two separate sub-rules, which can be expressed in formal language as:
:<math>\frac{P \land Q}{\therefore P}</math>
and
:<math>\frac{P \land Q}{\therefore Q}</math>
The two sub-rules together mean that, whenever an instance of "<math>P \land Q</math>" appears on a line of a proof, either "<math>P</math>" or "<math>Q</math>" can be placed on a subsequent line by itself. The above example in English is an application of the first sub-rule.
== Formal notation == The ''conjunction elimination'' sub-rules may be written in sequent notation:
: <math>(P \land Q) \vdash P</math> and : <math>(P \land Q) \vdash Q</math>
where <math>\vdash</math> is a metalogical symbol meaning that <math>P</math> is a syntactic consequence of <math>P \land Q</math> and <math>Q</math> is also a syntactic consequence of <math>P \land Q</math> in logical system;
and expressed as truth-functional tautologies or theorems of propositional logic:
:<math>(P \land Q) \to P</math> and :<math>(P \land Q) \to Q</math>
where <math>P</math> and <math>Q</math> are propositions expressed in some formal system.
== References == {{reflist}} {{logic-stub}} Category:Rules of inference Category:Theorems in propositional logic