Conjunction elimination explained

Conjunction elimination
Type:	Rule of inference
Field:	Propositional calculus
Statement:	If the conjunction A and B is true, then A is true, and B is true.
Symbolic Statement:	(P \land Q)/(\therefore P) , (P \land Q)/(\therefore Q) (P \land Q) \vdash P, (P \land Q) \vdash Q (P \land Q) \to P,(P \land Q) \to Q

In propositional logic, conjunction elimination (also called and elimination, ∧ elimination,^[1] or simplification)^{[2] [3] [4]} 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:

(P \land Q)/(\therefore P)

and

(P \land Q)/(\therefore Q)

The two sub-rules together mean that, whenever an instance of "

P \land Q " appears on a line of a proof, either "P " or "Q " 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:

(P \land Q) \vdash P and(P \land Q) \vdash Q

where

\vdash is a metalogical symbol meaning that P is a syntactic consequence of P \land Q and Q is also a syntactic consequence of P \land Q in logical system;

and expressed as truth-functional tautologies or theorems of propositional logic:

(P \land Q) \to P and(P \land Q) \to Q

where

P and Q are propositions expressed in some formal system.

Notes and References

1. Book: David A. Duffy . Principles of Automated Theorem Proving . New York . Wiley . 1991 . Sect.3.1.2.1, p.46
2. Copi and Cohen
3. Moore and Parker
4. Hurley