Find a closed formula

Question

I have a language $L=\{f,g\}$ (with "=")

$f$ and $g$ are functional symbols. I will call implementation $M$ of $L$ "nice", if it satisfies the next conditions:

1) Carrier is $N={0,1,2..}$

2) $f$ - addition operation

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

$M \models \varphi$ iff $g$ is being implemented as multiplication.

I mean $g_M(a,b)=a \cdot b$ for each $a,b \in N$

Thanks for any advice

Answer 1

Define the predicate $$0(x):(\forall y)(f(x,y)=y).$$ Define the relations $$x<y:(\exists z)(\lnot 0(z)\land f(x,z)=y)$$ and $$S(x,y):(x<y)\land(\forall z)(x<z\to y<z\lor y=z).$$ You can check that $0(x)$ is only satisfied by $0$, that $<$ coincides with the order of the natural numbers and that $S(x,y)$ says that $y=x+1$.

Now define the formula:

$$(\forall x,y)((0(y)\to g(x,y)=y)\land(\lnot 0(y)\to(\forall z)(S(z,y)\to g(x,y)=f(g(x,z),x))))$$

I think this formula guarantees that $g$ is the multiplication (but maybe there's a faster way).