Notions of Weak, Existential, Strong, and Evans Equality

Weak Equality,
Existential Equality,
Strong Equality,
Evans Equality
are special relations that differ from the usual
Primitive Equality
when terms may be undefined in the sense that they do not denote a proper object.
When we write def(t) for the definedness of t, we can define them the following way:
(t=t') or not def(t) or not def(t')
(t=t') and def(t) and def(t')
weak(t,t') and (def(t) iff def(t'))
strong(t,t') or not def (t'') for some proper subterm t'' of t or t'
The first three notions are standard, cf. e.g. Peter BURMEISTER: A Model Theoretic Oriented Approach to Partial Algebras. Akademie-Verlag, Berlin, 1986, Section 8.1. There, also the name "Evans equality" seems to appear for the first time. It refers to the following papers:
Trevor EVANS: The Word Problem for Abstract Algebras. J. of the London Math. Soc. 26 (1951), pp. 64--71.
Trevor EVANS: Embeddability and the word problem. J. of the London Math. Soc. 28 (1953), pp. 76--80.
The name "Evans equality" was also used by Harald GANZINGER in his joint paper cited below.

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:

But note that the implication from evans(t,t') to weak(t,t') is only valid in the case of strictness, i.e. when each term with an undefined subterm is undefined. For example, assuming recover(car(nil))=true, def(true), def(false), and not def(car(nil)), we have evans(recover(car(nil)),false) but not weak(recover(car(nil)),false).

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,
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:

This means that cons(car(x),cdr(x))=x gets truth value 1/2 for a free delta- variable x, because universal quantification is minimum, as standard. For free delta-, delta+, and gamma variables according to Smullyan's classification, cf. Claus-Peter WIRTH: Descente Infinie + Deduction. Logic Journal of the IGPL, Vol. 12(1), pp. 1--96, January 2004.
Acknowledgements: I am indebted to Viorica SOFRONIE for some help and I would like to thank Uwe WALDMANN and Klaus Becker for some short discussions &c.
This is file p/eq1.html on Claus-Peter Wirth's web site.
Last modified 2004/10/17/17.40