the axiom of infinity. This axiom asserts that there is a set I that contains 0 and is closed under the operation of taking the successor; that is, for each element of I, the successor of that element is also in I. Thus the essence of the axiom is: There is a set, I, that includes all the natural numbers. The axiom of infinity is also one of the von Neumann–Bernays–Gödel axioms. Extracting the natural numbers from the infinite set The infinite set I is a superset of the natural numbers. To show that the natural numbers themselves constitute a set, the axiom schema of specification can be applied to remove unwanted elements, leaving the set N of all natural numbers. This set is unique by the axiom of extensionality. To extract the natural numbers, we need a definition of which sets are natural numbers. The natural numbers can be defined in a way which does not assume any axioms except the axiom of extensionality and the axiom of induction—a natural number is either zero or a successor and each of its elements is either zero or a successor of another of its elements. In formal language, the definition says: Or, even more formally: Alternative method An alternative method is the following. Let be the formula that says "x is inductive"; i.e. . Informally, what we will do is take the intersection of all inductive sets. More formally, we wish to prove the existence of a unique set such that (*) For existence, we will use the Axiom of Infinity combined with the Axiom schema of specification. Let be an inductive set guaranteed by the Axiom of Infinity. Then we use the Axiom Schema of Specification to define our set - i.e. is the set of all elements of which happen also to be elements of every other inductive set. This clearly satisfies the hypothesis of (*), since if , then is in every inductive set, and if is in every inductive set, it is in particular in , so it must also be in . For uniqueness, first note that any set which satisfies (*) is itself inductive, since 0 is in all inductive sets, and if an element is in all inductive sets, then by the inductive property so is its successor. Thus if there were another set which satisfied (*) we would have that since is inductive,