nLab
equality

Context

Equality and Equivalence

Foundations

Contents

Idea

There is a lot of interesting stuff to be said about equality in logic, higher category theory, and the foundations of mathematics, but it hasn't all been said here yet.

Different kinds of equality

Here is a list of distinctions between different notions of equality, in different contexts, where possibly all the following pairs of notions are, in turn, “the same”, just expressed in terms of different terminologies:

  • the difference between axiomatic and defined equality;
  • the difference between identity and equality,
  • the difference between intensional and extensional equality,
  • the difference between equality judgements and equality propositions,
  • the difference between equality and isomorphism,
  • the difference between equality and equivalence,
  • the possibility of operations that might not preserve equality.

In type theory

In a formal language such as type theory, one distinguishes various different notions of equality or equivalence of the terms of the language.

Note that both intensional and extensional type theories may distinguish between intensional and extensional equality (and whether the type theory satisfies function extensionality is yet a separate issue).

Definitional equality

The most basic one is definitional equality or intensional equality.

According to PML (1980), p. 31:

Definitional equality is intensional equality, or equality of meaning (synonymy). [] It is a relation between linguistic expressions [] Definitional equality is the equivalence relation generated by abbreviatory definitions, changes of bound variables and the principle of substituting equals for equals. [] Definitional equality can be used to rewrite expressions [].

on p. 60:

… intensional (sameness of meaning) …

For instance the symbols “22” and “s(s(0))s(s(0))” (meaning the successor of the successor of 00) are definitionally/intensionally equal terms (of type the natural numbers): the first is merely an abbreviation for the second.

Computational equality

Another sort of equality which is very important in type theory is computational, conversional, or reductional equality. This is the congruence on terms generated by various conversion or reduction rules, such as β-reduction or η-conversion (the choice of rules depends on the type theory).

The paradigmatic example of computational equality is a pair of terms like “(λx.x+x)2(\lambda x. x+x)2” and “2+22+2”, where the second is obtained by β\beta-reduction from the first. In a type theory that includes definitions by recursion, expansion of a recursor is also computational equality. For instance, if addition is defined by recursion, then “2+22+2” (that is, s(s(0))+s(s(0))s(s(0))+s(s(0))) reduces via this rule to “44” (that is, s(s(s(s(0))))s(s(s(s(0))))).

For better or for worse, however, it is common in type theory to use the phrase “definitional equality” to include computational equality, even though it involves more than mere expansion of definitional abbreviations. There is even a phrase “δ\delta-reduction” for the substitution of definitions regarded as a conversion rule analogous to β\beta-reduction and η\eta-expansion. Thus, even though “2+22+2” and “44” are not literally equal by definition but only by performing some computation (even if the computation is fairly trivial in this case), the type of equality they do enjoy is generally called definitional.

Perhaps this is because in type theory, computational equality plays the same role as true definitional equality. In particular, typing judgments respect it: if Γ(t:A)\Gamma \vdash (t:A), while tt and AA are computationally equal to tt' and AA', then also Γ(t:A)\Gamma \vdash (t':A'). For tt and tt', this fact is sometimes called type preservation? and is an important provable aspect of a type theory. For AA and AA', the statement is generally only contentful in a dependent type theory, in which case it is often included explicitly as one of the typing rules.

