Uniqueness in Structural Set Theories, II
In set theory, using a 1-sorted first-order language $L$ with $=$ and $\in$, one defines a set to be empty just if it has no elements. That is,
It is a simple result that Extensionality implies that there is a unique empty set:
From Cantor on, the usual assumption is that the concept of set is inseparable from Extensionality.
But in Structural Set Theories, like $\mathsf{ETCS}$ and $\mathsf{SEAR}$, one cannot prove uniqueness of mathematical objects, and, in particular, the uniqueness of the empty set. Instead, an empty set is defined as an initial object in a certain category. (Lawvere (1964) gave the first categorical characterization of the set-theoretic universe.) And while one can prove that initial objects are (uniquely) isomorphic, one cannot prove that initial objects are identical: one cannot express that they are identical.
So---at least as I now understand it---in category theory, one can't prove, for objects $X,Y$ in a category $\mathcal{C}$, a uniqueness claim:
$\mathsf{Empty}(x)$ for $\forall y(y \notin x)$The axiom $\mathsf{Ext}$ of Extensionality states that sets with the same elements are identical:
$\forall x \forall y(\forall z(z \in x \leftrightarrow z \in y) \to x = y)$(This axiom can be modified to allow urelemente/atoms, by restricting the quantifiers $\forall x, \forall y$, to classes/sets.)
It is a simple result that Extensionality implies that there is a unique empty set:
$\mathsf{Ext} \vdash \forall x \forall y((\mathsf{Empty}(x) \wedge \mathsf{Empty}(y)) \to x = y)$For assume $\mathsf{Ext}$ and let $\mathsf{Empty}(x)$ and $\mathsf{Empty}(y)$. Given any $z$, we have $z \notin x$ and $z \notin y$. So, $z \in x \leftrightarrow z \in y$. So, by $\mathsf{Ext}$, $x = y$.
From Cantor on, the usual assumption is that the concept of set is inseparable from Extensionality.
But in Structural Set Theories, like $\mathsf{ETCS}$ and $\mathsf{SEAR}$, one cannot prove uniqueness of mathematical objects, and, in particular, the uniqueness of the empty set. Instead, an empty set is defined as an initial object in a certain category. (Lawvere (1964) gave the first categorical characterization of the set-theoretic universe.) And while one can prove that initial objects are (uniquely) isomorphic, one cannot prove that initial objects are identical: one cannot express that they are identical.
So---at least as I now understand it---in category theory, one can't prove, for objects $X,Y$ in a category $\mathcal{C}$, a uniqueness claim:
$(\mathsf{Initial}_{\mathcal{C}}(X) \wedge \mathsf{Initial}_{\mathcal{C}}(Y)) \to X = Y$And this is merely because one can't express identity of objects:
$X = Y$.So ... as far as I understand the conceptual ideology/assumptions of Category Theory (which I'm not so sure I do understand), there simply is no identity predicate for mathematical objects. It was quite surprising to me when I realised this might be so.
This post got me doing some reading on Category Theory and Structural Set Theory. I found this nLabs page. It seems that the upshot is that identity can't be expressed for all categories, but that within strict categories, identities can be expressed and assessed. Does this seem right to you?
ReplyDeleteIs your final statement about a Category Theory founded on something like SEAR (where identity would be meaningless)? It seems like that would be in-line with a certain way of thinking about structuralism (maybe the Shapiro route, where the mathematical "objects" are _merely_ places in a structure, and somehow not really objects).
Personally, I'm attracted to something where identity is defined within a category but is meaningless or always false across categories. This is sort of similar to the way Hale and Wright try to respond to the Caesar problem in "To Bury Caesar...". The only modification I'd make is something like a counterpart relation to substitute for identity across categories, where this would select counterparts based on structural similarity in most contexts.
Dennis,
ReplyDeleteThanks for those links. But I am still rather in the dark about the broad topic of identity in CT, due to my own ignorance, and I am enjoying reading up on it, as it's quite interesting. So, a strict category does have a notion of identity for its objects, unlike, e.g., ETCS and SEAR. And this issue is, as it turns out, important and central for CT-structuralism - articulated in Steve Awodey's article I linked to the other day.
CT-structruralism is strangely unlike Eliminative structuralism (Hellman) or Ante-rem structuralism (Resnik, Shapiro) that philosophers have written a lot about over the last thirty years! So, it seems like a genuinely separate kind of structuralism that one needs to try and understand. I intend to try and write something about these three kinds of structuralism.
Eliminative structuralism (Quine: ordinary sets, plus convenient definitional extensions)
Ante rem structuralism (Shapiro, Resnik: ordinary sets, plus ante rem structures)
Category-theoretic structuralism (Lawvere, McLarty, Awodey: sets are "structural" too...)
Well, a relativized identity predicate is not unknown, and thinking in terms of a counterpart relation seems an interesting idea!
Jeff
Well, I look forward to more postings on this stuff. I'm beginning to think it's time to learn some category theory.
ReplyDeleteThanks! Yes, it is interesting; and has probably unjustly been neglected by philosophers of mathematics. (I did once learn bits of category theory from Geroch's 1985 textbook, Mathematical Physics; but then forgot it all!)
ReplyDeleteJeff
Set theory can be used to compare and contrast. Using a Venn Diagram Maker we can create venn diagrams of 2-sets, 3-sets/4-sets or get creative with the app Creately. There are 100s of diagram templates and examples to be used freely in the diagram community of Creately online diagramming and collaboration software.
ReplyDelete