Thinking about Equality Philosophically

03-27-2021 | math, philosophy

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?