definition of the ordered pair, which yields a type-level ordered pair. However, Quine's definition relies on set operations on each of the elements a and b, and therefore does not directly work in NFU. As an alternative approach, Holmes (1998) takes the ordered pair (a, b) as a primitive notion, as well as its left and right projections and , i.e., functions such that and (in Holmes' axiomatization of NFU, the comprehension schema that asserts the existence of for any stratified formula is considered a theorem and only proved later, so expressions like are not considered proper definitions). Fortunately, whether the ordered pair is type-level by definition or by assumption (i.e., taken as primitive) usually does not matter. The existence of a type-level ordered pair implies Infinity, and NFU + Infinity interprets NFU + "there is a type-level ordered pair" (they are not quite the same theory, but the differences are inessential). Conversely, NFU + Infinity + Choice proves the existence of a type-level ordered pair. Admissibility of useful large sets NF (and NFU + Infinity + Choice, described below and known consistent) allow the construction of two kinds of sets that ZFC and its proper extensions disallow because they are "too large" (some set theories admit these entities under the heading of proper classes): The universal set V. Because is a stratified formula, the universal set V = {x | x=x} exists by Comprehension. An immediate consequence is that all sets have complements, and the entire set-theoretic universe under NF has a Boolean structure. Cardinal and ordinal numbers. In NF (and TST), the set of all sets having n elements (the circularity here is only apparent) exists. Hence Frege's definition of the cardinal numbers works in NF and NFU: a cardinal number is an equivalence class of sets under the relation of equinumerosity: the sets A and B are equinumerous if there exists a bijection between them, in which case we write . Likewise, an ordinal number is an equivalence class of well-ordered sets. Finite axiomatizability New Foundations can be finitely axiomatized. Cartesian closure The category whose objects are the sets of NF and whose arrows are the functions between those sets is not Cartesian closed; Since NF lacks Cartesian closure, not every function curries as one might intuitively expect, and NF is not a topos. The consistency problem and related partial results For many years, the outstanding problem