Tautology (rule of inference)

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:

$P \or P \Leftrightarrow P$

and the principle of idempotency of conjunction:

$P \and P \Leftrightarrow P$

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

Formal notation

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

The tautology rule may be expressed as a sequent:

$P \or P \vdash P \,$

and

$P \and P \vdash P \,$

where $\vdash$ is a metalogical symbol meaning that $P$ is a syntactic consequence of $P \or P$, in the one case, $P \and P$ in the other, in some logical system;

or as a rule of inference:

$\frac{P \or P}{\therefore P}$

and

$\frac{P \and P}{\therefore P}$

where the rule is that wherever an instance of "$P \or P$" or "$P \and 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 \or P) \to P \,$

and

$(P \and P) \to P \,$

where $P$ is a proposition expressed in some formal system.

References

1. Hurley, Patrick (1991). A Concise Introduction to Logic 4th edition. Wadsworth Publishing. pp. 364–5.
2. Copi and Cohen
3. Moore and Parker
4. Logic in Computer Science, p. 13