Tautology (rule of inference)

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.