How is exponentiation defined in Peano arithmetic?

How would exponentiation be defined in Peano arithmetic? Unless $n$ is fixed natural number, $x^n$ seems to be hard to define.

Edit 2: So, what would be the way to define $x^n+y^n = z^n$ using $\Sigma_1^0$ formula?

Edit: OK, I say Peano arithmetic has addition and multiplication stuffs. This allows additions to be expressed without quantifiers but as for exponentiation Peano arithmetic is silent. That's why I asked this question. Just for clarification.

The bare bones answer is something like what Hagen has said. The idea is this: Exponentiation is understood to be a function defined recursively: $y=2^x$ iff there is a sequence $t_0,t_1,\dots,t_x$ such that

• $t_0=1$,
• $t_x=y$, and
• For all $n<x$, $t_{n+1}=2\times t_n$.

In this respect, exponentiation is hardly unique: $y=x!$ is defined similarly, for example. Now you'd say that there is a sequence $z_0,z_1,\dots,z_x$, such that

• $z_0=1$,
• $z_x=y$, and
• For all $n<x$, $z_{n+1}=(n+1)\times z_n$.

(That $t_0=z_0=1$ is coincidence. In one case it is because $2^0=1$; in the other, because $0!=1$.)

So, to define a formula saying that $y=2^x$, you'd like to say that there is a sequence $t_0,\dots,t_x$ as above.

The problem, of course, is that in Peano Arithmetic one talks about numbers rather than sequences. Gödel solved this problem when working on his proof of the incompleteness theorem: He explained how to code finite sequences by numbers, by using the Chinese remainder theorem. Recall that this result states that, given any numbers $n_1,\dots,n_k$, pairwise relatively prime, and any numbers $m_1,\dots,m_k$, there is a number $x$ that simultaneously satisfies all congruences $$x\equiv m_i\pmod {n_i}$$ for $1\le i\le k$.

In particular, given $m_1,\dots,m_k$, let $n=t!$ where $t=\max(m_1,\dots,m_k,k)$. Letting $n_1=n+1$, $n_2=2n+1,\dots$, $n_k=kn+1$, we see that the $n_i$ are relatively prime, and we can find an $x$ that satisfies $x\equiv m_i\pmod{n_i}$ for all $i$. We can then say that the pair $\langle x,n\rangle$ codes the sequence $(m_1,\dots,m_k)$. In fact, given $x,n$, it is rather easy to "decode" the $m_i$: Just note that $m_i$ is the remainder of dividing $x$ by $in+1$.

Accordingly, we can define $y=2^x$ by saying that there is a pair $\langle a,b\rangle$ that, in the sense just described, codes a sequence $(t_0,t_1,\dots,t_x)$ such that $t_0=1$, $t_x=y$, and $t_{n+1}=2t_n$ for all $n<x$. (Again, "in the sense just described" ends up meaning simply that "the remainder of dividing $a$ by $ib+1$ is $t_i$ for all $i\le x$". Note that we are not requiring $b$ to be the particular number we exhibited above using factorials.)

Of course, one needs to prove that any two pairs coding such a sequence agree on the value of $t_x$, but this is easy to establish. And we can code a pair by a number using, for example, Cantor's enumeration of $\mathbb N\times\mathbb N$, so that $\langle a,b\rangle$ is coded as the number $$c=\frac{(a+b)(a+b+1)}2+b.$$ This is a bijection, and has the additional advantages that it is definable and satisfies $a,b\le c$ (so it is given by a bounded formula).

An issue that appears now is that we need to formalize the discussion of the Chinese remainder theorem and the subsequent coding within Peano arithmetic. This presents new difficulties, as again, we cannot (in the language of arithmetic) talk about sequences, and cannot talk about factorials, until we do all the above, so it is not clear how to prove or even how to formulate these results.

This problem can be solved by noting that we can use induction within Peano arithmetic. One then proceeds to show, essentially, that given any finite sequence, there is a pair that codes it, and that if a pair codes a sequence $\vec s$, and a number $t$ is given, then there is a pair that codes the sequence $\vec s{}^\frown(t)$. That is, one can write down a formula $\phi(x,y,z)$, "$y$ codes a sequence, the $z$-th member of which is $x$", such that PA proves:

• For all $z$ and $y$ there is a unique $x$ such that $\phi(x,y,z)$.
• For all $x$ there is a $y$ such that $\phi(x,y,0)$.
• For all $x,y,z$ there is a $w$ such that the first $z$ terms of the sequences coded by $y$ and $w$ coincide, and the next term coded by $w$ is $x$.

In fact, we can let $\phi$ be a bounded formula: Take $\phi(x,y,z)$ to be

