I don't know about category theory, but identity can't be defined in first-order logic, so it is usually added as a primitive logical predicate to first-order logic. Adding infinite axiom schemas of the sort you showed above don't qualify as a definition, which has to be a finite biconditional. But identity is definable in pure second-order logic. Using Leibniz's law, one can define
Intuitively, and are defined identical iff they have all their properties in common. Formally, there is always a subset of the domain in the range of and which for any object contains only . This guarantees that the definition cannot accidentally identify different objects.
For instance, are the symbols "1" = "2" in first order logic? Depends on the axioms!
Yes and that is because in predicate logic, different names (constant symbols) are allowed to refer to the same object or to different objects, while the same names always refer to the same object. This is similar to natural language where on thing can have multiple names. Frege (the guy who came up with modern predicate logic) has written about this in an 1892 paper:
Equality gives rise to challenging questions which are not altogether easy to answer. Is it a relation? A relation between objects, or between names or signs of objects? In my Begriffsschrift I assumed the latter. The reasons which seem to favour this are the following: a = a and a = b are obviously statements of differing cognitive value; a = a holds a priori and, according to Kant, is to be labelled analytic, while statements of the form a = b often contain very valuable extensions of our knowledge and cannot always be established a priori. The discovery that the rising sun is not new every morning, but always the same, was one of the most fertile astronomical discoveries. Even to-day the identification of a small planet or a comet is not always a matter of course. Now if we were to regard equality as a relation between that which the names
a' andb' designate, it would seem that a = b could not differ from a = a (i.e. provided a = b is true). A relation would thereby be expressed of a thing to itself, and indeed one in which each thing stands to itself but to no other thing. What is intended to be said by a = b seems to be that the signs or namesa' andb' designate the same thing, so that those signs themselves would be under discussion; a relation between them would be asserted. But this relation would hold between the names or signs only in so far as they named or designated something. It would be mediated by the connexion of each of the two signs with the same designated thing. But this is arbitrary. Nobody can be forbidden to use any arbitrarily producible event or object as a sign for something. In that case the sentence a = b would no longer refer to the subject matter, but only to its mode of designation; we would express no proper knowledge by its means. But in many cases this is just what we want to do. If the signa' is distinguished from the signb' only as object (here, by means of its shape), not as sign (i.e. not by the manner in which it designates something), the cognitive value of a = a becomes essentially equal to that of a = b, provided a = b is true. A difference can arise only if the difference between the signs corresponds to a difference in the mode of presentation of that which is designated. Let a, b, c be the lines connecting the vertices of a triangle with the midpoints of the opposite sides. The point of intersection of a and b is then the same as the point of intersection of b and c. So we have different designations for the same point, and these names (point of intersection of a and b,'point of intersection of b and c') likewise indicate the mode of presentation; and hence the statement contains actual knowledge.
It is natural, now, to think of there being connected with a sign (name, combination of words, letter), besides that to which the sign refers, which may be called the reference of the sign, also what I should like to call the sense of the sign, wherein the mode of presentation is contained. In our example, accordingly, the reference of the expressions
the point of intersection of a and b' andthe point of intersection of b and c' would be the same, but not their senses. The reference ofevening star' would be the same as that ofmorning star,' but not the sense. (...)
He argues that identity expressed between names is a relationship between their "modes of presentation" (senses/meanings) rather than between their names or reference object(s). This makes sense because different names can be synonymous or not, and only if they are we can infer equality, while in the latter case whether they are equal or unequal has to be established by other means.
The thing you have said (presence of an isomorphism) is not equality in category theory. Set-theoretic equality is equality in category theory (assuming doing category theory with set-theoretic foundations). Like, we could consider a (small) category as set of objects + set of morphisms + function assigning ordered pair of objects to each morphism.
Rather, what you're talking about is a certain type of equivalence relation (presence of an isomorphism). It doesn't always behave like equality, because it is not equality.
Not sure if this is the thing you're confused about or not, but seems worth make sure you're clear on the difference between judgemental equality and propositional equality. Chapter 1 of the Homotopy Type Theory book has a good explanation.
Different formalisations have different ideas of what “equals” means.
Principia Mathematica took the approach that for booleans p and q you have a relation p \equiv q, and then if you have some universe of objects and predicates on those objects, x equals y iff for all predicates f [in your universe of predicates] f(x) \equiv f(y).
But that’s not how typical automated theorem provers define equals.
PM is kind of backwards relative to how it’s usually done. You can start with equals as a primitive notion, and then have an axiom of referential transparency that x = y -> f(x) = f(y)
But PM did it backwards, define x = y as \forall f : f(x) \equiv f(y)
Whilst cycling today, I remembered that when reading Mark Kac's autobiography, Enigmas of Change, which is truly fantastic, his search for the meaning of probabilistic independence struck me as massive. What would it even mean to understand independence at a deep level? It's just P(A,B) = P(A)P(B), surely? The biography didn't truly answer that question for me, but it did gesture at what a deeper understanding might look like.
Which then reminded me that there was a famous analysis of the definition of equality in mathematics. So I figured, now's as good a time as any to get deeply confused about the most basic concept in mathematics. And I succeeded.
First off, a brush-up with equality. What's the standard definition? Well, it's a binary, reflexive, symmetric and transitive relationship. Or, at least, that's what an equivalence relation is. You can get a trivial equivalence relationship: everything's equivalent to everything else. Not selective enough to define equality.
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.
Maybe that comes from first order logic? How's equality defined there? Same as above, except there's for two big old schemas of properties it satisfies. First, if
for any function f we can cook up in our logic's syntax. Second,
for any property we can cook up in our logic's syntax.
In other words, if , then they can substitute for one another in anything we do to them.
Which is a heck of a lot more oomph than just saying equality is an equivalence relation. But now I'm less confused. I've undone all my hard work. I'll have to look at more definitions to remedy the situation.
OK, what about in category theory? There, the notion of equality depends on context. (And in type theory.) For in a category (objects plus maps between them) two objects are equal iff there is an isomorphism between them. That is, implies there is some with a corresponding inverse s.t.
Let me give an example. Take a category of shapes, but with only continuous functions between them. Then, a sphere and a cube are isomorphic to one another, i.e. they are equal. Wait, what?
Yes, a cube and a sphere are equal to one another if you only have continuous maps available to you. For the purposes of continuous maps, the distances between things don't matter, only topology. And a cube and a sphere have the same topology.
But if you enrich the category with some more discriminating maps, say distance preserving ones, then the sphere and cube are no longer equal. Conversely, if you reduce the category by removing all the isomorphisms between the sphere and the cube, then they are no longer equal.
This is what I meant by equality being contextual in category theory. Two objects may or may not be equal, depending on the category they're in. You can go to a "bigger" category and make two objects unequal. Or you can go to a smaller category and make them unequal.
But that doesn't make sense. In a theory in first order logic, whether two things are equal or not also depends on the context i.e. the axioms of the and theory you're working with. For instance, are the symbols "1" = "2" in first order logic? Depends on the axioms! You may not be able to prove it either way if the axioms are weak enough. Which is certainly the case if your theory has no axioms, except for the logical axioms assumed by the logic itself.
If you add some axioms and strengthen the theory, then you could get equality or inequality. But once you have it, adding axioms can't change whether two things are equal or not. At least, not without running into contradictions?
So what gives? Why is equality in category theory more "flexible" than of first order logic? And have I remystified equality for myself?
In both cases, equality is reflexive, symmetric, transitive and binary. In both cases, if two objects are equal, then you can substitute them for one another in any operation and wind up with equivalent results.
Is it just that you can have many different equalities between objects in category theory? Is it some weird feature of the semantics of the theory? My current guess is that the equivalent of the axiom schemas for equality from FOL in category theory are all the statements like . We can add/remove any of these conditions (except when ) from the category. But we can't do the same for the axiom schemas in FOL. And that's why they're more rigid.
So confusion dissolved? Well, at least until I tackle equality in programming.