Computational complexity of logical theories of one successor and another unary function (Q868664)

This paper studies the set of natural numbers as a universe equipped with equality as the unique relation and simple, usual unary, functions as basic operations. The logic theory derived from the above is proven to be complete for some choices of the unary function. In particular, it is known that this is the case for the unary functions \(x+1\), \(2x\), \(x^2\) and \(2^x\), where equality is the only relation assumed. The author extends the result to the first-order logical theory derived by the function \(x+1\) combined with the functions \(c^x\) and \(x^c\). The article begins with an overview of the necessary definitions and other preliminaries, which is then followed with an extensive series of theorems, lemmas and corollaries with complete proofs. Completeness is assumed for the class ATIME-ALT\((2^{O(n)},O(n))\) throughout this article. The paper concludes with a list of relevant articles.