thus makes true. It follows from the definition that if a formula is a contradiction, then tautologically implies every formula, because there is no truth valuation that causes to be true, and so the definition of tautological implication is trivially satisfied. Similarly, if is a tautology, then is tautologically implied by every formula. Substitution 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 . Let be and let be . It follows from the substitution rule that the sentence Semantic completeness and soundness 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. Efficient verification and the Boolean satisfiability problem 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