Tautology (rule of inference)

From Wikipedia, the free encyclopedia
Jump to navigation Jump to search

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:

and the principle of idempotency of conjunction:

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

Formal notation[edit]

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

The tautology rule may be expressed as a sequent:


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

or as a rule of inference:


where the rule is that wherever an instance of "" or "" appears on a line of a proof, it can be replaced with "";

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:


where is a proposition expressed in some formal system.


  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