From Wikipedia, the free encyclopedia - View original article

Transformation rules |
---|

Propositional calculus |

Predicate logic |

For other uses, see Simplification (disambiguation).

In propositional logic, **simplification**^{[1]}^{[2]}^{[3]} (equivalent to **conjunction elimination**) 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 can be expressed in formal language as:

or as

where the rule is that whenever instances of "" appear on lines of a proof, either "" or "" can be placed on a subsequent line by itself.

The *simplification* rule may be written in sequent notation:

or as

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 a truth-functional tautology or theorem of propositional logic:

and

where and are propositions expressed in some logical system.