Consider a normal first course on category theory (say up to and including the statement and proof) of the adjoint functor theorem (AFT). What are the minimal assumptions for the definition of a set one needs to make in order that everything works? As far as I understand, up to and including the AFT there is very little one needs besides that fact that sets should have elements and that we have avoided Russell's paradox. So what is a minimal set of axioms allowing this to work?
Basic Category Theory – Minimal Set Theory Assumptions
adjoint-functorsct.category-theoryset-theory
Related Solutions
George Boolos has a number of very readable (to the non-expert like me) essays on this subject. Try "The Iterative Conception of Set" in Logic, Logic and Logic. He tries to find a way to look at the axioms of ZF set theory from a perspective that makes them look natural and not simply contrived to avoid paradoxes. I don't know anything about how Boolos's views are seen by other Set Theorists.
Caveat: it's become clear from comments and revisions that the original portion of this answer - leading up to the horizontal line below - is not really addressing the heart of the OP. I'm leaving it up since I think it is still at least somewhat relevant and potentially useful to readers. See below the horizontal line for an answer I thnk is ultimately more on-topic.
There is no circularity here.
A model of ZFC is simply a set $X$ together with a binary relation $E$ on $X$, satisfying some properties. We intuitively think of elements of $X$ as sets, but this is an intuition we impose on models of the theory from outside; a priori, a model of ZFC is just a special kind of (directed) graph.
For example, thinking of models of ZFC as graphs, the extensionality axiom just says
If two vertices are connected "from the left" to the same vertices, then they are in fact the same vertex. (More precisely: if $u, v$ are vertices such that for every vertex $w$ we have $wEu\iff wEv$, then in fact $u=v$.)
So for example, the discrete graph (= no edges at all) on two vertices is not a model of ZFC: the two vertices are each connected "from the left" to the same vertices (namely, none), but they are distinct.
Note that this demonstrates a fundamental point about ZFC (which is an instance of a more general fact about first-order theories in general):
The ZFC axioms describe, but do not define, sets.
EDIT: OK, the following is a bit long. The tl;dr is the following:
If we're skeptical of philosophical commitments such as Platonism (which I think we should be), then the right response to the circularity involved in defining mathematical objects in terms of sets while recognizing sets as mathematical objects is this: that all semantic reasoning, such as the development of model theory, is really syntactic reasoning taking place in a formal theory which we're choosing to interpret as being "about" objects whose existence is dubious, false, or meaningless. These syntactic claims (such as "ZFC proves that no set contains itself") are just statements about finite strings, and we can make sense of them even in a purely empirical way.
OK, now the long version:
Based on your edit (as far as I can tell, your "implementations" are just models), I think you're asking:
To what extent do we need to make set-theoretic commitments to do model theory?
(Note that I said "model theory," not "logic;" I'll say more about that in a moment.)
The answer is that we do in fact need to presuppose a notion of set. If one is a Platonist, this isn't necessarily problematic, and a formalist will dispense with the entire apparatus altogether and simply look at the formal system it takes place in (again, more on that in a moment).
There is also the option that what we really have here is a way of taking any "notion-of-set" and producing a corresponding model theory; this is exemplified by topos theory, where each topos can be understood as a universe of sets and model theory can be developed inside the topos. Based on your most recent comment to me, I think this might be interesting to you, but ultimately it runs into the same problem: we wind up having to talk about some sort of mathematical objects to develop semantics for mathematical statements, and this is ultimately no less circular or demanding of Platonism.
Now, what if we are unwilling to make any set-theoretic commitments at all? One approach is to argue that the whole semantic apparatus of model theory, and indeed all of mathematics, is not describing anything but rather is simply taking place inside a formal theory. That is, we don't view the statement "If there is a countable transitive model of ZFC, then there is a countable transitive model of ZFC + CH" as really referring to "countable transitive models," but rather is simply a string of symbols which has been produced by a certain formal system. The fundamental question of formalism, to my mind, is why the formal systems we do math in are valuable and interesting, but there's no doubt that formalism provides a vehicle for doing mathematics with the minimal philosophical commitment.
Now, after all, we do need some commitments to get off the ground. For "naive" formalism, this amounts to a commitment to the "existence" of the natural numbers in some sense; further examining this notion, we can try to reduce the philosophical commitment involved even further. For example, "truly empirical" mathematics is extremely ultrafinitist: the only things one is allowed to assert is "the string $\sigma$ is deducible from the strings $\sigma_1, ...,\sigma_n$," and only in the case when one actually has a formal deduction of $\sigma$ from $\sigma_1,...,\sigma_n$.
Why am I bringing this up? Well, the point I want to make is that formalism helps us not worry (as much) about circularity without invoking some kind of Platonism. Specifically, while one can be suspicious of set-theoretic foundations of mathematics because of the circularity involved in defining mathematical objects via sets while sets themselves are mathematical objects, a claim like "ZFC proves $\sigma$" is universally intelligible. Essentially, what this means to me is that we can do mathematics as if we were Platonists without actually making the philosophical commitments involved in any serious way, and still be doing "honest mathematics" - the point being that the formalist perspective gives us a bulwark to "fall back to."
This "optional Platonism," I think, is why mathematicians tend not to care about these issues; we tend to recognize that we could reduce all our reasoning to concrete statements about finite strings, and therefore that our Platonist statements can be translated into obviously meaningful ones.
Of course, this translates (one of) the Platonist challenge(s) - "In what sense can mathematical objects be said to exist, and why are we justified in claiming that they do?" - into the "formalist challenge:"
What criteria determine whether a formal theory is "mathematically valuable"?
I have strong and wrong opinions on this matter, but I think that's off-topic for this specific question.
Best Answer
To complement Tom Leinster's answer, let me try to be specific:
To form the product category $\mathcal{C} \times \mathcal{D}$, we need ordered pairs, which we can get from the axiom of unordered pairs.
It's probably a good idea to have the empty set $\emptyset$, so that the initial category exists.
My experience from type theory leads me to believe that we want function extensionality, or else we cannot reasonably work with functors and natural transformations (which are functions). Function extensionalty is equivalent to set-theoretic extensionalty.
To form the hom-set $\mathrm{Hom}(A,B) = \{f \in \mathcal{C}_1 \mid \mathrm{dom}(f) = A \land \mathrm{cod}(f) = B\}$ we seemingly need bounded separation. It's a little more difficult to see whether we need unbounded separation (my guess would be that we can work pretty nicely without it).
To form functor categories, we need powersets. Indeed, given any set $A$, its powerset may be generated as the set of objects of the functor category $2^A$, where $2$ is the discrete category on two objects.
There are two functors form the terminal category $\mathbf{1}$ to the arrow category $\bullet \to \bullet$. If we think their coequalizer exists (in the category of small categories) then we believe in the axiom of infinity, because the coequalier is the monoid of natural numbers.
I am pretty sure the axiom of choice and excluded middle are not needed for general category theory, and foundation also seems quite irrelevant. How about union and replacement?