lo.logic - Exponent function as uninterpreted function in first order logic

The function $f(m,n)=m^n$ is primitive recursive, so expressible in
first-order arithmetic: there is a formula in three free variables
$F(m,n,p)$ over the language of first-order arithmetic
which is valid in Peano arithmetic for numerals $m$, $n$ and $p$ iff $p=m^n$.

Logic texts (e.g. Boolos and Jeffrey) will prove that primitive recursive
functions can be expressed in this way, but the general method does
not tend to provide nice formulas for concrete examples like this.