Update: The answer shows that some tweaking is necessary to get this to work. The problem are those $f$ where there exist an $N$ such that $f(n)$ is always odd for $n \ge N$. But this can be remedied in a simple way -condition $\text{(2)}$ below is dropped and we just handle these 'overloaded' functions by equating them to 'there equal'.
If $f$ is overloaded there is a least $k$ (that might be $0$ with $f(0)$ also odd) so that $f(m)$ is odd for all $m \gt k$. We define a function $g$ that agrees with $f$ for $n \lt k$, has $g(k)=f(k)+1$ and for $m \ge k$, we recursively define $g(m + 1) = 2 * g(m)$. This function $g(x)$ is not overloaded.
Then, considering these two functions as equivalent the problem goes away.
So, we can define a binary operation that is obviously commutative. Interestingly, when adding numbers, if one is overloaded we can't use that representation in the definition of the binary operation – you must use that other representation in the two element block of the (really fine-grained) partition. So the necessity of condition $\text{(2)}$ below 'melts away;.
But showing that the operation is associative is not immediate. I think we can do this by using the fact that the binary operation is 'continuous'; c.f.
Prove Addition is Continuous (without epsilon-delta!)
When I work out the details I will post them in a another proof-checking question.
Incidentally, the purpose of this is to create a model of the positive real numbers under addition. Intuitively, you can think of the function $f$ as representing a canonical Cauchy sequences; for every $x$ there is one and only one $f$ with
$\quad x = \lim\limits_{n \to +∞} f(n) \, 2^{-n}$
But note that this is quite different – the real numbers with $+$ are being directly constructed ab initio; it is not necessary to define or use the rational numbers as an intermediate step. A computer running an artificial intelligence program might be able to 'understand' this construction easier than the usual methods.
Here $0 \in \mathbb N$.
Definition: A function $f: \mathbb N \to \mathbb N$ is called a Eudoxus magnitude if it satisfies the following:
$\tag 1 \forall n \; f(n+1) = 2f(n) \text{ or } f(n+1) = 2f(n) + 1$
$\tag 2 \forall\, m \; \exists \, n \ge m \; \text{ such that } f(n+1) = 2f(n)$
One interesting thing about a Eudoxus magnitude $f$ is that if we know the value of $f$ at $n$, then the value at all smaller numbers is determined:
$\tag 3 f(n-1) = \text{the quotient (Euclidean division) of dividend } f(n) \text{ by divisor } 2$.
Also, given any number $k$, we can create a Eudoxus magnitude with $f(n) = k$ using $\text{(3)}$.
I've come up with a way of adding two Eudoxus magnitudes (not pointwise addition) $f$ and $g$ as follows.
For any integer $n \ge 0$ such that $f(n+1) = 2f(n)$ or $g(n+1) = 2g(n)$, set $k = f(n) + g(n)$ and create a (partial) Eudoxus magnitude $h$ with $h(n) = k$ and defined on $[0,n]$.
In words, we look for an even output of either function at $n + 1$, then working on the initial segment $[0,n]$ take point-wise addition on $n$ and then 'ripple back' with $\text{(3)}$.
Claim: The value of the partial functions obtained by using different integers $n$ where $f(n+1) = 2f(n)$ or $g(n+1) = 2g(n)$ always agree on their common initial integer intervals.
If this is true, we've defined a unique function $h: \mathbb N \to \mathbb N $ by just 'going out further towards' $+\infty$. A bonus is that we can then immediately assert that the 'Eudoxus sum' $\oplus$ of two Eudoxus magnitudes is a Eudoxus magnitude.
I would like to prove this using only elementary number theory and logic. But besides writing a Python program to check out the coherence of this endeavor, at this point I don't have any proof at all.
Question 1: Can the above claim be established using any mathematical
theories?
Best Answer
The claim$^1$ is false: the operation you've described doesn't always output a Eudoxus magnitude. In particular - and shifting from functions to sequences for ease of writing - take $$f=(1,2,5,10,21,...),\quad g=(1,3,6,13,26,...)$$ (the important feature being that each doubles infinitely often, but they never double at the same time). Then when we try to build their "Eudoxus sum" according to your rule, we have good news and bad news. On the plus side, the "initial segment sums" we get agree with each other; however, on the minus side we get the sequence $$(2,5,11,23,37,...)$$ which never doubles and hence fails to satisfy condition $(2)$.
Dropping condition $(2)$ from the definition doesn't help: the sequence $$(1,3,7,15,31,...)$$ would then be considered a Eudoxus magnitude, but there's no good way to define "Eudoxus sum" so as to not have its Eudoxus sum with itself violate $(1)$.
What you need is a way to ensure frequent simultaneous doubling. You can ensure this by strengthening condition $(2)$; e.g. you'll get better results if you demand that $f$ is a Eudoxus magnitude only if its set of doubling points has asymptotic density $1$ (since the intersection of two asymptotic-density-$1$ sets has asymptotic density $1$). But I suspect such a requirement will ruin things elsewhere, namely the original motivation for these.
$^1$This is a bit unfair of me. Your actual claim as written is just that we never see disagreement between the "initial segment sums," and it's not hard to show that this is in fact true. But implicitly, you want the output to again be a Eudoxus magnitude ("A bonus is that we can then immediately assert that the [Eudoxus sum] of two Eudoxus magnitudes is a Eudoxus magnitude.") and this doesn't hold.