The sum of the first $n$ natural numbers is $n(n+1)/2.$ How do we express this in Peano arithmetic? The following is a well-known proposition. $$\forall n \in \mathbb{N} :\sum_{j=1}^n j = \frac{n(n+1)}{2}$$
How do we actually express a sentence like this in the language of Peano Arithmetic?
 A: The expression $n \mapsto \sum_{j=1}^{n} j$ can be regarded as defining a certain primitive recursive function $f$:
\begin{align}
f (0) & = 0 \\
f (n + 1) & = f (n) + n + 1
\end{align}
Gödel has shown that every primitive recursive function is definable in Peano arithmetic. In our case, that means there exists a formula $\varphi (x, y)$ such that PA proves:


*

*$\varphi (x, y)$ is functional.

*$\varphi (0, 0)$.

*$\forall x . \varphi (x, y) \to \varphi (x+1, y + x + 1)$


The formula $\varphi$, even for such a simple function, is rather complicated. The hardest part is to develop a coding for finite lists of natural numbers. Once we have this, $\varphi (x, y)$ essentially says that there exists $L$ coding a finite list such that:


*

*The $0$-th entry of $L$ is $0$.

*If the $n$-th entry of $L$ is $a$, and $L$ has an $(n+1)$-th entry, then the $(n+1)$-th entry is $a + n + 1$.

*$L$ has an $x$-th entry.

*The $x$-th entry of $L$ is $y$.


The theorem you wish to state can then be formalised as follows:
$$\forall x. \exists y. \varphi (x, y) \land (2 \times y = x \times (x + 1))$$
A: You are interested in $f(n) = \sum_{j=0}^n j$. But evidently $f$ is primitive recursive, and there is a standard trick due to Gödel for expressing any primitive recursive function in the language of PA by deploying his so-called $\beta$-function [now outlined by Zhen Lin]. 
The clearest fuller explanation of that which I know is in P*t*r Sm*th's Introduction to Gödel's Theorems, Ch. 15 of the second edition (which is a bit too long to cut'n'paste here)! 
