In propositional logic, tautology is either 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:

${\displaystyle P\lor P\Leftrightarrow P}$

and the principle of idempotency of conjunction:

${\displaystyle P\land P\Leftrightarrow P}$

Where "${\displaystyle \Leftrightarrow }$" is a metalogical symbol representing "can be replaced in a logical proof with."

Formal notation

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

The tautology rule may be expressed as a sequent:

${\displaystyle P\lor P\vdash P}$

and

${\displaystyle P\land P\vdash P}$

where ${\displaystyle \vdash }$ is a metalogical symbol meaning that ${\displaystyle P}$ is a syntactic consequence of ${\displaystyle P\lor P}$, in the one case, ${\displaystyle P\land P}$ in the other, in some logical system;

or as a rule of inference:

${\displaystyle {\frac {P\lor P}{\therefore P))}$

and

${\displaystyle {\frac {P\land P}{\therefore P))}$

where the rule is that wherever an instance of "${\displaystyle P\lor P}$" or "${\displaystyle P\land P}$" appears on a line of a proof, it can be replaced with "${\displaystyle P}$";

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:

${\displaystyle (P\lor P)\to P}$

and

${\displaystyle (P\land P)\to P}$

where ${\displaystyle P}$ is a proposition expressed in some formal system.