is a Kleene equality means that it asserts that if either side of the equality is defined, then so is the other, and they are equal. Sometimes another symbol is used for Kleene equality, such as
For example, in elementary algebra (or more generally, the first-order theory of a field),
is always true as Kleene equality, even when , because then both sides are undefined. In contrast,
is not always true, even though the two sides are equal whenever both are defined, because the right-hand side is defined when but the left-hand side is not.
The example (2) can be fixed in either of two ways. First, we can make its statement contingent on some condition under which the equality holds, as follows:
This states that (2) holds whenever , which is correct. Alternatively, we can add a clause to the term on the right-hand side that forces it to be undefined when , as follows:
The idea here is that is a term (like a piecewise-defined? expression with only one piece) that is defined only when . Note that (4) is a stronger statement than (3); while (3) states only that (2) holds when , (4) states additionally that the left-hand side of (2) is defined only when .
The version usually seen in elementary algebra textbooks,
In general, if is a context and is a type, then the set of terms of type with free variables given by can be thought of as something like the set of sections of a product projection . Aside from the fact that we only get definable operations this way, we also get a finer notion of equality, as several distinct terms may denote equal operations. However, that is where the proposition ‘’ comes in; it states that the terms and denote equal operations.
If we now allow for terms for undefined expressions, then we get sections of the projection (where is the set of subsingletons of ). Then Kleene equality denotes equality of these operations.