First-order logic contains, in addition to all symbols and rules of , the universal $\forall$ and existential $\exists$ quantifiers. These satisfy $\neg\forall xP(x)\iff\exists x\neg P(x)$ and $\neg\exists xP(x)\iff\forall x\neg P(x)$. First-order logic is used to build up the axioms of most set theory formulations, including Zermelo–Fraenkel.