A logical approach to the problem of representation of integers by systems of diagonal forms

It is suspected that there exists no algorithm to decide whether or not an arbitrary finite system of diagonal quadratic forms represents an arbitrary given vector of integers. Motivated by this problem, we prove undecidability of the positive existential theory of Z in languages that contain {0, 1,+} and, either divisibility and 'is a k-th power' (for any fixed k epsilon 2), or divisibility and the exponential 'n& k(n)' (for any fixed k epsilon 2), or 'is a square' and a relation R-k strictly contained in the divisibility relation (for any fixed k epsilon 1). We also prove a similar result conditionally in the language {0, 1,+, 'xy is a square'}.