Tautology (rule of inference)

From HandWiki
Short description: Commonly used rules of replacement in propositional logic

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:

[math]\displaystyle{ P \lor P \Leftrightarrow P }[/math]

and the principle of idempotency of conjunction:

[math]\displaystyle{ P \land P \Leftrightarrow P }[/math]

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

Formal notation

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

The tautology rule may be expressed as a sequent:

[math]\displaystyle{ P \lor P \vdash P }[/math]


[math]\displaystyle{ P \land P \vdash P }[/math]

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

or as a rule of inference:

[math]\displaystyle{ \frac{P \lor P}{\therefore P} }[/math]


[math]\displaystyle{ \frac{P \land P}{\therefore P} }[/math]

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

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:

[math]\displaystyle{ (P \lor P) \to P }[/math]


[math]\displaystyle{ (P \land P) \to P }[/math]

where [math]\displaystyle{ P }[/math] is a proposition expressed in some formal system.


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