1914, Norbert Wiener showed how to code the ordered pair as a set of sets, making it possible to eliminate relation types in favor of the linear hierarchy of sets described here. Quinean set theory Axioms and stratification The well-formed formulas of New Foundations (NF) are the same as the well-formed formulas of TST, but with the type annotations erased. The axioms of NF are: Extensionality: Two objects with the same elements are the same object; A comprehension schema: All instances of TST Comprehension but with type indices dropped (and without introducing new identifications between variables). By convention, NF's Comprehension schema is stated using the concept of stratified formula and making no direct reference to types. A formula is said to be stratified if there exists a function f from pieces of 's syntax to the natural numbers, such that for any atomic subformula of we have f(y) = f(x) + 1, while for any atomic subformula of , we have f(x) = f(y). Comprehension then becomes: exists for each stratified formula . Even the indirect reference to types implicit in the notion of stratification can be eliminated. Theodore Hailperin showed in 1944 that Comprehension is equivalent to a finite conjunction of its instances, so that NF can be finitely axiomatized without any reference to the notion of type. Comprehension may seem to run afoul of problems similar to those in naive set theory, but this is not the case. For example, the existence of the impossible Russell class is not an axiom of NF, because cannot be stratified. Ordered pairs Relations and functions are defined in TST (and in NF and NFU) as sets of ordered pairs in the usual way. The usual definition of the ordered pair, first proposed by Kuratowski in 1921, namely , has a serious drawback for NF and related theories: the resulting ordered pair (a, b) necessarily has a type two higher than the type of its arguments a and b. Hence for purposes of determining stratification, a function is three types higher than the members of its field. If one can define a pair in such a way that its type is the same as that of its arguments (resulting in a type-level ordered pair), then a relation or function is merely one type higher than the type of the members of its field. Hence NF and related theories usually employ Quine's set-theoretic