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

Abstract

A new method for obtaining lower bounds on the computational complexity of logical theories is presented. It extends widely used techniques for proving the undecidability of theories by interpreting models of a theory already known to be undecidable. New inseparability results related to the well known inseparability result of Trakhtenbrot and Vaught are the foundation of the method. Their use yields hereditary lower bounds (i.e., bounds which apply uniformly to all subtheories of a theory). By means of interpretations lower bounds can be transferred from one theory to another. Complicated machine codings are replaced by much simpler definability considerations, viz., the kinds of binary relations definable with short formulas on large finite sets.Numerous examples are given, including new proofs of essentially all previously known lower bounds for theories, and lower bounds for various theories of finite trees, which turn out to be particularly useful.