I was thinking about Tarski's problem, and was wondering what happens if we have a theory $T$ with two sorts $N,Z$ with intended interpretations $\def\nn{\mathbb{N}}$$\def\zz{\mathbb{Z}}$$\nn,\zz$ respectively, and we axiomatize arithmetic on $\zz$, including addition, subtraction, multiplication and non-negative exponentiation as follows:
$0,1$ are (overloaded) constants of sort $Z$ or $N$ [the context is sufficient to disambiguate them].
$+,\times$ are (overloaded) binary functions with signature $(Z,Z;Z)$ or $(N,N;N)$.
$-$ is a binary function with signature $(Z,Z;Z)$.
Exponentiation is a binary function with signature $(Z,N;Z)$.
$(Z,0,1,+,-,\times)$ is a commutative ring.
$(N,0,1,+,\times)$ is a commutative semi-ring.
$x^0 = 1$. $x^1 = x$. $1^m = 1$.
$x^{m+n} = x^m \times x^n$.
$x^{m \times n} = (x^m)^n$.
$(x \times y)^m = x^m \times y^m$.
Then Wilkie's identity that disproves Tarski's conjecture can be proven within $T$:
$\left( (1+x)^m + (1+x+x^2)^m \right)^n \times \left( (1+x^3)^n + (1+x^2+x^4)^n \right)^m$
$\ = \left( (1+x)^m + (1+x+x^2)^m \right)^n \\ \quad \times \left( (1+x)^n \times (1-x+x^2)^n + (1+x+x^2)^n \times (1-x+x^2)^n \right)^m$
$\ = \left( (1+x)^m + (1+x+x^2)^m \right)^n \\ \quad \times \left( (1+x)^n + (1+x+x^2)^n \right)^m \times (1-x+x^2)^{n \times m}$
$\ = \left( (1+x)^n + (1+x+x^2)^n \right)^m \\ \quad \times \left( (1+x)^m + (1+x+x^2)^m \right)^n \times (1-x+x^2)^{m \times n}$
$\ = \left( (1+x)^n + (1+x+x^2)^n \right)^m \\ \quad \times \left( (1+x)^m \times (1-x+x^2)^m + (1+x+x^2)^m \times (1-x+x^2)^m \right)^n$
$\ = \left( (1+x)^n + (1+x+x^2)^n \right)^m \times \left( (1+x^3)^m + (1+x^2+x^4)^m \right)^n$.
My questions are:
(1) Is every identity over $T$ that is true for $(\nn,\zz)$ provable within $T$?
(1*) If so, is every identity over $T$ provable within $T$ using only the axioms and substitution?
If (1) or (1*) is false, what are explicit counter-examples?
Notes
Wilkie's paper states that, if we extend Tarski's original equational theory by adding a function symbol for each (multivariate) polynomial over $\zz$ and adding as axioms all sentences that are true in $\nn$ and do not involve exponentiation, then the resulting equational theory proves every sentence over the original theory that is true in $\nn$.
Wilkie comments that this seems the best possible positive solution to Tarski's problem, though he says that he does not know whether the extended theory proves every sentence over itself that is true in $\nn$. He also says that there would be "great difficulties of interpretation" in extending the original theory to negative integers, but I'm not sure why that is so since I have pretty much done that above.
Unfortunately, the rest of Wilkie's paper went over my head.