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. 

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.
