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 ∨ P ⇔ P displaystyle Plor PLeftrightarrow P and the principle of idempotency of conjunction: P ∧ P ⇔ P displaystyle Pland PLeftrightarrow P Where " ⇔ displaystyle Leftrightarrow " is a metalogical symbol representing "can be replaced in a logical proof with." Formal notation[edit] 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: P ∨ P ⊢ P displaystyle Plor Pvdash P and P ∧ P ⊢ P displaystyle Pland Pvdash P where ⊢ displaystyle vdash is a metalogical symbol meaning that P displaystyle P is a syntactic consequence of P ∨ P displaystyle Plor P , in the one case, P ∧ P displaystyle Pland P in the other, in some logical system; or as a rule of inference: P ∨ P ∴ P displaystyle frac Plor P therefore P and P ∧ P ∴ P displaystyle frac Pland P therefore P where the rule is that wherever an instance of " P ∨ P displaystyle Plor P " or " P ∧ P displaystyle Pland P " appears on a line of a proof, it can be replaced with " P 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: ( P ∨ P ) → P displaystyle (Plor P)to P and ( P ∧ P ) → P displaystyle (Pland P)to P where P displaystyle P is a proposition expressed in some formal system. References[edit] ^ Hurley, Patrick (1991). A Concise Introduction to Logic 4th edition. Wadsworth Publishing. pp. 364–5. ^ Copi and Cohen ^ Moore and Parker ^ Logic in Computer Sc |