In material set theory as a foundation of mathematics, the axiom of pairing is an important axiom needed to get the foundations off the ground (to mix metaphors). It states that unordered pairs exist.
The axiom of pairing (or axiom of pairs) states the following:
If and are (material) sets, then there exists a set such that .
Using the axiom of separation (bounded separation is enough), we can prove the existence of a particular set such that and are the only members of . Using the axiom of extensionality, we can then prove that this set is unique; it is usually denoted and called the unordered pair of and . Note that may also be denoted simply .
The axiom of pairing is the binary part of a binary/nullary pair whose nullary part is the axiom stating the existence of the empty set. We can use these axioms and the axiom of union to prove every instance of the following axiom (or rather theorem) schema of finite sets:
If are sets, then there exists a set such that .
Again, we can prove the existence of specific such that are the only members of and prove that this is unique; it is denoted and is called the finite set consisting of .
Note that this is a schema, with one instance for every (metalogical) natural number. Within axiomatic set theory, this is very different from the single statement that begins with a universal quantification over the (internal) set of natural numbers. In particular, each instance of this schema can be stated and proved without the axiom of infinity.
Of course, there is one proof for each natural number.