Let $f:\mathbb{N}\to\mathbb{N}$ be defined in the following recursive way: for any $n$ in $\mathbb{N}$, $f(n)$ is the least natural number different from all $f(k)$ and $f(k)+k+1$ with $k<n$ (for instance, $f(0)=0$, $f(1)=2$, $f(2)=3$, $f(3)=5$). Is it possible to define this function in the language of Presburger arithmetic (the same question about the function defined as above, but with $f(k)+k$ instead of $f(k)+k+1$)?



About some functions in the set of the natural numbers
$\let\fii\varphi\let\ol\overline$Andreas has already answered the original question, however it was raised in the comments whether $f$ coincides with the sequence in <http://oeis.org/A022342>:
$$\tag{$\*$}f(n)=\lfloor n\fii+\fii^{-1}\rfloor=\lfloor(n+1)\fii\rfloor-1,$$
where $\fii=(1+\sqrt5)/2$ is the golden ratio, so let me argue that this is indeed the case.


Every integer $n\ge0$ can be written as $n=\ol a:=\sum\_{i=2}^\infty a\_iF\_i$, where $F\_i$ is the $i$th Fibonacci number, and $a=(a\_i)\_{i\ge2}$ is a sequence such that $a\_i\in\{0,1\}$, $a\_i=0$ for all but finitely many $i$, and no two consecutive elements of $a$ are $1$. (We can find find such a representation recursively by choosing the largest $i$ such that $F\_i\le n$, and combining it with a representation of $n-F\_i$. This is known as the Zeckendorf expansion of $n$.) Let $A$ denote the set of all such sequences $a$. It is easy to see that if $i$ is the largest index of a nonzero element of $a\in A$, then $\ol a< F\_{i+1}$; it follows that $\ol a< \ol b$ iff $a< b$ in the lexicographic order. In particular, the representation is *unique*.


Define $f'\colon\mathbb N\to\mathbb N$ by $f'(\ol a)=\ol{a0}$, where for $u\in\{0,1\}$, $au$ denotes the concatenation of $u$ and $a$: $(au)\_{i+1}=a\_i$, $(au)\_2=u$. In other words, $f'(\ol a)=\sum\_ia\_iF\_{i+1}$. Clearly, $f'$ is an increasing function. Moreover,
$$f'(\ol a)+\ol a+1=\sum\_ia\_i(F\_i+F\_{i+1})+1=\sum\_ia\_iF\_{i+2}+F\_2=\ol{a01}.$$
It follows that $\mathbb N$ is the disjoint union of $\{f'(k):k\in\mathbb N\}$ and $\{f'(k)+k+1:k\in\mathbb N\}$. Then it is easy to show
$$f(n)=f'(n)$$
by induction on $n=\ol a$: indeed, $a0$ is the lexicographically least sequence in $A$ excluded from $\{b0,b01:b< a\}$.


Since $F\_i=\bigl(\fii^i-(-\fii)^{-i}\bigr)/\sqrt5$, we have
$$f(n)-\fii n=\sum\_{i:a\_i=1}(F\_{i+1}-\fii F\_i)=\sum\_{i:a\_i=1}(-\fii)^{-i}\frac{\fii^{-1}+\fii}{\sqrt5}=\sum\_{i:a\_i=1}(-\fii)^{-i}.$$
Thus,
\begin{align\*}
f(n)-\fii n&< \sum\_{\substack{i\ge2\\\\i\text{ even}}}\fii^{-i}=\frac{\fii^{-2}}{1-\fii^{-2}}=\fii^{-1},\\\\
f(n)-\fii n&>-\sum\_{\substack{i\ge2\\\\i\text{ odd}}}\fii^{-i}=-\frac{\fii^{-3}}{1-\fii^{-2}}=-\fii^{-2}=\fii^{-1}-1,
\end{align\*}
which shows $(\*)$.


