The complexity of logical theories

In this paper we introduce a method of encoding the computation of an alternating TM into a logical theory. The efficiency of the embedding we give together with the decision procedures, using Ehrenfencht games, which have been developed over the past few years, yield precise lower bounds for many decidable theories. In this paper we apply our technique explicitly to the theory of reals with addition; however, it should be clear that the techniques apply directly to other theories as well. We also outline the proof of a general theorem, motivated by a comment of A.R. Meyer and discovered independently by A.R. Meyer and L. Stockmeyer, which allows us to obtain a recent result of Bruss and Meyer directly from our precise characterization of R.A. © 1980.