In propositional logic, **tautology** is one of two commonly used rules of replacement. 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**:

P
∨
P
⇔
P
and the principle of **idempotency of conjunction**:

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

Theorems are those logical formulas
ϕ
where
⊢
ϕ
is the conclusion of a valid proof, while the equivalent semantic consequence
⊨
ϕ
indicates a tautology.

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

P
∨
P
⊢
P
and

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

or as a rule of inference:

P
∨
P
∴
P
and

P
∧
P
∴
P
where the rule is that wherever an instance of "
P
∨
P
" or "
P
∧
P
" appears on a line of a proof, it can be replaced with "
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:

(
P
∨
P
)
→
P
and

(
P
∧
P
)
→
P
where
P
is a proposition expressed in some formal system.