Revision in response to early comments. Users of set theory need an implementation (in case "model" means something different) of the axioms. I would expect something like this:
An implementation consists of a "collection-of-elements" $X$, and a relation
(logical pairing) $E:X\times X\to \{0,1\}$. A logical function $h:X\to\{0,1\}$
is a set if it is of the form $x\mapsto E[x,a]$ for some $a\in X$. Sets are
required to satisfy the following axioms: ….
The background "collection-of-elements" needs some properties to even get started. For instance "of the form $x\mapsto E[x,a]$" needs first-order quantification. Mathematical standards of precision seem to require some discussion, but so far I haven't seen anything like this. The first version of this question got answers like $X$ is "the domain of discourse" (philosophy??), "everything" (naive set theory?) "a set" (circular), and "type theory" (a postponement, not a solution). Is this a missing definition? Taking it seriously seems to give a rather fruitful perspective.
Best Answer
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
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):
EDIT: OK, the following is a bit long. The tl;dr is the following:
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:
(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:"
I have strong and wrong opinions on this matter, but I think that's off-topic for this specific question.