# Tautology (rule of inference)

Transformation rules |
---|

Propositional calculus |

Rules of inference |

Rules of replacement |

Predicate logic |

In propositional logic, **tautology** is one of two commonly used rules of replacement.^{[1]}^{[2]}^{[3]} The rules are used to eliminate redundancy in disjunctions and conjunctions when they occur in logical proofs. They are:

The principle of **idempotency of disjunction**:

and the principle of **idempotency of conjunction**:

Where "" is a metalogical symbol representing "can be replaced in a logical proof with."

## Formal notation[edit]

Theorems are those logical formulas where is the conclusion of a valid proof,^{[4]} while the equivalent semantic consequence indicates a tautology.

The *tautology* rule may be expressed as a sequent:

and

where is a metalogical symbol meaning that is a syntactic consequence of , in the one case, in the other, in some logical system;

or as a rule of inference:

and

where the rule is that wherever an instance of "" or "" appears on a line of a proof, it can be replaced with "";

or as the statement of a truth-functional tautology or theorem of propositional logic. The principle was stated as a theorem of propositional logic by Russell and Whitehead in *Principia Mathematica* as:

and

where is a proposition expressed in some formal system.