There are $a,b\le y$ such that $y=\langle a,b\rangle$ (Cantor's pairing) and $x<zb+1$ and there is a $d\le a$ such that $a=d(zb+1)+x$.

Once we have in PA the existence of coded sequences like this, implementing recursive definitions such as exponential functions is straightforward.

There are two excellent references for these coding issues and the subtleties surrounding them:

1. Richard Kaye. Models of Peano arithmetic. Oxford Logic Guides, 15. Oxford Science Publications. The Clarendon Press, Oxford University Press, New York, 1991. MR1098499 (92k:03034). (See chapter 5.)
2. Petr Hájek, and Pavel Pudlák. Metamathematics of first-order arithmetic. Perspectives in Mathematical Logic. Springer-Verlag, Berlin, 1993. MR1219738 (94d:03001). (See chapter 1.)
• Curiously, I just gave a talk in the set theory seminar at Boise State on this question: math.stackexchange.com/questions/282865/…, so I had just (re)worked through these details. Commented Feb 24, 2013 at 17:01
• As for $\phi (x,y,z)$, bounded formula, it's $\Sigma^0_0$ formula, I guess, right? (But I heard that $\Sigma^0_0$ formula can also refer to quantifier-free formula, so which definition is usually used in this case?)
– UQT
Commented Feb 28, 2013 at 5:33
• (There was a typo on my previous comment, it is fixed in this version.) Bounded is the usual definition. Sometimes, in the context of Hilbert's $10$-th problem, one talks of $\Sigma_0=\Pi_0=\Delta_0$ being quantifier free, and $\Sigma_1$ being existential quantification over $\Sigma_0$, so the Davis-Matiyasevich-Putnam-Robinson result can be stated succinctly as $\Sigma^0_1=\Sigma_1$. Commented Mar 1, 2013 at 6:00
• You have an off-by-one indexing error, in your explicit definition for $\phi$ at the end. You have $\phi(x,y,0)$ logically implies $x<0b+1$ and thus $x=0$, and this contradicts the requirement $\forall x, \exists y, \phi(x,y,0)$ outlined in the second bullet. I think you meant to write $x<(z+1)b+1$ and likewise $a=d((z+1)b+1)+x$, which would fix the error. Alternatively you could adjust the second bullet to start at index $1$ instead of index $0$, either way works. Commented Mar 26, 2023 at 9:57
• Thank you very much Andrés, excellent exposition. I would add that it is important to underline that the definition of exponentiation, or of any other recursive function, obtained from working with codings of sequences is a bona fide definition, not just an encoded version of the exponential; that is, the resulting existence and uniqueness formula proved in PA is for the actual value of the exponential, and we can add a function symbol to the language defining it with the use of that formula -thus adding a "trivial" axiom. I say this because the machinery may make it not obvious.
– plm
Commented Aug 26, 2023 at 21:27

Using the following abbreviations

\begin{align}a\le b&\equiv\exists n\colon a+n=b\\ a< b&\equiv Sa\le b\\ \operatorname{mod}(a,b,c)&\equiv \exists n\colon a=b\cdot n+c\land c<b\\ \operatorname{seq}(a,b,k,x)&\equiv \operatorname{mod}(a,S(b\cdot Sk),x)\\ \operatorname{pow}(a,b,c)&\equiv\exists x\exists y\colon\operatorname{seq}(x,y,0,S0)\land\operatorname{seq}(x,y,b,c)\land \\&\quad\forall k\forall z\colon((k<b\land \operatorname{seq}(x,y,k,z))\to \operatorname{seq}(x,y,Sk,a\cdot z))\end{align} we have $\operatorname{pow}(a,b,c)$ if and only if $c=a^b$. Intriguingly, you need some elementary number theory (such as the Chinese remainder theorem) to meta-appreciate this.

Example: In order to show that $\operatorname{pow}(10,3,1000)$ is true (i.e., that $10^3=1000$), you may want to try $x=41366298973$ and $y=250$ in the formula above, i.e., verify that $\operatorname{seq}(x,y,0,1)$, $\operatorname{seq}(x,y,1,10)$, $\operatorname{seq}(x,y,2,100)$, and $\operatorname{seq}(x,y,3,1000)$. (It does not matter that $\operatorname{seq}(x,y,4,1138)$ instead of $\operatorname{seq}(x,y,4,10000)$).

• What, intuitively, does $\text{seq}$ mean? Commented Jul 29, 2016 at 15:52
• Does the $S$ preceding terms represent the successor of a number? Commented Jul 29, 2016 at 20:05
• @PyRulez $\operatorname{seq}(a,b,k,x)$ means "$x$ is the $k$th term in the somewhat strangely defined sequence $a\bmod{b+1},a\bmod {2b+1},a\bmod{3b+1},\ldots$". Remarkably, any finite sequence can be represented this way. So $\operatorname{pow}(a,b,c)$ mans "There exists a finite sequence $x_0,x_1,x_2,\ldots,x_m$ with $x_0=1$ and $x_b=c$ and for $0\le k<b$ we have $x_{k+1}=a\cdot x_k$". (Writing this down explicitly just made me spot a typo, which I'll correct now) Commented Jul 30, 2016 at 10:58
• I guess you can't use prime factorizations to store sequences of numbers since that would involve exponents, right? Commented Jul 30, 2016 at 11:48
• @PyRulez seq is the Godel beta function en.wikipedia.org/wiki/G%C3%B6del%27s_%CE%B2_function Commented Oct 20, 2018 at 20:49