Are quantifiers a primitive notion? Are quantifiers a primitive notion? I know that one can be defined in terms the other one, so question can be posed, for example, like this: is universal quantifier a primitive notion?  I know, that $\forall x P (x) $ can be viewed as a logical conjunction of a predicate $ P $ being applied to all possible variables in, for example, $\sf ZFC$. But how can one write such a statement down formally? Also, it seems you can not use the notion of a set to define the domain of discourse, because you are trying to build $\sf ZFC$ from scratch, and sets make sense only inside $\sf ZFC$. Obviously, I'm missing a lot here. Any help is appreciated. 
 A: (1) "$∀xP(x)$ can be viewed as a logical conjunction of a predicate $P$ being applied to all possible variables in, for example, ." Not so. The language of ZFC has only countably many terms $\tau$ so even if you allow infinite conjunctions of the form $P(\tau_0) \land P(\tau_1) \land P(\tau_2) \land \ldots$ you can't get something equivalent to the universal quantification over the uncountable domain of sets.
The basic point, of course, is this (a general observation about quantification, not especially about ZFC). In the general case, the language of a theory $T$ won't have a term $\tau$ for every object in the domain of quantification, so that a conjunction of wffs $P(\tau_0)$ -- even an infinitary one -- won't be equivalent to a universal claim $∀xP(x)$ in $T$.
(2) Is the universal quantifier a primitive notion? Well, grasping $∀xP(x)$ involves understanding something more than understanding conjunctions of wffs like $P(\tau)$ (whether finite or infinitary ones). It involves understanding that the quantification will be false if there is an unnamed object which doesn't satisfy $P$, compatibly with all the named objects satisfying $P$, and hence the conjunction of wffs of the form $P(\tau_0)$ being true. So we do indeed have a new notion here over an above the idea of a conjunction. 
A: Note for example in PA  that even if $P(0)$ and $P(1)$ and $P(2)$ and ... are all theorems, it may happen that $\forall n\colon P(n)$ is not a theorem. Thus $\forall n\colon P(n)$ is in fact something different from $P(0)\land P(1)\land P(2)\land \ldots$ even if one were to accept such an infinte string as a wff (which  is a box of Pandora that should not be opened as in the next step such an infinite conjuntion would reuire an infinte proof and so on).
So this means that quantification does bear a "new" notion and should be considered primitive.
A: Well, I would say they are a primitive notion. Usually formal systems such as FOST only include one, since one of them can be defined in terms of another. For example, $\exists \alpha (\varphi(\alpha))$ is the same as $\neg (\forall \alpha (\neg \varphi(\alpha)))$, and $\forall \alpha (\varphi(\alpha))$ is the same as $\neg (\exists \alpha (\neg \varphi(\alpha)))$. But I agree with Hagen von Eitzen. A good example of this is that "TREE(n) is finite" can be proved for all n, but "for all n, TREE(n) is finite" cannot be proved.
