nLab equality

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 first notion 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 “$2$” and “$s(s(0))$” (meaning the successor of the successor of $0$) are definitionally/intensionally equal terms (of type the natural numbers): the first is merely an abbreviation for the second.

The notion of definitional equality was introduced first in AUTOMATH. The following paper presents a suggestive explanation of this notion and how proof-checking was designed in this system (especially section 10):

On the roles of types in mathematics

The notion of definitional equality was later introduced by Per Martin-Löf, first in the context of normalization proofs for higher-order logic in the paper Hauptsatz for Intuitionistic Simple Type Theory and generalized in Type Theory. He discusses this notion in the paper About Models for Intuitionistic Type Theory and The notion of Definitional Equality.

The extension from AUTOMATH is that one adds the notion of data type (natural number), of constructors (zero and successor) and primitive recursion as definitional equality. The motivation is that one can consider the schema of primitive recursion as a definition of a function.

This was also influenced by natural deduction, where constructors correspond to introduction rules and the work of Gödel on system T.

With this extension, one obtains a programming language with dependent types and where computations correspond to unfolding of definitions (that can be primitive recursive definitions). This programming language has the feature that all computations terminate. This has been also considered in functional programming, see e.g. the discussion in this paper.

A description of the evaluation algorithm using techniques from functional programming can be found in this work of Gregoire and Leroy.

However, not all type theories have definitional equality; objective type theory is a framework of type theories without definitional equality.

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 “$(\lambda x. x+x)2$” and “$2+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+2$” (that is, $s(s(0))+s(s(0))$) reduces via this rule to “$4$” (that is, $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+2$” and “$4$” 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 $\Gamma \vdash (t:A)$, while $t$ and $A$ are computationally equal to $t'$ and $A'$, then also $\Gamma \vdash (t':A')$. For $t$ and $t'$, this fact is sometimes called type preservation and is an important provable aspect of a type theory. For $A$ and $A'$, 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 $\Gamma \vdash (t:A)$, we have equality judgments $\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+2$” and “$4$”, it is pretty much impossible to write down rules of computational equality such that the symbols “$a + b$” and “$b + a$” (in a context with free variables $a$ and $b$ 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))$ and $s(s(s(0)))$, say) are substituted for $a$ and $b$. An actual proof is necessary to demonstrate this equality in general: it is not a definition but a theorem that $a + b = b + a$ for all natural numbers $a, b$. With addition defined recursively on (say) its first argument, this theorem must be proven by induction on $a$ 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_{\mathbb{N}}(2+2,4)$ is the type/proposition that $2+2$ is propositionally equal to $4$, while $\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 $t$, $t'$ are computationally/judgmentally equal, then they are also propositionally equal. This is because the type $Id(t,t)$ is always inhabited by the reflexivity term $refl_t$, but then this term $refl_t$ also inhabits the type $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')$ is inhabited, then $t=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 $S$ has an equality relation, a binary relation according to which two elements $x$ and $y$ of $S$ are related if and only if they are equal; in this case we write $x = y$. This is the smallest reflexive relation on $S$, and it is in fact an equivalence relation; it is the only equivalence relation on $S$ that is also a partial order (although that fact is somewhat circular). This relation is often called the identity relation on $S$, either because ‘identity’ can mean ‘equality’ or because it is the identity for composition of relations.

In the category of reflexive relations on $S$, the equality relation on $S$ is an initial reflexive relation; when the equality relation is a type family instead of a family of propositions, then the equality relation is the initial type generated by reflexivity or the first law of thought.

As a subset of $S \times S$, the equality relation is often called the diagonal and written $\Delta_S$ or similarly. As an abstract set, this subset is isomorphic to $S$ itself, so one also sees the diagonal as a map, the diagonal function $S \overset{\Delta_S}\to S \times S$, which maps $x$ to $(x,x)$; note that $x = 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.

Related concepts

• equality, equation

• identity type,

• identity of indiscernibles

• inequality

  • denial inequality

  • apartness relation

• isomorphism

• equivalence

• weak equivalence

• homotopy equivalence, weak homotopy equivalence

• equivalence in an (∞,1)-category

• equivalence of (∞,1)-categories

basic symbols used in logic

$\phantom{A}$symbol$\phantom{A}$	$\phantom{A}$meaning$\phantom{A}$
$\phantom{A}$$\in$	$\phantom{A}$element relation
$\phantom{A}$$\,:$	$\phantom{A}$typing relation
$\phantom{A}$$=$	$\phantom{A}$equality
$\phantom{A}$$\vdash$$\phantom{A}$	$\phantom{A}$entailment / sequent$\phantom{A}$
$\phantom{A}$$\top$$\phantom{A}$	$\phantom{A}$true / top$\phantom{A}$
$\phantom{A}$$\bot$$\phantom{A}$	$\phantom{A}$false / bottom$\phantom{A}$
$\phantom{A}$$\Rightarrow$	$\phantom{A}$implication
$\phantom{A}$$\Leftrightarrow$	$\phantom{A}$logical equivalence
$\phantom{A}$$\not$	$\phantom{A}$negation
$\phantom{A}$$\neq$	$\phantom{A}$negation of equality / apartness$\phantom{A}$
$\phantom{A}$$\notin$	$\phantom{A}$negation of element relation $\phantom{A}$
$\phantom{A}$$\not \not$	$\phantom{A}$negation of negation$\phantom{A}$
$\phantom{A}$$\exists$	$\phantom{A}$existential quantification$\phantom{A}$
$\phantom{A}$$\forall$	$\phantom{A}$universal quantification$\phantom{A}$
$\phantom{A}$$\wedge$	$\phantom{A}$logical conjunction
$\phantom{A}$$\vee$	$\phantom{A}$logical disjunction
$\phantom{A}$$\otimes$$\phantom{A}$	$\phantom{A}$multiplicative conjunction$\phantom{A}$
$\phantom{A}$$\oplus$$\phantom{A}$	$\phantom{A}$multiplicative disjunction$\phantom{A}$

References

In

• Georg Hegel, Science of Logic, 1812

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

• Per Martin-Löf, Intuitionistic type theory, Lecture notes (1980)

Besides

• Kurt Gödel, Über eine bisher noch nicht benützte Erweiterung des finiten Standpunktes. Dialectica (1958), pp. 280–287,

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

• Nicolaas de Bruijn, Automath,

where de Bruijn makes a distinction between definitional equality and “book” equality.