Another apt word for computational equality is judgmental equality, since it is often expressed in type theory by a separate judgment: in addition to typing judgments Γ(t:A)\Gamma \vdash (t:A), we have equality judgments Γ(t=t):A\Gamma \vdash (t = t'): A. The rules for manipulating such judgments then include reflexivity, symmetry, transitivity, and the generating computations such as β\beta-reduction.

Propositional equality

By contrast with “2+22+2” and “44”, it is pretty much impossible to write down rules of computational equality such that the symbols “a+ba + b” and “b+ab + a” (in a context with free variables aa and bb for, say, natural numbers) become equal. They are (only) extensionally equal, in the sense that they become computationally equal when any particular natural numbers (such as s(s(0))s(s(0)) and s(s(s(0)))s(s(s(0))), say) are substituted for aa and bb. An actual proof is necessary to demonstrate this equality in general: it is not a definition but a theorem that a+b=b+aa + b = b + a for all natural numbers a,ba, b. With addition defined recursively on (say) its first argument, this theorem must be proven by induction on aa and is surprisingly nontrivial to formalize.

In type theory, this extensional equality is a judgement, not itself yet a proposition (an item in the formal system itself). It can be internalized, however, into a notion of equality called propositional equality, by introducing identity types (or identity propositions). Thus, Id (2+2,4)Id_{\mathbb{N}}(2+2,4) is the type/proposition that 2+22+2 is propositionally equal to 44, while a,b:Id (a+b,b+a)\prod_{a,b:\mathbb{N}} Id_{\mathbb{N}}(a+b,b+a) is the proposition that addition is commutative. Exhibiting a term belonging to such a type is exhibiting (i.e. proving) such a propositonal equality.

The fact that typing judgments respect computational/judgmental equality means that if two terms tt, tt' are computationally/judgmentally equal, then they are also propositionally equal. This is because the type Id(t,t)Id(t,t) is always inhabited by the reflexivity term refl trefl_t, but then this term refl trefl_t also inhabits the type Id(t,t)Id(t,t').

The converse, however, is not true in general. It is possible to add a rule to type theory saying that “if Id(t,t)Id(t,t') is inhabited, then t=tt=t' judgmentally”. (In this case, the adjectives “computational” and “definitional” sometimes used for judgmental equality truly lose their applicability.) This is a very strong way to make the type theory extensional type theory, but is often eschewed by type theorists (even those who don’t care about homotopy type theory) because it makes type checking undecidable — because type checking has to respect judgmental equality, such a rule means that it also has to respect propositional equality, which in turn means that it has to be able to evaluate arbitrary functions defined inside of type theory.

In set theory

Every set SS has an equality relation, a binary relation according to which two elements xx and yy of SS are related if and only if they are equal; in this case we write x=yx = y. This is the smallest reflexive relation on SS, and it is in fact an equivalence relation; it is the only equivalence relation on SS that is also a partial order (although that fact is somewhat circular). This relation is often called the identity relation on SS, either because ‘identity’ can mean ‘equality’ or because it is the identity for composition of relations.

As a subset of S×SS \times S, the equality relation is often called the diagonal and written Δ S\Delta_S or similarly. As an abstract set, this subset is isomorphic to SS itself, so one also sees the diagonal as a map, the diagonal function SΔ SS×SS \overset{\Delta_S}\to S \times S, which maps xx to (x,x)(x,x); note that x=xx = x. This is in Set; analogous diagonal morphisms exist in any cartesian monoidal category.

In an axiomatic set theory? such as ZFC or ETCS, the presence of the equality relation is part of the axiomatization, although this is usually swept under the rug by including an equality relation by default in all first-order theories. (It has to be made more explicit in a structural set theory such as SEAR, where there is no equality relation on sets themselves, only on elements of a particular set.)

By contrast, in a definitional set theory?, an equality relation is structure which has to be put onto a type or preset in order to obtain a set. See for example setoid.

References

In

equality is the subject of volume 1, book 2 “Die Lehre vom Wesen” (The doctrine of essence). As discussed at Science of Logic, one can roughly identify in Hegel’s text there the notion of intensional identity and of the reflector term in identity types.

Texts on type theory typically deal with the subtleties of the notion of equality. For instance

Besides

which might be the first paper to mention intensional equality (and the fact that it should be decidable), another reference is

Dick de Bruijn?, Automath,

which makes a distinction between definitional equality and “book” equality.

Revised on May 31, 2014 07:57:32 by Urs Schreiber (89.204.135.200)