Tautology (rule of inference) explained

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:

P \lor P \Leftrightarrow P

and the principle of idempotency of conjunction:

P \land P \Leftrightarrow P

Where "

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

Formal notation

\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 \lor P \vdash P

and

P \land P \vdash P

where

\vdash is a metalogical symbol meaning that P is a syntactic consequence of P \lor P , in the one case, P \land P in the other, in some logical system;

or as a rule of inference:

(P \lor P)/(\therefore P)

and

(P \land P)/(\therefore P)

where the rule is that wherever an instance of "

P \lor P " or "P \land 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 \lor P) \to P

and

(P \land P) \to P

where

P is a proposition expressed in some formal system.

Notes and References

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