Can the canonical Eudoxus-real representatives be defined easily?

Question

(See e.g. here for background on the Eudoxus reals, which motivates this question.)

Let $\mathcal{Z}=(\mathbb{Z};+,<)$. Say that a Eudoxus function is an $f:\mathbb{Z}\rightarrow\mathbb{Z}$ such that $\{\vert f(a)+f(b)-f(a+b)\vert: a,b\in\mathbb{Z}\}$ is bounded, and a canonical Eudoxus function is a Eudoxus function of the form $c_\alpha: x\mapsto \lfloor \alpha x\rfloor$ for some real $\alpha$. Two Eudoxus functions $f,g$ are equivalent iff $\{\vert f(a)-g(a)\vert: a\in\mathbb{Z}\}$ is bounded.

Both the class of Eudoxus functions and equivalence of such are definable over $\mathcal{Z}$ in the appropriate sense: there are formulas $\varphi[F],\eta[F,G]$ in the expansions of the language of $\mathcal{Z}$ by one and two new function symbols respectively such that $(\mathcal{Z},f)\models\varphi$ iff $f$ is a Eudoxus function and $(\mathcal{Z},f,g)\models\eta$ iff $f$ and $g$ are equivalent Eudoxus functions. My question is whether the canonical Eudoxus functions are similarly definable:

Is there a sentence $\sigma$ in the language of $\mathcal{Z}$ expanded by a new unary function symbol $H$ such that $(\mathcal{Z},h)\models\sigma$ iff $h$ is a canonical Eudoxus function?

If we include multiplication in our language we get a positive answer (via coding of finite sequences), but the resulting definition isn't very natural. Essentially, I'm asking whether there is a "nice" definition of canonicity. I would be happy to replace $\mathcal{Z}$ with any similarly-"tame" expansion if that would help.

Answer 1

I can do it with these two axioms:

For all $a,b\in \mathbb Z$ we have either $f(a+b)=f(a)+ f(b)$ or $f(a+b)=f(a)+f(b)+1$.

For each $a\in \mathbb Z$, there exists a positive integer $b\in \mathbb Z$ with $f(a+b)=f(a)+f(b)$ and a negative integer $b\in \mathbb Z$ with $f(a+b) =f (a)+f(b)$.

Proof: In particular the first axiom implies $f(a+b) \geq f(a)+f(b)$ so $f(na) \geq n f(a)$ so $\lim_{n \to \infty} \frac{f(na)}{n} \geq f(a) $ but it also implies $f(a+b) \leq f(a)+ f(b)+1$ so $f(na) \leq n f(a)+ (n-1)$ so $\lim_{n\to\infty} \frac{f(na)}{n} \leq f(a)+1$

For $f$ a Eudoxus real associated to the usual real number $\alpha$ we have $ \lim_{n\to\infty} \frac{f(na)}{n}=a\alpha$ so this gives that $f(a)$ is an integer between $a\alpha-1$ and $a \alpha$. This gives $f(a) = \lfloor a \alpha \rfloor$ unless $a=0$ or $\alpha$ is a rational number and $a$ is a multiple of the denominator of $\alpha$, in which case we have two choices, either $a \alpha$ or $a\alpha-1$. If $a$ and $b$ are sent to $a\alpha$ and $b \alpha$ respectively then $a+b$ is sent to $(a+b)\alpha$, and similarly if $a$ and $b$ are sent to $a\alpha-1$ and $b\alpha-1$ respectively then $a+b$ is sent to $(a+b)\alpha-1$, so we must make the same choice for all positive integer multiples of the denominator and all negative integer multiples of the denominator. We also have to make this choice for $0$. However, the second axiom forces us to always choose $a\alpha$, giving $f(a)=\lfloor a\alpha \rfloor$:

If $f(a) =a \alpha-1$ for all positive integer multiples of the denominator then $f(a+b) \neq f(a)+f(b)$ when $a$ is one of these values and $b$ is positive, violating the second axiom, and similarly if $f(a)=a\alpha-1$ for all negative integer multiples of the denominator then $f(a+b) \neq f(a)+f(b)$ when $a$ is one of these values and $b$ is negative, so in fact $f(a) = \lfloor a \alpha \rfloor$ for all nonzero $a$.

Also if $f(0)=-1$ then $f(0+b)\neq f(0)+f(b)$ for all $b$, violating the second axiom.