Tautology (rule of inference)

The principle of idempotency of disjunction:

${\displaystyle P\vee P\iff P}$

and the principle of idempotency of conjunction:

${\displaystyle P\wedge P\iff P}$

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

Formal notation

Theorems are those logical formulas ${\displaystyle \varphi }$ where ${\displaystyle ⊢\varphi }$ is the conclusion of a valid proof, while the equivalent semantic consequence ${\displaystyle \models \varphi }$ indicates a tautology.

The tautology rule may be expressed as a sequent:

${\displaystyle P\vee P⊢P}$

and

${\displaystyle P\wedge P⊢P}$

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

or as a rule of inference:

${\displaystyle \frac{P\vee P}{\therefore P}}$

and

${\displaystyle \frac{P\wedge P}{\therefore P}}$

where the rule is that wherever an instance of "${\displaystyle P\vee P}$" or "${\displaystyle P\wedge 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\vee P)\to P}$

and

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

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