On the complexity of the theories of weak direct powers
Charles Rackoff · Journal of Symbolic Logic · 1976
Abstract Mostowski [11] shows that if a structure has a decidable theory, then its weak direct power has one as well; his proof however never produces decision procedures which are elementary recursive. Some very general results are obtained here about the nature of the weak direct power of a structure, which in most cases lead to elementary recursive decision procedures for weak direct powers of structures which themselves have elementary recursive procedures. In particular, it is shown that 〈N*, +〉, the weak direct power of 〈N, +〉, can be decided in space for some constant c. As corollaries, the same upper bound is obtained for the theory of the structure 〈N+, ·〉 of positive integers under multiplication, and for the theory of finite abelian groups. Fischer and Rabin [7] have shown that the theory of 〈N,* +〉 requires time even on nondeterministic Turing machines.