I've been getting into formalizing math in computer proof assistants, and it made be realize equality was much more subtle than I had previously thought. Consi

I've been getting into formalizing math in computer proof assistants, and it made be realize equality was much more subtle than I had previously thought. Consider the sets {1, 2}, {2, 1}, {1, 2, 2}, and {n in Z | 1 <= n < 3}. These are not literally the same (since they're written differently; they're "intensionally" different), however, in math, sets are considered to be equal if they have the same elements (they're "extensionally" equivalent). These sets do happen to have the same elements (1 and 2) so they're all equal to each other. But you have to go through some process to construct an equality between pairs of sets to actually see this. It's like how in many programming languages there are multiple kinds of equality. The most basic is that the variables refer to the same object in memory (i.e., a pointer comparison), which is hardly a computation at all. Others are more involved, like how in Python the `==` operator recursively checks for element-wise equality in data structures like lists, dictionaries, sets, and tuples. There is a concrete computation that demonstrates whether things are equal. In math, there is no algorithm that can, in general, determine whether on not two things are actually equal. Given two objects, you might be able to come up with some ad hoc method to tell they're equal (which is a sort of computation -- proofs are programs). Math depends on a belief that these ad hoc equality proofs won't ever mutually contradict one another. Through this belief, we can pretend that there is exactly one Platonic ideal form of each thing somewhere out there in the mathematical universe. (The almost-algorithm for determining equality, which is horribly slow but general, is to enumerate all possible proofs, checking one at a time to see if they prove or disprove the equality. Unfortunately, there are some concretely definable sets, similar to the machine you create for the halting problem, that this equality program will never decide are equal or not -- assuming math is consistent, that is. This is what the first Godel incompleteness theorem is about.)