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

$\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\rfloor1,$$ 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 $nF_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 $(*)$. 


Suppose, toward a contradiction, that $f$ is definable in Presburger arithmetic. By quantifier elimination for Presburger arithmetic, there must be a constant $M$ such that, on each congruence class modulo $M$, $f$ is an affine function $f(n)=an+b$ except for finitely many $n$'s, and the coefficient $a$ of the linear term is rational. Furthermore, since $f$ is clearly monotone, these coefficients $a$ must be the same for all of the congruence classes. Now consider (approximately) what happens when we compute, using the inductive definition, $f(n)$ for a large $n$, large enough so that the constant terms $b$ are negligible. $f(n)$ is defined as the first number different from the $n$ numbers $f(k)$ and the $n$ other numbers $f(k)+k+1$ for all $k$ in the range $0\leq k<n$. Notice first that "other" is literally correct; no number appears in both sets of $n$. How many of these $2n$ numbers are relevant in the sense that they are below $f(n)$ and thus really matter in the calculation of $f(n)$? One answer to this question is $f(n)$, since $f(n)$ is the first number above all of them; remember that this is roughly $an$. Another answer is that all of the first set of $n$ (the values of previous $f(k)$'s) are relevant, but in the second set, whose largest elements are roughly $an+n$, only those below roughly $an$ are relevant. Altogether, we have roughly $n+(an/(an+n))=n(2a+1)/(a+1)$ relevant numbers, and $f(n)$, being the first number different from these, is roughly of this size. Thus, we must have $a=(2a+1)/(a+1)$. This means that $a$ must equal the golden ratio. But we know, from quantifier elimination, that $a$ must be rational. This contradiction shows that $f$ cannot be definable in Presburger arithmetic. 

