Is $s=t$ always strictly stronger than $s+s=t+t$?

Question

This question was inspired by a comment on one of my previous questions. As before, let our signature be that of a single binary operation $+$. Suppose $s$ and $t$ are two distinct terms in this signature. Then, is it always the case that the equational identity $s=t$ is strictly stronger than $s+s=t+t$, meaning $s=t$ implies $s+s=t+t$ but not conversely? Note, the terms $s$ and $t$ should be distinct, for certainly $s=s$ is equivalent to $s+s=s+s$. Obviously, $s=t$ implies $s+s=t+t$. So, the real question is, how to prove that $s+s=t+t$ does not imply $s=t$ for distinct terms $s$ and $t$? Or, if my conjecture is false, can someone exhibit two distinct terms $s$ and $t$ such that $s=t$ is equivalent to $s+s=t+t$?

Answer 1

NOTE: I'm not 100% confident in the following answer. If you spot an error, let me know and I'll try to patch it up. At the very least, though, I hope this will give you some ideas. ;-)

If your signature consists of only a single binary operation $+$, then yes, $s=t$ is always strictly stronger than $s+s=t+t$ for distinct terms $s,t$.

For the sake of contradiction, suppose that $s+s=t+t$ implies $s=t$ for some two distinct terms $s\neq t$ over your signature.

Let $\langle A,\star\rangle$ be the free magma on $\mathbb N=\{0,1,\cdots\}$ so that its elements are in bijective correspondence with the terms over your signature. More specifically, there exists bijective $f:\mathtt{TERM}\to A$ such that $$f(x_i)=i$$ and $$f(s+t) = f(s)\star f(t)$$ for all terms $s,t$. Let us define now an equivalence relation $\sim$ on $A$ by letting $a\sim b$ if and only if $a=b$ or $f^{-1}(a)$ and $f^{-1}(b)$ contain either $s$ or $t$ as a proper subterm. That is, we are "collapsing" all of the elements of the free algebra containing a proper subterm of shape either $s$ or $t$ (or both) into a single equivalence class $\kappa$.

We can show that $\sim$ respects the magma structure, that is, that $f(u)\sim f(u')$ and $f(v)\sim f(v')$ together imply $f(u)\star f(v) \sim f(u')\star f(v')$. (Exercise?) Hence, we can form the quotient magma $\langle A',\star'\rangle$ of $\langle A,\star\rangle$ by the equivalence relation $\sim$. In this quotient magma, $s+s=t+t$ does not imply $s=t$, so this will serve as our counterexample. In particular, if $s$ and $t$ depends on the variables $x_0,\cdots, x_n$, so that $s=s(x_0,\cdots,x_n)$ and $t=t(x_0,\cdots,x_n)$, then we have that $$(s+s)([0],\cdots,[n]) = (t+t)([0],\cdots,[n])$$ evaluated in $\langle A',\star'\rangle$, as both are equal to the single equivalence class \kappa. (This is because both $s+s$ and $t+t$ have proper subterms of shape $s$ or $t$.) On the other hand, we have $$s([0],\cdots,[n]) \neq t([0],\cdots,[n])$$ which can be seen via casework. The left hand side equals either $[f(s)]$ or $\kappa$, and the right hand side equals either $[f(t)]$ or $\kappa$. Furthermore, they cannot both equal $\kappa$, as this would imply that each of $s,t$ is a subterm of the other. Hence, they are unequal and we have completed our counterexample!