# Exponent function as uninterpreted function in first order logic

I want to express the following sentence in first order logic.

There are naturals numbers that can not be expressed as one natural number raised to the power of another natural number other than one.

Under normal circumstances this is very simple. I am wondering if the the exponent function involved here can be expressed as uninterpreted function. Can we use some combination of *,+ as interpreted functions to express exponent function as uninterpreted one ?

-
Talk of first-order logic and "normal circumstances" makes me unsure as to exactly what you want here. The set of interpretations open to the infix symbol "^" are the same as those open to "+" - there must be some fixing of interpretations to be able to make your language describe exponentiation: what do you have in mind? –  Charles Stewart Aug 11 '10 at 9:49
What I mean here is that we are allowed to use + with it's usual interpretation but not allowed to use ^ with it's normal interpretation. The question here is "how to express ^ as uninterpreted function?" –  Akshar Prabhu Desai Aug 11 '10 at 11:29

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$.
Basically, the definition of $y=m^n$ says that there is a number $s$ which codes a sequence of length $n$, such that the first memeber of the sequence is $m$, each member is $m$ times the previous member, and the last member is $y$. Thus, the sequence coded by $s$ is simply the recursive construction history of $m^n$. The coding of sequences is possible in a variety of ways, one of which uses the Chinese Remainder Theorrem. –  Joel David Hamkins Aug 11 '10 at 9:41