Editing Conjunction elimination

{{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 calculus|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 [[Validity (logic)|valid]] [[immediate inference]], [[argument form]] and [[rule of inference]] which makes the [[inference]] that, if the [[Logical conjunction|conjunction]] ''A and B'' is true, then ''A'' is true, and ''B'' is true. The rule makes it possible to shorten longer [[formal proof|proofs]] by deriving one of the conjuncts of a conjunction on a line by itself. 

An example in [[English language|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 [[metalogic]]al symbol meaning that <math>P</math> is a [[logical consequence|syntactic consequence]] of <math>P \land Q</math> and <math>Q</math> is also a syntactic consequence of <math>P \land Q</math> in [[formal system|logical system]];

and expressed as truth-functional [[tautology (logic)|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]]

[[sv:Matematiskt uttryck#Förenkling]]