# Translation of the Axiom schema of Separation into purely category-theoretic terms.

It is well-known the the category $\mathcal Set$ is a topos. In this topos, how would one translate the Axiom schema of Separation into purely category-theoretic terms? I ask this question because of the following theorem of Radu Diaconescu (found in his paper "Axiom of Choice and Complementation", Proceedings of the American Mathematical Society, Volume 51, Number 1, August 1975):

$AC$ implies that every subobject has a complement

Though this may show my ignorance regarding both the Axiom schema of Separation and Category theory, a cursory reading of Separation seems to suggest that, at least for subsets of some set $\mathcal S$ defined by some formula $\varphi$ in the language of set theory, these subsets have relative complements defined by the formula $\lnot$$\varphi. Also, in his paper, Diaconescu has the following theorem (from which the theorem stated above follows as a corollary. In stating this theorem, I will replace his chosen symbol \mathscr E for an arbitrary topos with the topos of my interest \mathcal Set: Any coequalizer of two nonintersecting monomorphisms has a section iff in \mathcal Set subobjects have complements. (Perhaps this theorem might give readers a clue as to how to translate the axiom schema of Separation into purely category-theory terms.) I am hoping by this to discover relations betwen the axiom schema of Separation and the Axiom of Choice (or, in the alternative, that no relation exists). Thanks in advance for any help given. (Addendum) Since Stefan, in his comment to me, raised the issue of the distinctness between the set-theoretic definition of complement and the category-theoretic definition of complement, I now ask the following question(s): In the category (Topos) \mathcal Set: in what ways does the category-theoretic definition of complement coincide with the set-theoretic definition of complement (if they coincide at all)? In what ways do they differ (if, in fact, they differ at all)? • I suspect your confusion to be caused by the different definition of "complement" in category theory. – Stefan Mesken Jul 18 '16 at 9:44 • @Stefan: Probably. How do they differ, and, more importantly, in the category \mathcal Set do they at all coincide? – Thomas Benjamin Jul 18 '16 at 10:29 • @Stefan: In any case, what is the translation of the axiom schema of Separation into the language of Category theory? – Thomas Benjamin Jul 18 '16 at 10:31 ## 1 Answer The point you're missing is that in a general topos, the internal logic is not necessary Boolean, so \neg does not necessarily give complements. Topological spaces are a good source of examples for intuitionistic logic; in a lattice of open sets, \neg gives the exterior of an open set. Usually, the complement of the set is not open, and thus does not exist in the lattice. Diaconescu proves that the axiom of choice implies that negations are complements. Here, I reserve "complement" for the case that we have • X \wedge \neg X = \bot • X \vee \neg X = \top The first (the law of noncontradiction) always holds in intuitionistic logic, but the second (the law of the excluded middle) may not. But regarding the question you asked, we have to decide what 'predicate' means. One formulation of internal logic is that predicates are subobjects, so the axiom of separation is a triviality. Another formulation of internal logic that works in toposes are that predicates on an object X are maps X \to \Omega; i.e. truth-valued functions on X. In a topos, the definition of the subobject classifier \Omega guarantees that there is a one-to-one correspondence between maps X \to \Omega and (equivalence classes of) subobjects of X, and so that's your axiom of separation. • Earlier today I was looking on nLab regarding the relation between Separation and AC and found the following notions: Full Separation is equivalent to the Axiom of Replacement and the Law of Excluded Middle; and, the Law of Excluded Middle is equivalent to the following statement--'finite sets are choice sets'. How does this relate to your statement that predicates on an object X are maps X$$\rightarrow$$\Omega$, where $\Omega$ is the subobject classifier? – Thomas Benjamin Jul 18 '16 at 23:49
• Your answer as it stands is helpful--if you can answer the question posted in my previous comment I will accept it. Thanks. – Thomas Benjamin Jul 18 '16 at 23:57
• @Thomas: There are various forms of first-order logic and of its semantics, especially as applied to a set theory. I was speaking of the internal language of the category; I had presumed from the question that specifically was what you were interested in. In that, all variables are bound to objects; in particular, the only separation principle you can even talk about in the internal language of a topos is 'bounded separation'. (p.s. the article at nLab says that full separation follws from AR and LeM, not that it is equivalent to) – user14972 Jul 19 '16 at 16:14
• Thanks for correcting me regarding my misstatement of what nLab said regarding $AR$ and LEM. – Thomas Benjamin Jul 20 '16 at 1:58