In mathematical logic, a tautology (from Greek, Ancient (to 1453);: ταυτολογία) is a formula or assertion that is true in every possible interpretation. An example is "x=y or x≠y". Similarly, "either the ball is green, or the ball is not green" is always true, regardless of the colour of the ball.
The philosopher Ludwig Wittgenstein first applied the term to redundancies of propositional logic in 1921, borrowing from rhetoric, where a tautology is a repetitive statement. In logic, a formula is satisfiable if it is true under at least one interpretation, and thus a tautology is a formula whose negation is unsatisfiable. In other words, it cannot be false.
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
\vDashS
\top
\bot
Tautologies are a key concept in propositional logic, where a tautology is defined as a propositional formula that is true under any possible Boolean valuation of its propositional variables.[2] A key property of tautologies in propositional logic is that an effective method exists for testing whether a given formula is always satisfied (equiv., whether its negation is unsatisfiable).
The definition of tautology can be extended to sentences in predicate logic, which may contain quantifiers—a feature absent from sentences of propositional logic. Indeed, in propositional logic, there is no distinction between a tautology and a logically valid formula. In the context of predicate logic, many authors define a tautology to be a sentence that can be obtained by taking a tautology of propositional logic, and uniformly replacing each propositional variable by a first-order formula (one formula per propositional variable). The set of such formulas is a proper subset of the set of logically valid sentences of predicate logic (i.e., sentences that are true in every model).
The word tautology was used by the ancient Greeks to describe a statement that was asserted to be true merely by virtue of saying the same thing twice, a pejorative meaning that is still used for rhetorical tautologies. Between 1800 and 1940, the word gained new meaning in logic, and is currently used in mathematical logic to denote a certain type of propositional formula, without the pejorative connotations it originally possessed.
In 1800, Immanuel Kant wrote in his book Logic:Here, analytic proposition refers to an analytic truth, a statement in natural language that is true solely because of the terms involved.
In 1884, Gottlob Frege proposed in his Grundlagen that a truth is analytic exactly if it can be derived using logic. However, he maintained a distinction between analytic truths (i.e., truths based only on the meanings of their terms) and tautologies (i.e., statements devoid of content).
In his Tractatus Logico-Philosophicus in 1921, Ludwig Wittgenstein proposed that statements that can be deduced by logical deduction are tautological (empty of meaning), as well as being analytic truths. Henri Poincaré had made similar remarks in Science and Hypothesis in 1905. Although Bertrand Russell at first argued against these remarks by Wittgenstein and Poincaré, claiming that mathematical truths were not only non-tautologous but were synthetic, he later spoke in favor of them in 1918:Here, logical proposition refers to a proposition that is provable using the laws of logic.
During the 1930s, the formalization of the semantics of propositional logic in terms of truth assignments was developed. The term "tautology" began to be applied to those propositional formulas that are true regardless of the truth or falsity of their propositional variables. Some early books on logic (such as Symbolic Logic by C. I. Lewis and Langford, 1932) used the term for any proposition (in any formal logic) that is universally valid. It is common in presentations after this (such as Stephen Kleene 1967 and Herbert Enderton 2002) to use tautology to refer to a logically valid propositional formula, but to maintain a distinction between "tautology" and "logically valid" in the context of first-order logic
.
See main article: Propositional logic. Propositional logic begins with propositional variables, atomic units that represent concrete propositions. A formula consists of propositional variables connected by logical connectives, built up in such a way that the truth of the overall formula can be deduced from the truth or falsity of each variable. A valuation is a function that assigns each propositional variable to either T (for truth) or F (for falsity). So by using the propositional variables A and B, the binary connectives
\lor
\land
lnot
(A\landB)\lor(lnotA)\lor(lnotB)
A valuation here must assign to each of A and B either T or F. But no matter how this assignment is made, the overall formula will come out true. For if the first disjunct
(A\landB)
A formula of propositional logic is a tautology if the formula itself is always true, regardless of which valuation is used for the propositional variables. There are infinitely many tautologies. Examples include:
(A\lorlnotA)
lnot
(A\toB)\Leftrightarrow(lnotB\tolnotA)
((lnotA\toB)\land(lnotA\tolnotB))\toA
lnot(A\landB)\Leftrightarrow(lnotA\lorlnotB)
((A\toB)\land(B\toC))\to(A\toC)
((A\lorB)\land(A\toC)\land(B\toC))\toC
A minimal tautology is a tautology that is not the instance of a shorter tautology.
(A\lorB)\to(A\lorB)
C\toC
The problem of determining whether a formula is a tautology is fundamental in propositional logic. If there are n variables occurring in a formula then there are 2n distinct valuations for the formula. Therefore, the task of determining whether or not the formula is a tautology is a finite and mechanical one: one needs only to evaluate the truth value of the formula under each of its possible valuations. One algorithmic method for verifying that every valuation makes the formula to be true is to make a truth table that includes every possible valuation.
For example, consider the formula
((A\landB)\toC)\Leftrightarrow(A\to(B\toC)).
A\landB | (A\landB)\toC | B\toC | A\to(B\toC) | ((A\landB)\toC)\Leftrightarrow(A\to(B\toC)) | ||||
|---|---|---|---|---|---|---|---|---|
| T | T | T | T | T | T | T | T | |
| T | T | F | T | F | F | F | T | |
| T | F | T | F | T | T | T | T | |
| T | F | F | F | T | T | T | T | |
| F | T | T | F | T | T | T | T | |
| F | T | F | F | T | F | T | T | |
| F | F | T | F | T | T | T | T | |
| F | F | F | F | T | T | T | T |
It is also possible to define a deductive system (i.e., proof system) for propositional logic, as a simpler variant of the deductive systems employed for first-order logic (see Kleene 1967, Sec 1.9 for one such system). A proof of a tautology in an appropriate deduction system may be much shorter than a complete truth table (a formula with n propositional variables requires a truth table with 2n lines, which quickly becomes infeasible as n increases). Proof systems are also required for the study of intuitionistic propositional logic, in which the method of truth tables cannot be employed because the law of the excluded middle is not assumed.
See main article: Tautological consequence.
A formula R is said to tautologically imply a formula S if every valuation that causes R to be true also causes S to be true. This situation is denoted
R\modelsS
R\toS
For example, let
S
A\land(B\lorlnotB)
S
A
S
A
S
B\lorlnotB
R
A\landC
R\modelsS
R
A
S
It follows from the definition that if a formula
R
R
R
S
S
See main article: Substitution instance. There is a general procedure, the substitution rule, that allows additional tautologies to be constructed from a given tautology (Kleene 1967 sec. 3). Suppose that is a tautology and for each propositional variable in a fixed sentence is chosen. Then the sentence obtained by replacing each variable in with the corresponding sentence is also a tautology.
For example, let be the tautology:
(A\landB)\lorlnotA\lorlnotB
C\lorD
C\toE
It follows from the substitution rule that the sentence:
((C\lorD)\land(C\toE))\lorlnot(C\lorD)\lorlnot(C\toE)
An axiomatic system is complete if every tautology is a theorem (derivable from axioms). An axiomatic system is sound if every theorem is a tautology.
The problem of constructing practical algorithms to determine whether sentences with large numbers of propositional variables are tautologies is an area of contemporary research in the area of automated theorem proving.
The method of truth tables illustrated above is provably correct – the truth table for a tautology will end in a column with only T, while the truth table for a sentence that is not a tautology will contain a row whose final column is F, and the valuation corresponding to that row is a valuation that does not satisfy the sentence being tested. This method for verifying tautologies is an effective procedure, which means that given unlimited computational resources it can always be used to mechanistically determine whether a sentence is a tautology. This means, in particular, the set of tautologies over a fixed finite or countable alphabet is a decidable set.
As an efficient procedure, however, truth tables are constrained by the fact that the number of valuations that must be checked increases as 2k, where k is the number of variables in the formula. This exponential growth in the computation length renders the truth table method useless for formulas with thousands of propositional variables, as contemporary computing hardware cannot execute the algorithm in a feasible time period.
The problem of determining whether there is any valuation that makes a formula true is the Boolean satisfiability problem; the problem of checking tautologies is equivalent to this problem, because verifying that a sentence S is a tautology is equivalent to verifying that there is no valuation satisfying
lnotS
The fundamental definition of a tautology is in the context of propositional logic. The definition can be extended, however, to sentences in first-order logic.[4] These sentences may contain quantifiers, unlike sentences of propositional logic. In the context of first-order logic, a distinction is maintained between logical validities, sentences that are true in every model, and tautologies (or, tautological validities), which are a proper subset of the first-order logical validities. In the context of propositional logic, these two terms coincide.
A tautology in first-order logic is a sentence that can be obtained by taking a tautology of propositional logic and uniformly replacing each propositional variable by a first-order formula (one formula per propositional variable). For example, because
A\lorlnotA
(\forallx(x=x))\lor(lnot\forallx(x=x))
(((\existsxRx)\landlnot(\existsxSx))\to\forallxTx)\Leftrightarrow((\existsxRx)\to((lnot\existsxSx)\to\forallxTx)).
A
\existsxRx
B
lnot\existsxSx
C
\forallxTx
((A\landB)\toC)\Leftrightarrow(A\to(B\toC))
Not all logical validities are tautologies in first-order logic. For example, the sentence:
(\forallxRx)\tolnot\existsxlnotRx
A\toB