About some functions in the set of the natural numbers 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$)?
 A: 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.
A: $\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 $(*)$.
