In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:
where y is the Power set of x, .
In English, this says:
- Given any set x, there is a set such that, given any set z, this set z is a member of if and only if every element of z is also an element of x.
More succinctly: for every set , there is a set consisting precisely of the subsets of .
Note the subset relation is not used in the formal definition as subset is not a primitive relation in formal set theory; rather, subset is defined in terms of set membership, . By the axiom of extensionality, the set is unique.
The axiom of power set appears in most axiomatizations of set theory. It is generally considered uncontroversial, although constructive set theory prefers a weaker version to resolve concerns about predicativity.
The Power Set Axiom allows a simple definition of the Cartesian product of two sets and :
and, for example, considering a model using the Kuratowski ordered pair,
and thus the Cartesian product is a set since
Note that the existence of the Cartesian product can be proved without using the power set axiom, as in the case of the Kripke–Platek set theory.
- Paul Halmos, Naive set theory. Princeton, NJ: D. Van Nostrand Company, 1960. Reprinted by Springer-Verlag, New York, 1974. ISBN 0-387-90092-6 (Springer-Verlag edition).
- Jech, Thomas, 2003. Set Theory: The Third Millennium Edition, Revised and Expanded. Springer. ISBN 3-540-44085-2.
- Kunen, Kenneth, 1980. Set Theory: An Introduction to Independence Proofs. Elsevier. ISBN 0-444-86839-9.