Conjunction elimination
| Type | Rule of inference |
|---|---|
| Field | Propositional calculus |
| Statement | If the conjunction [math]\displaystyle{ A }[/math] and [math]\displaystyle{ B }[/math] is true, then [math]\displaystyle{ A }[/math] is true, and [math]\displaystyle{ B }[/math] is true. |
| Transformation rules |
|---|
| Propositional calculus |
| Rules of inference |
| Rules of replacement |
| Predicate logic |
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]\displaystyle{ \frac{P \land Q}{\therefore P} }[/math]
and
- [math]\displaystyle{ \frac{P \land Q}{\therefore Q} }[/math]
The two sub-rules together mean that, whenever an instance of "[math]\displaystyle{ P \land Q }[/math]" appears on a line of a proof, either "[math]\displaystyle{ P }[/math]" or "[math]\displaystyle{ 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]\displaystyle{ (P \land Q) \vdash P }[/math]
and
- [math]\displaystyle{ (P \land Q) \vdash Q }[/math]
where [math]\displaystyle{ \vdash }[/math] is a metalogical symbol meaning that [math]\displaystyle{ P }[/math] is a syntactic consequence of [math]\displaystyle{ P \land Q }[/math] and [math]\displaystyle{ Q }[/math] is also a syntactic consequence of [math]\displaystyle{ P \land Q }[/math] in logical system;
and expressed as truth-functional tautologies or theorems of propositional logic:
- [math]\displaystyle{ (P \land Q) \to P }[/math]
and
- [math]\displaystyle{ (P \land Q) \to Q }[/math]
where [math]\displaystyle{ P }[/math] and [math]\displaystyle{ Q }[/math] 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]
sv:Matematiskt uttryck#Förenkling
 |  |
