I’ve a long-running obsession with the meaning of equality, generally as it’s used in type theory, and about the divide between intensional equality and extensional equality. I’ve had discussions about this with real type theorists on IRC, and armchair theorists like myself, and I’m consistently left unsatisfied with the outcome. It seems that everyone has a different way of articulating this difference, and—as I’ve said this before—it’s been hard, at least in my experience, to really land on a common understanding. In this post, I’m going to give some background, then try and articulate my own way of thinking about this, and how I think it’s related to Kant’s ideas about synthetic and analytic utterances.
I. Equality’s Divide
As I alluded to above, a lot of my interest in this topic is anchored in the distinction between intensional equality and extensional equality. The dropping of that anchor is frankly due to the struggle I’ve had myself to grasp this distinction which makes it difficult to make headway when you’re learning about type theory. To start, let’s try and give some meaningful definitions to these two types of equality:
Intensional equality
An intensional equality is one whose definition ships with the theory we’re working within. It’s an equality that is a part of our metatheory.
Let’s, for example, think about working in Agda’s type theory, which
is pretty damn close to vanilla Martin-Löf dependent type theory
with some inconsequential—at least for the topic at
hand—embellishments. In Agda, equality is intensional, and the
metatheory we’re working within when we’re writing Agda is the
language itself. So another way to think about intensionality within
Agda is that equality is syntactic. When we, for instance, prove
something like x + y ≡ y + x in Agda, we’re tasked with showing the
type checker that the normal forms of the left-hand side of \(\equiv\)
is syntactically identical to the right-hand side. The thing to keep
in mind that we don’t have to do, is to illustrate that this is true
for all x’s and y’s by listing them, one by one, doing the two
additions with every possible combination of x and y, and showing
they both have the same results. If we’re using the natural numbers as
the type for x and y, this task would take an infinite span of
time. Instead, we get to use induction to show that, through
reduction, the syntax on the left side is the same as the syntax
on the right side. This is because ≡’s meaning is intrinsic to the
theory of Agda. When we use Agda what we’re using is the syntax of the
language, and that syntax comes with the notion of sameness, rather
simply in that two things are the same if they’re literally the same
normalized string of charactersThis is a bit of an over simplification w/r/t what is
essentially an implementation detail. In practice Agda isn’t literally
comparing strings of characters, but a data structure which can be
shown to a human in Agda’s syntax.
.
Extensional Equality
With an extensional equality, the equality isn’t a part of theory, but instead verifies the sameness of the objects created within the theory. Take for example extensional set theory. The way to determine that sets are equal is by determining that all of their elements are equal. It requires enumerating all the constituent pieces and testing them one by one, also known as “point-wise”.
Synthetic, Analytic, Intensional, Extensional
Western Philosophy’s most famous lover of rules is, far and away, Immanuel Kant.
Kant is the originator of the synthetic and analytic divide. Essentially, an analytic sentence or expression is inherently verifiable, e.g., “all pediatricians are doctors”, while a synthetic expression requires exterior verification, like “all pediatricians are rich”, to verify this statement, we’d have to talk with all pediatricians, while with the former we know it to be true just by the meaning of the words.
This is, I’d argue, very closely related to the notion of intensional vs. extensional equality, if not just a mathematician’s way of saying the same thing that Kant was trying to say. The real question lies, though, in what system would you use to verify this equational theory?