  To the extent that mathematical concepts can be implemented in the theory of wellfounded sets (aka ZF) they can also be interpreted in NF – since NF has a theory of wellfounded sets. However this is not the way in which we routinely interpret mathematics in NF since the interpreting formulæ are unstratified and unwieldy: extra axioms are needed. For example, the Von Neumann implementation of natural numbers tries to tell us that the collection of natural numbers is not the extension of a stratified formula, so it cannot be expected to be a set. By the same token, ordinary functions from the naturals to the naturals can fail to have extensions that are sets. Instead we trade on the fact that NF (and NFU too) admits a natural implementation of various kinds of mathematical entities as global isomorphism classes – which will of course be big sets (qv). The natural number \(n\) is implemented as the set of all \(n\)-membered sets: this is the Frege implementation used also in TST. Rosser [1953a] uses NF instead of ZF as a foundation for presenting ordinary mathematics (and to this day remains the only book to do so, though Holmes [1998] uses NFU for this purpose).