Английская Википедия:Conjunction elimination
Шаблон:Infobox mathematical statement Шаблон:Transformation rules
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:
- <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
sv:Matematiskt uttryck#Förenkling
