Definition
A tautology is a propositional formula that is true under every assignment of truth values to its atomic propositions. Examples: P ∨ ¬P (excluded middle), (P ⊃ (Q ⊃ P)), ((P ⊃ Q) ∧ (Q ⊃ R)) ⊃ (P ⊃ R) (hypothetical syllogism). The set of tautologies coincides with the set of theorems of propositional calculus (by soundness and completeness).
Why it matters
How it works
To check whether a formula is a tautology, construct its truth table over all 2ⁿ assignments to its n atoms; verify the formula is true in every row. For large formulas this is intractable directly; in practice, use logical equivalences (de Morgan, distributivity) to convert to a normal form (CNF or DNF) where tautology-checking is easier, or use a SAT solver to check whether the formula's negation is satisfiable (it is a tautology iff its negation is unsatisfiable).