Exponentiation of course satisfies a number of nontrivial identities:
$x^{y+z}=x^yx^z$
$(x^y)^z=x^{yz}$
$x^0=1$, $x^1=x$
However, these identities all involve functions other than exponentiation (I’m thinking of $0$ and $1$ as nullary functions, here). My question is what identities hold of exponentiation alone. That is:
What is the equational theory of $(\mathbb{N}, exp)$?
To be clear, I mean “identity” in the strict, universal-algebraic sense: one term equals another term, where each term is built from variables and exponentiation alone. Also, an identity has to hold on all of $\mathbb{N}$: identities which hold only on, say, numbers divisible by $17$ don’t count.
A related question:
Is that theory axiomatized by finitely many equations?
Note: A previous version of this question asked whether there were any nontrivial identities at all. This was extremely silly of me, as pointed out almost immediately by Stefan Perko below: $(x^y)^z=(x^z)^y$.
I learned indirectly that Martin [1] showed that the identity
$(x^z)^y = (x^y)^z$ is complete for the standard model ⟨N, ↑⟩ of positive natural numbers with exponentiation. Unfortunately, I don’t have access to this article.
Could someone confirm this information?
[1] Charles F. Martin. Axiomatic bases for equational theories of natural numbers. Notices of the Am. Math. Soc., 19(7), 778 (1972).