Computational complexity of logical theories of one successor and another unary function

摘要

The first-order logical theory Th $({mathbb{N}},x + 1,F(x))$ is proved to be complete for the class ATIME-ALT $(2^{O(n)},O(n))$ when $F(x) = 2^{x}$ , and the same result holds for $F(x) = c^{x}, x^{c} (c in {mathbb{N}}, c ge 2)$ , and F(x) = tower of x powers of two. The difficult part is the upper bound, which is obtained by using a bounded Ehrenfeucht–Fra?ssé game.