In mathematical logic, a tautology (from Ancient Greek: ταυτολογία) is a formula that is true regardless of the interpretation of its component terms, with only the logical constants having a fixed meaning.
Tautology is usually, though not always, used to refer to valid formulas of propositional logic.
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.
Such a formula can be made either true or false based on the values assigned to 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).
In 1800, Immanuel Kant wrote in his book Logic: The identity of concepts in analytical judgments can be either explicit (explicita) or non-explicit (implicita).
In 1884, Gottlob Frege proposed in his Grundlagen that a truth is analytic exactly if it can be derived using logic.
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: Everything that is a proposition of logic has got to be in some sense or the other like a tautology.
In this broad sense, a tautology is a formula that is true under all interpretations, or that is logically equivalent to the negation of a contradiction.
Tarski and Gödel followed this usage and it appears in textbooks such as that of Lewis and Langford.
[4] [5] Modern textbooks more commonly restrict the use of 'tautology' to valid sentences of propositional logic, or valid sentences of predicate logic that can be reduced to propositional tautologies by substitution.
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).
The problem of determining whether a formula is a tautology is fundamental in propositional logic.
[2] For example, consider the formula There are 8 possible valuations for the propositional variables A, B, C, represented by the first three columns of the following table.
The remaining columns show the truth of subformulas of the formula above, culminating in a column showing the truth value of the original formula under each valuation.
Because each row of the final column shows T, the sentence in question is verified to be a tautology.
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.
to be true, and so the definition of tautological implication is trivially satisfied.
Suppose that S is a tautology and for each propositional variable A in S a fixed sentence SA is chosen.
An axiomatic system is complete if every tautology is a theorem (derivable from axioms).
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 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.
It is widely believed that (equivalently for all NP-complete problems) no polynomial-time algorithm can solve the satisfiability problem, although some algorithms perform well on special classes of formulas, or terminate quickly on many instances.
[8] The fundamental definition of a tautology is in the context of propositional logic.
Similarly, in a first-order language with a unary relation symbols R,S,T, the following sentence is a tautology: It is obtained by replacing