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.)
  • 1
    $\begingroup$ 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. $\endgroup$ – Andrés E. Caicedo Feb 24 '13 at 17:01
  • $\begingroup$ 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?) $\endgroup$ – UQT Feb 28 '13 at 5:33
  • $\begingroup$ (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$. $\endgroup$ – Andrés E. Caicedo Mar 1 '13 at 6:00

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)$).

  • 1
    $\begingroup$ What, intuitively, does $\text{seq}$ mean? $\endgroup$ – PyRulez Jul 29 '16 at 15:52
  • $\begingroup$ Does the $S$ preceding terms represent the successor of a number? $\endgroup$ – someonewithpc Jul 29 '16 at 20:05
  • 1
    $\begingroup$ @someonewithpc Yes $\endgroup$ – Hagen von Eitzen Jul 30 '16 at 10:52
  • 2
    $\begingroup$ @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) $\endgroup$ – Hagen von Eitzen Jul 30 '16 at 10:58
  • $\begingroup$ I guess you can't use prime factorizations to store sequences of numbers since that would involve exponents, right? $\endgroup$ – PyRulez Jul 30 '16 at 11:48

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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