Tautologies are self evident truths, that require no assumptions to determine their veracity. Within the study of logic, a tautology is a statement containing more than one sub-statement, that is true regardless of the truth values of its parts. For example, the statement "Either all crows are black, or not all of them are," is a tautology, because it is true no matter what color crows are. Expressing this formally, as a proposition with X representing "All crows are black" would give
[X \lor \lnot X],
which is a tautology, denoted [\top], because regardless of the truth value of X, one of the disjuncts is true, making the whole statement true. The symbol [\top] means a "generic" tautology in contexts where any old tautology will do, without being specific about exactly where the tautology lies.
A statement such as
[X \land \lnot X]
that is always false regardless of the truth values of its parts is known as a contradiction on an inconsistency and is denoted [\bot].
In propositional logic, the symbol [\vDash] or [\vdash] may be placed before a sentence or formuale to indicate that it is a tautology. The blank to the left of the [\vdash] symbol means that no assumptions are required to logically deduce the material to the right of the symbol. So it is true to say:
[\lbrace X \lor \lnot X \rbrace \vdash \top, \lbrace\rbrace \vdash \top, \top \vdash X \lor \lnot X ]
Two key truths about tautology are 1) [ \lnot\top \vdash \bot ] and 2) [ \lnot\bot \vdash \top ]. So a non-tautology is an inconsistency and a non-inconsistency is a tautology.
In predicate logic, a distinction is often made between tautologies and validities (or logical truths). From this perspective, a statement is considered a tautology if and only if it is a validity in propositional logic (that is, when everything within the scope of a quantifier is viewed as a black box). So for example the statement
[(\forall x)(x=5)\lor\lnot(\forall x)(x=5)]
would be a tautology because it can be rewritten in the form
[X \lor \lnot X]
and this is a tautology. In contrast, the statement
[(\forall x)\big((x=5)\lor\lnot(x=5)\big)]
would be a validity but not a tautology, even though it is true in every possible interpretation, because there is no way to express it as a tautology in propositional logic. This distinction is not always observed.
Discovering tautologies
An effective procedure for checking whether a propositional formula is a tautology or not is by means of truth tables. As an efficient procedure, however, truth tables are constrained by the fact that the number of logical interpretations (or truth-value assignments) that have to be checked increases as 2k, where k is the number of variables in the formula. Algebraic, symbolic, or transformational methods of simplifying formulas quickly become a practical necessity to overcome the "brute-force", exhaustive search strategies of tabular decision procedures.
