Eliminating Bounded Universal Quantifier
In  the necessity to work with long arithmetical progressions consisting of primes only was due to the usage of a version of Godel’s technique for coding arbitrary long sequences of natural numbers via the Chinese Remainder Theorem. Julia Robinson has managed to replace such progressions by arithmetical progressions composed of pairwise relatively prime numbers having arbitrary large prime factors. Much later, in 1972, using a multiplicative version of Dirichlet principle, I  made further modification allowing one to work just with arithmetical progressions of arbitrary big relatively prime numbers.
In [37, Sect. 6.3] I introduced a quite different technique for eliminating bounded universal quantifier based on replacing Vy<z by Xzy=0 with a suitable summand allowing one to find a closed form for the corresponding sum.
The method for constructing the Davis normal form (2.6) presented in  starts with a representation of the set M by an arithmetical formula in prenex form with any number of bounded universal quantifiers constructed, for example, by Godel’s technique. Two tools are repeatedly applied to such a formula, one tool allowing us to glue two consecutive existential or universal quantifiers, and the other tool giving the possibility to change the order of consecutive universal and existential quantifiers. The footnote on page 36 in  tells us that the idea of this construction belongs to an unknown referee of the paper.
Nevertheless, the main theorem from  does belong to Martin Davis, but his original proof presented in  was quite different. Namely, for the initial representation of listable sets he used normal systems introduced by his teacher Post. Thanks to the great simplicity of the normal systems Martin Davis was able to arithmetize them in a very economical way using only one bounded universal quantifier.
While Martin Davis remarks in the same footnote that the proof presented in the paper is shorter that his original proof, the latter was very appealing to me: now that we know that there is no need to use bounded universal quantifiers at all, could not we perform completely existential arithmetizing, thus avoiding universal quantifiers?
Finally I was able to give such a quite different proof of the DPR-theorem based on arithmetization of the work of Turing machines . In  I presented another way of simulating Turing machines by means of exponential Diophantine equations. Peter van Emde Boas proposed in  yet another, rather different way of doing it. However, James P. Jones and I found  that so called register machines are even more suitable for existential arithmetization; several versions of such “visual proof” are given in [23, 24, 35, 39].
The “advantage” of register machines over Turing machines for constructing Dio- phantine representations is due to the fact that the former operate directly with integers. However, register machines are not such a “classical” tool as Turing machines are. Esteemed partial recursive function have both properties: on the one hand they are defined on natural numbers, on the other hand, they are quite “classical”. In  I used exponential Diophantine equations for simulating partial recursive function thus giving yet another proof of the DPR-theorem.
My paper  presents a unifying technique allowing one to eliminate bounded universal quantifier and simulate by means of exponential Diophantine equations Turing machines, register machines, and partial recursive functions in the same “algebraic” style.
Thus today we have quite a few very different proofs of the celebrated DPR- theorem. In contrast, it is a bit strange that no radically new techniques were found for transforming exponential Diophantine equations into genuine Diophantine ones: all known proofs in fact are minor variations of the construction presented by Martin Davis in  (Maxim Vsemirnov  made a generalization from (2.11) and (2.14) to some recurrent sequences of orders 3 and 4 but this gives no advantage for constructing Diophantine representations).