Triangular Numbers are Primitive Recursive

Theorem

Let $t : \N \to \N$ be defined as:

$\map t k = T_k$

where $T_k$ is the $k$-th triangular number.

Then $t$ is a primitive recursive function.

Proof

Define $f : \N^0 \to \N$ as:

$\map f {} = 0$.

Define $g : \N^2 \to \N$ as: $\map g x y = x + y + 1$.

By Constant Function is Primitive Recursive and Addition is Primitive Recursive:

$f$ and $g$ are primitive recursive.

By definition of primitive recursive, it suffices to show that $t$ is obtained by primitive recursion from $f$ and $g$.

That is, to show that, for all $n \in \N$:

$\map t n = \begin{cases}

\map f {} & : n = 0 \\ \map g {n - 1, \map t {n - 1}} & : n > 0 \end{cases}$

As:

$\map f {} = 0$

$\map g {n - 1, \map t {n - 1}} = n - 1 + \map t {n - 1} + 1$

$\map t k = T_k$ for all $k \in \N$

that is equivalent to showing:

$T_n = \begin{cases}

0 & : n = 0 \\ n + T_{n - 1} & : n > 0 \end{cases}$ which is the definition of triangular numbers.

$\blacksquare$