Does Peano Arithmetic prove all identities involving addition, multiplication, and exponentiation?

Question

Consider the structure $(\mathbb{N};+,*,\uparrow,0,1)$, where $+$ denotes addition, $*$ denotes multiplication, and $\uparrow$ denotes exponentiation. Does Peano Arithmetic, augmented with the axioms $x \uparrow 0 = 1$ and $x \uparrow (y + 1) = (x \uparrow y) * x$, prove all true universally quantified equations in that structure? I know that Tarski's high school axioms fail to prove all true identities, such as Wilkie's identity. Also, if Peano arithmetic fails to prove all true identities, is there an identity that the theory proves that can't be proven from Tarski's high school axioms?

Answer 1

There is strong evidence that the answer is yes.

What is known is that the set of identities in addition, multiplication, and exponentiation is computable. This is due to Macintyre, The laws of exponentiation; unfortunately that article is behind a paywall, so see also Gurevic's Equational theory of positive numbers with exponentiation.

Now it seems that in each case, more than just computability is proved: an explicit algorithm is exhibited and verified. This means that to check that $\mathsf{PA}$ suffices we only need to show that the arguments of one paper or the other go through in $\mathsf{PA}$. At a glance this looks doable for Gurevic's paper, and I assume the same is true of Macintyre's (in the pre-paywall part of Macintyre's paper he mentions the role of calculus, but that's probably not an issue - $\mathsf{PA}$ suffices for the arithmetic consequences of everything I can think of that would be called "basic calculus").

(As to your final question, $\mathsf{PA}$ already proves Wilkie's identity: the wiki page explains why the identity is true, and it's easy to see that that reasoning goes through in $\mathsf{PA}$.)