What is the relation between axiomatic set theory and logical quantifiers? On the one hand, the logical predicates $\forall$ and $\exists$ are defined using the concept of a Domain of Discourse, which itself is defined as a set (at least according to wikipedia).  On the other hand, axiomatic set theory defines the basic properties of set using these quantifiers (e.g. the Axiom of the Empty Set: $\exists x\forall y\,\neg(y\in x)$). This seems like a circular definition. If someone could please clarify this, I would be most greatful.
 A: We need not think of $\forall$ as defined in terms of a domain of quantification. Rather, we can take it to be a ${\it primitive}$ of our language. Definition has to stop somewhere, and the quantifiers seem like a pretty basic place to stop! Of course, a quantifier may ${\it have}$ a domain of quantification even if it isn't defined in terms of it. "is red", for instance, isn't defined in terms of the set of red things, although its extension (the set of things it applies to) is the set of red things. 
Here's one way to see quantifiers aren't in general defined in terms of sets. It is perfectly coherent to think there are no sets (although it's not true) -- that is, to think $\neg\exists x(x$ is a set$)$. Perhaps one thinks that the only things which exist are physical. But if the quantifier $\exists$ were defined in terms of sets, it wouldn't be coherent to think this. 
A: 
The logical predicates ∀ and ∃ are defined using the concept of a Domain of Discourse, which itself is defined as a set.

This much is true: to fix the content of e.g. $\forall xFx$, we need to know which objects the quantifier is ranging over -- i.e. which objects are such that each of them supposedly satisfies the predicate $F$.
But to understand $\forall xFx$ we don't have to assume that the objects which are being quantified over form a set. (If quantification required the objects we are quantifying over to form a set, that would be very bad news for set theory! -- for in a quantified claim of ZFC, the quantifiers are supposedly quantifying over all sets, yet according to ZFC itself the sets do not themselves form a set!)
It is a quirk of the history of logic that the formalized theories of logic inference that became canonical aimed to regiment singular reference and associated quantifiers and ignored plural reference and plural quantifiers (even though we use plural talk in informal maths all the time). So in formally regimenting our informal semantics for quantifiers we find ourselves substituting natural talk about the objects (plural) a quantifier runs over by talk about the domain of quantification (singular). But that's an artefact of our formalisation, not an insight!   
A: The quantifiers are symbols in syntax, nothing more. The string $\exists x: \forall y:  \neg (y \in x)$ is simply a string in a "game of symbols" (axiomatic set theory). The axioms and proof rules serve for manipulating strings (from the viewpoint of the metatheory).
Remaining within the object theory, we take a proof theoretic approach. In this case, we usually use a finitistic metatheory.
When we interpret the symbols of a theory in a metatheory that contains "sets" (e.g., the "domain of discourse"), then what we are doing is using as our metatheory set theory itself. It could be the same theory. So, the metatheory in this case involves infinitary reasoning. This approach is usually called model theory.
One way to think about this is that we have set theory as rules about symbols, and then we can ask the question "Can we encode this theory itself using values (sets) within itself?". Gödel did so to show that if we encode ZF within itself and try to prove it is consistent, then either we cannot prove it (in case ZF is consistent), or we can (and that shows ZF is inconsistent).
Kenneth Kunen gives a very good introduction to the subject in his book Foundations of mathematics.
