Conjunction eliminationType | Rule of inference |
---|
Field | Propositional calculus |
---|
Statement | If the conjunction and is true, then is true, and is true. |
---|
Symbolic statement | ![{\displaystyle {\frac {P\land Q}{\therefore P}},{\frac {P\land Q}{\therefore Q}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f2ad0a6166a64593a34bbcebd83bca806c1ef2ba) ![{\displaystyle (P\land Q)\vdash P,(P\land Q)\vdash Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7d14ab1ff12148c512460c46ff5ed9c1b1faae4a) ![{\displaystyle (P\land Q)\to P,(P\land Q)\to Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/e34337af18bf9965bcfae02ddb612bec85cd0f11) |
---|
Transformation rules |
---|
Propositional calculus |
---|
Rules of inference |
---|
- Implication introduction / elimination (modus ponens)
- Biconditional introduction / elimination
- Conjunction introduction / elimination
- Disjunction introduction / elimination
- Disjunctive / hypothetical syllogism
- Constructive / destructive dilemma
- Absorption / modus tollens / modus ponendo tollens
- Negation introduction
|
Rules of replacement |
---|
- Associativity
- Commutativity
- Distributivity
- Double negation
- De Morgan's laws
- Transposition
- Material implication
- Exportation
- Tautology
|
Predicate logic |
---|
Rules of inference |
---|
- Universal generalization / instantiation
- Existential generalization / instantiation
|
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:
![{\displaystyle {\frac {P\land Q}{\therefore P}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/db53bd233c94c3f9da1251118f986e91abda360f)
and
![{\displaystyle {\frac {P\land Q}{\therefore Q}}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/5dca8932d7609e9f1ce587a2d01c92c22cd568dd)
The two sub-rules together mean that, whenever an instance of "
" appears on a line of a proof, either "
" or "
" can be placed on a subsequent line by itself. The above example in English is an application of the first sub-rule.
The conjunction elimination sub-rules may be written in sequent notation:
![{\displaystyle (P\land Q)\vdash P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/58b49dee4a703fd57f9123df2ee44334e41ab260)
and
![{\displaystyle (P\land Q)\vdash Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/44110b004af0fa9c7b9444e232b0b24190b30b3a)
where
is a metalogical symbol meaning that
is a syntactic consequence of
and
is also a syntactic consequence of
in logical system;
and expressed as truth-functional tautologies or theorems of propositional logic:
![{\displaystyle (P\land Q)\to P}](https://wikimedia.org/api/rest_v1/media/math/render/svg/41e2aa33111c29464b13d96dc09280c8f6d377e0)
and
![{\displaystyle (P\land Q)\to Q}](https://wikimedia.org/api/rest_v1/media/math/render/svg/fcb8c81cffc2098e3f2ae24a3c985fc3cde28a13)
where
and
are propositions expressed in some formal system.
References
- ^ David A. Duffy (1991). Principles of Automated Theorem Proving. New York: Wiley. Sect.3.1.2.1, p.46
- ^ Copi and Cohen[citation needed]
- ^ Moore and Parker[citation needed]
- ^ Hurley[citation needed]