Find a (closed) defining formula for XOR

Question

I have a language $\mathcal L=\{f,g\}$ (with equality symbol $=$) where $f$ and $g$ are binary functional symbols. I will call a model $\mathfrak M$ of $\mathcal L$ "nice", if it satisfies the next conditions:

1) The universe of $\mathfrak M$ is $\mathbb N=\{0,1,2,\dots\}$,

2) $f$ is interpreted as addition operation.

I am looking for a way to find a closed formula $\varphi$ of $\mathcal L$ such that for each "nice" model $\mathfrak M$:

$\mathfrak M \models \varphi$ iff $g$ is interpreted as bitwise XOR and $f$ appears in one atomic subformula (like $t_1=t_2$) of $\varphi$.

I mean $g^\mathfrak M(\sum^{s}_{i=0}a_i \cdot 2^i, \sum^{s}_{i=0}b_i \cdot 2^i)= \sum^{s}_{i=0}((a_i + b_i)\mod2)\cdot 2^i$ for $s\in\mathbb N, a_i, b_i \in \{0,1\}$.

Thanks for any advice. $$ $$ Update (Some steps):

$\operatorname{ZERO}(n) \equiv f(n, n) = n$

$\operatorname{ONE}(j) \equiv \lnot\operatorname{ZERO}(j) \land \forall x\forall y(f(x, y) = j \rightarrow (\operatorname{ZERO}(x) \lor \operatorname{ZERO}(y)))$

We can define bitwise XOR by induction, according to number of bits of operands. $0 \oplus 0 = 0$, then for each $a,b \in N$

$2a \oplus 2b = (2a + 1) \oplus (2b + 1) = 2(a \oplus b) \\ 2a \oplus (2b + 1) = (2a + 1) \oplus 2b = 2(a \oplus b) + 1$

Answer 1

You can find a good candidate for $\varphi$ using your inductive definition of $a\oplus b$, and definitions of $\operatorname{ZERO}$ and $\operatorname{ONE}$, this way: $$\varphi\equiv\forall x\forall y\forall z\Bigg(z=g(x,y)\leftrightarrow\\ \big(\operatorname{ZERO}(x)\land\operatorname{ZERO}(y)\land\operatorname{ZERO}(z)\big)\lor\\ \exists u\exists v\Big(x=f(u,u)\land y=f(v,v)\land z=f\big(g(u,v),g(u,v)\big)\Big)\lor\\ \exists u\exists v\exists w\Big(\operatorname{ONE}(w)\land x=f\big(f(u,u),w\big)\land y=f\big(f(v,v),w\big)\land z=f\big(g(u,v),g(u,v)\big)\Big)\lor\\ \exists u\exists v\exists w\Big(\operatorname{ONE}(w)\land x=f\big(f(u,u),w\big)\land y=f(v,v)\land z=f\big(f(g(u,v),g(u,v)\big),w)\Big)\lor\\ \exists u\exists v\exists w\bigg(\operatorname{ONE}(w)\land x=f(u,u)\land y=f\big(f(v,v),w\big)\land z=f\Big(f\big(g(u,v),g(u,v)\big),w\Big)\bigg)\Bigg)$$ which is interpreted this way in a "nice" model" $$\forall x\forall y\forall z\Big(z=g(x,y)\leftrightarrow\\ (x=0\land y=0\land z=0)\lor\\ \exists u\exists v\big(x=2u\land y=2v\land z=2g(u,v)\big)\lor\\ \exists u\exists v\big(x=2u+1\land y=2v+1\land z=2g(u,v)\big)\lor\\ \exists u\exists v\big(x=2u+1\land y=2v\land z=2g(u,v)+1\big)\lor\\ \exists u\exists v\big(x=2u\land y=2v+1\land z=2g(u,v)+1\big)\Big)$$

$$$$ EDIT: In fact you can omit the base case from your inductive definition of XOR since: $$0\oplus0=(2\cdot0)\oplus(2\cdot0)=2(0\oplus0)\\ \therefore\:0\oplus0=0$$ Hence $\varphi$ can be simplified by omiting the "$\operatorname{ZERO}(x)\land\operatorname{ZERO}(y)\land\operatorname{ZERO}(z)$" part.

Answer 2

This isn't exactly the answer to the question you ask, but I hope it can be used to answer your question.

I will show that there is no formula $\phi(x,y,z)$ in language including $S$ (successor)$,+,0$ (i.e. the language of Presburger arithmetic) which is equivalent to $x\oplus y=z$.

Suppose such formula exists. There is a standard result (which you can see here) is that the only subsets of $\Bbb N$ definable using Presburger arithmetic are the eventually periodic sets. But using $\phi$ we can define set of numbers of the form $n\oplus (n+1)$. But it's easy to see (I leave it as an exercise) that these numbers are precisely numbers which are one less than a power of $2$, so they don't form an eventually periodic set. This is a contradiction.