Let
$$U \colon C \to \operatorname{Set}$$
be a
concrete functor,
ie. a faithful one.
Someone might wonder when such a functor is
conservative,
ie. reflects isomorphisms.
There are known cases when this is true, for example when this is an algebraic functor (or more generally a monadic functor).
Trying to level up from this case (but still keep cool), let us consider a first order language $L$ (over classical logic), a theory $T$ over $L$ and the forgetful functor $$U \colon \operatorname{Mod}_L(T) \to \operatorname{Set}.$$
If the language $L$ does not contain relation symbols (and even if the theory is not equational) the forgetful functor is conservative:
let $f \colon M \to N$ be a bijective morphism of models of $T$ and let $g$ be the inverse function, then for every $n$-ary function symbol $\varphi$ we have that $$ \begin{align} g(\varphi(y_1, \ldots, y_n)) &= g(\varphi(f(g(y_1), \ldots, f(g(y_n)) \\ &= g(f(\varphi(g(y_1), \ldots, g(y_n)))) \\ &= \varphi(g(y_1), \ldots, g(y_n)) \end{align} $$ which shows that $g$ is indeed a morphism.
It is also easy to see that the forgetful functor is not necessarely conservative.
For example, let $L$ consists of one $n$-ary relation symbol $R$ and let $T$ be the empty theory. If $X = Y$ is a non-empty set and the interpretation of $R$ is respectively $R_X = \emptyset$ and $R_Y = Y^n$ then the identity $$id \colon (X, R_X) \to (Y, R_Y)$$ is a bijective morphism whose inverse function is not a morphism.
If we consider linear (= total) orders then the forgetful functor is conservative, as we could prove by hand. This would essentially use the fact that $$ \tag{1} \neg(x < y) \quad \text{if and only if} \quad x = y \text{ or } y < x. $$
Someone else might suggest that linear orders can be expressed in the language of lattices (with some additional axioms) and so reduce to the previous analysis. This would raise questions.
Formula (1) also suggest to consider preservation theorems from model theory (which regrettably I'm not too familiar with).
Theorem (whose name goes here?)
Let $\varphi(x_1, \ldots, x_n)$ be a formula in the language $L$.
Then the following are equivalent:
(a) $\varphi$ is equivalent to a positive quantifier-free
formula in $L$ modulo $T$;
(b) every morphism $f \colon M \to N$ of models of $T$
preserves $\varphi$.
The implication (a) $\Rightarrow$ (b) is trivial, as morphisms between structures preserve positive quantifier-free formulas. I do not know the proof of the other implication.
Yet, note that the inverse function $g$ of a bijective morphism $f \colon M \to N$ is a morphism if and only if for every $n$-ary relation symbol $R$ and every $n$-uple $x_1, \ldots, x_n \in M$ $$ M \models R(x_1, \ldots, x_n) \quad\Leftarrow\quad N \models R(f(x_1), \ldots, f(x_n)) $$ which is equivalent to say that $$ M \models \neg R(x_1, \ldots, x_n) \quad\Rightarrow\quad N \models \neg R(f(x_1), \ldots, f(x_n)). $$
So, consider the weaker statement
(b') every bijective morphism $f \colon M \to N$ preserves $\varphi$.
Clearly (a) implies (b'), and so by formula (1) the forgetful functor from the category of linear orders is conservative.
The question of interest is the following.
Is it true that the forgetful functor $$U \colon \operatorname{Mod}_L(T) \to \operatorname{Set}$$ is conservative (if and) only if for every $n$-ary relation $R$ in $L$ the formula $\neg R(x_1, \ldots, x_n)$ is equivalent modulo $T$ to some positive quantifier-free formula?
Any comment is welcome. The main quest is to understand when a concrete functor is conservative.
First of all, let me correct your statement of the theorem.
Theorem 1: Let $\varphi$ be a formula and $T$ a theory. The following are equivalent:
$\varphi$ is preserved by all homomorphisms between models of $T$.
$\varphi$ is $T$-equivalent to a positive existential formula.
Here a positive extential formula is one built from the atomic formulas by $\land$, $\lor$, and $\exists$.
Another classic model-theoretic preservation theorem extends this to surjective homomorphisms (see Theorem 3.2.4 in Model Theory by Chang and Keisler, and note that by "preserved under homomorphisms" they mean "preserved by surjective homomorphisms").
Theorem 2: Let $\varphi$ be a formula and $T$ a theory. The following are equivalent:
Here a positive formula is one built from the atomic formulas by $\land$, $\lor$, $\exists$, and $\forall$.
Note that an injective map additionally preserves the truth of the negated atomic formula $x\neq y$. By extending the language with a new binary relation symbol $\neq$ and extending the theory $T$ with a new axiom $\forall x \, \forall y\, (\lnot (x = y) \leftrightarrow (x\neq y))$, we don't change the models of $T$, but we restrict to considering only injective homomorphisms. And we can apply the theorem above to obtain the following.
Theorem 3: Let $\varphi$ be a formula and $T$ a theory. The following are equivalent:
Where a $\neq^+$ formula is one buit from the atomic formulas and instances of $\neq$ by $\land$, $\lor$, $\exists$, and $\forall$.
As explained in your question, it follows from Theorem 3 that for any theory $T$, the forgetful functor to the category of sets reflects isomorphisms if and only if for every $n$-ary relation symbol $R$ in the language, the formula $\lnot R(x_1,\dots,x_n)$ is equivalent to a $\neq^+$ formula.
Here's a sketch of a direct proof of Theorem 3.
The direction $2\rightarrow 1$ is an easy induction the structure of $\varphi$. Injective homomorphisms preserve the truth of all atomic formulas and instances of $\neq$. The inductive steps for $\land$ and $\lor$ and $\exists$ are easy (and apply to all homomorphisms). The inductive step for $\forall$ uses surjectivity.
For the direction $1\rightarrow 2$, it suffices (by a standard compactness argument) to show that for every complete type $p$ with $\varphi\in p$ and every complete type $q$ with $\varphi\notin q$, there exists a $\neq^+$ formula $\psi$ with $\psi\in p$ and $\psi\notin q$.
So suppose for contradiction that we have complete types $p$ and $q$ with $\varphi\in p$ and $\varphi\notin q$, but such that every $\neq^+$ formula in $p$ is also in $q$. Let $a$ be a realization of $p$ in a model $M_0\models T$, and let $b$ be a realization of $q$ in a model $N_0\models T$.
By a compactness argument, we obtain an elementary extension $N_0\preceq N_1$ together with a map $f_0\colon M_0\to N_1$ which preserves the truth of all $\neq^+$ formulas, and such that $f_0(a) = b$ (take the union of the $\neq^+$ diagram of $M_0$ and the elementary diagram of $N_0$, identifying $a$ and $b$).
By another compactness argument, we obtain an elementary extension $M_0\preceq M_1$ together with a map $g_1\colon N_1\to M_1$ which reflects the truth of all $\neq^+$ formulas, and such that $g_1\circ f_0$ is the inclusion $M_0\to M_1$ (take union of the elementary diagram of $M_0$ and the negated $\neq^+$ diagram of $N_1$, identifying the elements of $M_0$ with their images in $N_1$ under $f_0$).
Repeating, we obtain elementary chains $M_0\preceq M_1\preceq M_2\preceq\dots$ and $N_0\preceq N_1\preceq N_2\preceq \dots$, and connecting maps $f_i\colon M_i\to N_{i+1}$ preserving all $\neq^+$formulas (and hence an injective homomorphism) and $g_i\colon N_i\to M_i$ reflecting all $\neq^+$ formulas (and hence also injective, but not necessarily a homomorphism), making all triangles commute.
Taking directed colimits (unions of the elementary chains), we obtain $M_0\preceq M_\omega$, $N_0\preceq N_\omega$, and a bijective homomorphism $f_\omega\colon M_\omega\to N_\omega$ (with inverse map $g_\omega\colon N_\omega\to M_\omega$, which is not necessarily a homomorphism). Since $M_0\models \varphi(a)$, $M_\omega\models \varphi(a)$, so $N_\omega\models \varphi(b)$ (since $\varphi$ is preserved by bijective homomorphisms, and $f_\omega(a) = f_0(a) = b$), hence $N_0\models \varphi(b)$, contradicting $\varphi\notin q$.