1
$\begingroup$

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 ?

Improve this question
$\endgroup$
2
  • 1
    $\begingroup$ 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? $\endgroup$
    – Charles Stewart
    Commented Aug 11, 2010 at 9:49
  • $\begingroup$ 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?" $\endgroup$
    – Akshar Prabhu Desai
    Commented Aug 11, 2010 at 11:29

1 Answer 1

Reset to default
5
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • 7
    $\begingroup$ 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. $\endgroup$
    – Joel David Hamkins
    Commented Aug 11, 2010 at 9:41

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .