In logic, a tautology (from the Greek word ταυτολογία) is a formula that is true in every possible interpretation.

Philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921. (It had been used earlier to refer to rhetorical tautologies, and continues to be used in that alternative sense.) A formula is satisfiable if it is true under at least one interpretation, and thus a tautology is a formula whose negation is unsatisfiable. Unsatisfiable statements, both through negation and affirmation, are known formally as contradictions. A formula that is neither a tautology nor a contradiction is said to be logically contingent. Such a formula can be made either true or false based on the values assigned to its propositional variables. The double turnstile notation is used to indicate that S is a tautology. Tautology is sometimes symbolized by "Vpq", and contradiction by "Opq". The tee symbol is sometimes used to denote an arbitrary tautology, with the dual symbol (falsum) representing an arbitrary contradiction; in any symbolism, a tautology may be substituted for the truth value "true," as symbolized, for instance, by "1."