major difference between the implementations in ZFC and NFU becomes evident. The Axiom of Infinity of ZFC tells us that there is a set A which contains and contains for each . This set A is not uniquely determined (it can be made larger while preserving this closure property): the set N of natural numbers is which is the intersection of all sets which contain the empty set and are closed under the "successor" operation . In ZFC, a set is finite if and only if there is such that : further, define as this n for finite A. (It can be proved that no two distinct natural numbers are the same size). The usual operations of arithmetic can be defined recursively and in a style very similar to that in which the set of natural numbers itself is defined. For example, + (the addition operation on natural numbers) can be defined as the smallest set which contains for each natural number and contains whenever it contains . In NFU, it is not obvious that this approach can be used, since the successor operation is unstratified and so the set N as defined above cannot be shown to exist in NFU (it is consistent for the set of finite von Neumann ordinals to exist in NFU, but this strengthens the theory, as the existence of this set implies the Axiom of Counting (for which see below or the New Foundations article)). The standard definition of the natural numbers, which is actually the oldest set-theoretic definition of natural numbers, is as equivalence classes of finite sets under equinumerousness. Essentially the same definition is appropriate to NFU (this is not the usual definition, but the results are the same): define Fin, the set of finite sets, as For any set , define as . Define N as the set . The Axiom of Infinity of NFU can be expressed as : this is enough to establish that each natural number has a nonempty successor (the successor of being for any ) which is the hard part of showing that the Peano axioms of arithmetic are satisfied. The operations of arithmetic can be defined in a style similar to the style given above (using the definition of successor just given). They can also be defined in a natural set theoretical way: if A and B are disjoint finite sets, define |A|+|B| as .