Stratifiable formulae are not context-free

Abstract

Stratified formulae were introduced by Quine as an alternative way to attack Russell's Paradox. Instead of limiting comprehension by size (as in $\mathsf{ZF}$ set theory, using its axiom scheme of separation), unlimited comprehension is given to formulae that are in some sense descended from formulae of typed set theory. By keeping variables in a stratified structure, the most common candidates for inconsistency such as $\{x\mid x\notin x\}$ are eliminated. Under the usual syntax of set theory, the set of stratified formulae form a formal language. We show that, unlike the full class of well-formed formulae of set theory, this language is not context-free, and extend the result to its complement. Therefore, much like the axioms of $\mathsf{PA}$ and $\mathsf{ZF}$ (under their usual axiomatizations), the theory $\mathsf{NF}$ as a formal language is not context-free. We then introduce a non-standard syntax of set theory and show that with this syntax there is a restricted class of formulae, the exo-stratified formulae, that is context-free and full (up to relabelling of variables).