Can any Power function (whose base is not zero) , e.g. $2^{n}$, be defined arithmetically (i.e. using addition and multiplication only)?

92 Views Asked by At

In other words, I'm looking for a binary relation $P(x,y)$, being arithmetical, i.e being expressed in the first order language of Peano arithmetic (hence non-recursively, i.e. using addition and multiplication only - without using the very symbol $P$), which satisfies:

  1. For every $x$, there exists a unique $y$, satisfying $P(x,y)$.
  2. $P(0,1)$.
  3. Every $x,y$, satisfying $P(x,y)$, satisfy $P(x+1,2y)$.

If such an arithmetical function (as defined above) does not exist, I will be glad to read the proof of this fact.

(No Gödel's coding please).