OK, maybe if we look at some other definitions of equality we can get a grip on it? In set theory, you say that two sets are equal if they’ve got the same elements. How do you know the elements are the same i.e. equal? You just know.
If we have the axiom of foundation—or, more perspicuously maybe, the principle of epsilon-induction its equivalent to in presence of other usual axioms—the picture is less mysterious.
Yes, in order to tell if A and B are equal, we need to see if they have the same elements, but in order to do that we need to already know how to tell if any two elements are the same, and so on, which does not seem to actually get us anywhere.
Except that when A or B has no elements, we don’t need to have already figured out any way to tell two elements apart—if A has no elements but B does, then A and B are not equal, and if both A and B have no elements, its trivially true that all their elements are equal, so A is equal to B, and they are both the unique empty set. Given foundation, all membership chains terminate at the empty set, so we’ve now got a way to use extensionality—the principle that two sets are the same if they have got exactly the same elements—to give us a non-circular notion of equality by grounding in the empty case.
(If we don’t have foundation, or if we indeed actively welcome non-well-founded sets, we do need something beyond extensionality to give a well-defined notion of equality, e.g. bisimulation in case of the anti-foundation-axiom.)
If we have the axiom of foundation—or, more perspicuously maybe, the principle of epsilon-induction its equivalent to in presence of other usual axioms—the picture is less mysterious.
Yes, in order to tell if A and B are equal, we need to see if they have the same elements, but in order to do that we need to already know how to tell if any two elements are the same, and so on, which does not seem to actually get us anywhere.
Except that when A or B has no elements, we don’t need to have already figured out any way to tell two elements apart—if A has no elements but B does, then A and B are not equal, and if both A and B have no elements, its trivially true that all their elements are equal, so A is equal to B, and they are both the unique empty set. Given foundation, all membership chains terminate at the empty set, so we’ve now got a way to use extensionality—the principle that two sets are the same if they have got exactly the same elements—to give us a non-circular notion of equality by grounding in the empty case.
(If we don’t have foundation, or if we indeed actively welcome non-well-founded sets, we do need something beyond extensionality to give a well-defined notion of equality, e.g. bisimulation in case of the anti-foundation-axiom.)