In the formal language of the Zermelo-Fraenkel axioms, the axiom reads:
∃ ω, {} ∈ ω ∧ (∀ x, x ∈ ω ⇒ x ∪ {x} ∈ ω);
or in words: There is a set ω, such that the empty set is in ω and such that whenever x is a member of ω, the set formed by taking the union of x with its singleton {x} is also a member of ω.
To understand this axiom, first we define x ∪ {x} as the successor of x. Note that the axiom of pairing allows us to form the singleton {x}, and the axiom of union to perform the union. Successors are used to define the usual set theory encoding of the natural numbers. In this encoding, zero is the empty set (0 = {}), and 1 is the successor of 0:
1 = 0 ∪ {0} = {} ∪ = = {0}.
Likewise, 2 is the successor of 1:
2 = 1 ∪ {1} = {0} ∪ {1} = } = {0,1},
and so on. A consequence of this definition is that every natural number is equal to the set of all preceding natural numbers.
We might wish to form the set of all natural numbers, but it turns out that, using only the other axioms, this is impossible. The axiom of infinity thus assumes the existence of this set. It does this by a method similar to mathematical induction, by first assuming that ω contains zero, and then enforcing that for every element of ω, the successor of that element is also in it.
This set may contain more than just the natural numbers (they form a subset of it), but we may apply the axiom schema of specification to remove unwanted elements, leaving the set ω of all natural numbers. This set is unique by the axiom of extensionality.
Thus the essence of the axiom is:
There is a set containing all the natural numbers.
The axiom of infinity is also one of the von Neumann-Bernays-Gödel axioms.