In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom of pairing is one of the axioms of Zermelo–Fraenkel set theory.
It was introduced by Zermelo (1908) as a special case of his axiom of elementary sets.
Thus the essence of the axiom is: The set {A,A} is abbreviated {A}, called the singleton containing A.
Being able to construct a singleton is necessary, for example, to show the non-existence of the infinitely descending chains
, the ordered pair is defined by the following: Note that this definition satisfies the condition Ordered n-tuples can be defined recursively as follows: The axiom of pairing is generally considered uncontroversial, and it or an equivalent appears in just about any axiomatization of set theory.
Nevertheless, in the standard formulation of the Zermelo–Fraenkel set theory, the axiom of pairing follows from the axiom schema of replacement applied to any given set with two or more elements, and thus it is sometimes omitted.
Using the axiom schema of separation we can construct the set whose members are exactly
And this could be used to generate all hereditarily finite sets without using the axiom of union.
We can extend this schema to include n=0 if we interpret that case as the axiom of empty set.
Normally, however, one uses the axioms of empty set and pairing separately, and then proves this as a theorem schema.