By logic without equality I mean those kind of logics where equality is treated as a binary relation satisfying some axioms, as opposed to a logics where equality is a logical symbol satisfying some inference rules.
In my understanding there should be no difference at the syntactic level between logics with or without equality since the syntax should not be able to distinguish a logic-primitive predicate or any other predicate (but in case I am wrong please correct me).
So I am wondering what are the differences at a semantic level between these kind of logics.
In particular I am wondering whether all the definitions and theorems of classical model theory can be transported verbatim to the without-equality logics.
If it is possible I would also appreciate references that treat the subject.
Addendum: After Andrej Bauer's answer I realize it would be better to add some specification.
I am interested basically in logical theories where every theory comes equipped with an axiom-schema for substitution, that is a family of axioms of the form
$$\forall x,y. (x=y) \land \varphi(x) \rightarrow \varphi(y)$$
where $\varphi$ is a formula of the language.
In short I am curious to know what changes we get if we change the semantics of the symbol of equality.
Addendum 2: also it seems from the answer provided so far that the model theory should remain unchanged but it does not look like it to me.
First of all while quotienting for the equivalence relation should provide a (elementary?) equivalent model it does not (necessarily) preserves the homomorphisms: consider a set with an equivalence relation that identifies all elements, the corresponding quotient structure should be the terminal model (in the sense of category theory) but the first model clearly does not have to be a terminal object in the category.
Also it seems to me that one could lose the characterisation of homomorphisms as mapping that preserve atomic formulas, since, if we drop the requirement of interpreting the equality symbol as the identity relation, then we could have mappings that preserve atomic formulas but for some operations symbols do not respect the external equality: i.e. we could have a mapping $f \colon A \to B$ and an operation symbol $o$ such that $$B \models f(o^A(a)) = o^B(f(a))$$
but $f(o^A(a))$ and $o^B(f(a))$ are not identical.
It seems rather difficult to find references that deal with this kind of phenomena, that is why I would really appreciate if someone could provide some pointers.
Thanks in advance.
Best Answer
Yes, logic with equality treats equality in a special way because it relates equality to substitution. That is, we have the substutition rule (to be read as a schema, of course) $$\frac{\vdash \phi[s/x] \qquad \vdash s = t}{\vdash \phi[t/x]}$$ which expresses the fact that $\phi[s/x]$ entails $\phi[t/x]$ when $s = t$, for any formula $\phi$. In other words, we may always replace a term with an equal one. This together with reflexivity is enough to get all of the rules of equality. For instance, to get symmetry, take $\phi$ to be the formula $x = s$.
If equality is not treated in a special way, then we may still express the fact that it is an equivalence relation, but the substution rule is not directly expressible. We might try to simulate the substitution rule by further axioms stating that all function symbols and relations respect equality, but at that point we might as well admit we've just axiomatized the substitution rule by hand.
The difference carries over to model theory. Suppose we have a model $M$ in which equality is interpreted by some relation $E \subseteq M \times M$. It follows that $E$ is an equivalence relation. In order for $M$ to validate the substitution rule, the interpretations of all other functions and relation symbols must be congruences with respect to $E$. Consequently, we may quotient the model by $E$ to obtain another model $M/E$ in which equality is equality. The upshot of this is that nothing much is gained by the extra generality of taking equality to be a general relation $E$.