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. 

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.
