Let $\mathcal L$ be a (fixed) language and let $t$ and $s$ both denote $\mathcal L$-terms.
My question is:
Is $\vDash t=s$ enough to conclude that $t$ and $s$ are notations for the same term?
Contrapositively in words: if two terms are distinct then is it always possible to find an interpretation (i.e. structure plus assignment) that confirms this fact?
I suspect this is the case but did not meet this (yet) in my efforts to get more familiarity with logics.
Thank you in advance.
Yes, this is true - and this is one of those things which can seem more mysterious than it actually is if we think too hard about it.
Specifically, let $\mathcal{A}$ be any structure in which each function symbol is interpreted as an injective function and different function symbols' interpretations have disjoint ranges, and let $\nu$ be any variable assignment giving distinct variables different values. By induction on complexity of $s$ and $t$, we get $s^{\mathcal{A},\nu}\not=t^{\mathcal{A},\nu}$.
HINT: thinking of $s$ and $t$ as labelled trees growing downwards - e.g. "$f(g(x), y)$" has a top node labelled "$f$" which has two children labelled "$g$" and "$y$," the latter of which is terminal and the former of which has a child labelled "$x$" which is then terminal - look at the "highest" point of difference between them. For instance, if the outermost function symbols are different then disjoint ranges condition on $\mathcal{A}$ automatically gives the desired result.