Note that weak(t,t') and exist(t,t') are trivially true and false, resp., if one of the terms t, t' is undefined. Therefore, the use of primitive equality in the definitions of weak and existential equality is unproblematic because the definientia do not depend on the behavior of primitive equality on undefined objects.
Strong equality is the standard in theories of sets and classes without urelements: There, function application f(x) is typically defined as the intersection over all y with (x,y) element of f, and the universal class of all sets is taken as a single error element.
Note that def(t) is logically equivalent to exist(t,t). In two-valued logics, there is, however, no general way to express definedness directly with primitive, weak, strong, or Evans equality alone.
From logically strongest to weakest we get:
Moreover, the inclusion of t=t' in the above list
only makes sense when we have some means to model
the undefined objects, as e.g. in
Ulrich KÜHLER,
Claus-Peter WIRTH:
Conditional Equational Specifications of Data Types with
Partial Operations for Inductive Theorem Proving.
RTA-97, LNCS 1232, 1997, pp.38-52,
http://www.ags.uni-sb.de/~cp/p/rta97/welcome.html.
There you also can see how to overcome the traditional strictness restrictions
that do not allow you to write error recovery functions
such as the above "recover".
It is folklore that weak equality is often useless in practice because it is too weak. Similarly, existential equality is mostly too strong, but cf. the references Scott (1979) and Burmeister (1986) in Harald GANZINGER: Relating Semantic and Proof-Theoretic Concepts for Polynomial Time Decidability of Uniform Word Problems.
Note that the negation of existential equality plays the role of a weak unequality: Indeed, not exist(t,t') is logically equivalent to not (t=t') or not def(t) or not def(t').
Evans equality suffers from being an essentially syntactical notion, i.e. depending on the syntax besides semantics: The word "subterm" appears in its definition and if you assume if(true,X,Y) = X you get evans(if(true,true,undefined),false) but not evans(true,false). In practice of logic, syntactical notions tend to be useful only as internal notions not visible at outer interfaces.
Moreover, as we have weak(false,false), the above Evans equality of recover(car(nil)) and false cannot be used for rewriting as otherwise false = weak(recover(car(nil)),false) = weak(false,false) = true.
Thus, Evans equality and weak equality suffer from the fact that
they make rewriting difficult or expensive:
Unless we strongly restrict rewriting by syntactical criteria,
each rewrite step can be done only
after a costly definedness proof.
Nevertheless, Evans equality is well-suited for embedding, completion and
modularity tasks, cf.
Harald GANZINGER, Viorica SOFRONIE-STOKKERMANNS, Uwe WALDMANN:
Modular Proof Systems for Partial Functions with Weak Equality.
This approach uses two objects for the undefined (undefined, irrelevant)
and three truth values (0, 1/2, 1), where validity means not to be zero.
"irrelevant" means that there is a proper subterm which is undefined.
An equation gets truth value "1/2" iff
one of the sides is irrelevant
or
both sides are undefined.
For example, cons(car(nil),cdr(nil))=nil evaluates as follows in the obviously intended standard model: