A formula expressing that $ m = \sum^n_{i=1} i^n $

Question

Write a such formula $\phi(x,y) $ in arithmetic language that $(\mathbb{N}, x : n, y : m) \models \phi(x,y) \iff m = \sum^n_{i = 1}i^n $

So why cannot I write: $\phi (x,y): y = 1^x + 2^x + 3^x + .. + x^x$

But it seems to be too simple.

Answer 1

There is no built in summation operation in first order logic, or anything dealing with a series of variable length. So, you want to do this recursively:

Define a function $sum(z,x)$ that you want to be $\sum^z_{i=1} i^x$ as follows:

$\forall x \: sum(1,x)=1$

$\forall z \forall x \: sum(s(z),x) = sum(z,x) + s(z)^x$

Here, $s(z)$ is the successor of $z$, i.e. $z+1$, and it is also assumed you have a function $x^y$ ... You can refer to the axioms of Peano Arithmetic here if needed, where the power function can be defined recursively similar to how addition and multiplication are defined recursively:

$\forall x \: x^0 = 1$

$\forall x \forall y \: x^{s(y)}=x^y * x$

With the above $sum(z,x)$ function, you can define your $\phi (x,y)$ as follows:

$\forall x \forall y (\phi(x,y) \leftrightarrow y = sum(x,x))$

Answer 2

Actually getting a first-order formula in arithmetic that expresses this is a bit long and unwieldy:

If this is a homework assignment, I presume you have covered in class some way of coding arbitrarily long finite sequences of natural numbers as natural numbers. (This can be done, for example, using prime decomposition or via Cantor's pairing function.) In developing this, you would get first order formulas that are equivalent to \begin{align}"\!x\text{ codes}&\text{ a finite sequence of length }y\!",\tag{1} \\"\!x\text{ codes}&\text{ a finite sequence, }\\&y\text{ is less than the length of that finite sequence,}\\&\text{and }z\text{ is the }y^{\text{th}}\text{ element in that finite sequence (starting the indexing at }0)\!",\tag{2}\end{align} etc.

You can then write $x=y^z$ as:

\begin{align}(\exists w)\Big((w&\text{ codes a finite sequence of length }z+1)\;\land \\&\text{(the }0^\text{th}\text{ element of that finite sequence}=1)\;\land \\&(\text{the }z^\text{th}\text{ element of that finite sequence}=x)\;\land \\&(\forall v)\big(v\lt z \rightarrow(y\cdot(\text{the }v^\text{th}\text{ element of the sequence coded by }w)=(\text{the }(v+1)^\text{st}\text{ element of the sequence coded by }w)\big)\Big). \end{align}

In a similar fashion, and using the formula for $x=y^z$ above, you can write a first-order formula in arithmetic that expresses $m = \sum^n_{i = 1}i^n$ as:

\begin{align} (\exists w)\Big((w&\text{ codes a finite sequence of length }n+1)\;\land \\&\text{(the }0^\text{th}\text{ element of that finite sequence}=0)\;\land \\&(\text{the }n^\text{th}\text{ element of that finite sequence}=m)\;\land \\&(\forall v)\big(v\lt n \rightarrow (\exists u)\big((u=i^{v+1})\land \\&\hphantom{\big(v\lt n \rightarrow (\exists u)\big((u=i}u+(\text{the }v^\text{th}\text{ element of the sequence coded by }w) \\&\hphantom{\big(v\lt n \rightarrow (\exists u)\big((u=i)\big)}=(\text{the }(v+1)^\text{st}\text{ element of the sequence coded by }w)\big)\big)\Big). \end{align}

Expand everything out in full and you'll get a first-order formula of arithmetic with the property you wanted.