A uniform method for proving lower bounds on the computational complexity of logical theories (Q917543)

The paper presents a new method for obtaining lower bounds on the computational complexity of logical theories. The method is based on a family of new inseparability results for certain logical problems, related to the inseparability result of Trakhtenbrot and Vaught that no recursive set separates the logically valid sentences from those which are false in some finite model, as long as the underlying language has at least one non-unary relation symbol. The method yields hereditary lower bounds, i.e. bounds which apply uniformly to all subtheories of the theory. Another important benefit of this method is that it allows the use of interpretations to transfer lower bounds from one theory to another. In this way the need to code machine computations into the models of the studied theory is eliminated and the proofs for lower bounds are analogues to the methods for establishing NP-hardness via polynomial time reductions. The method is richly illustrated by providing new proofs (or sketches of proofs) of essentially all previously known lower bounds for theories. This beautiful paper provides an important technical and conceptual tool in the area of the computational complexity of logical theories. It is an invitation to investigate the many decidable theories for which no detailed complexity bounds have been found.