Sign up ×
MathOverflow is a question and answer site for professional mathematicians. It's 100% free, no registration required.

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 ?

share|cite|improve this question
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

1 Answer 1

up vote 5 down vote accepted

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.

share|cite|improve this answer
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

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.