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)?
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
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.