Axiom of power set
In the formal language of the Zermelo–Fraenkel axioms, the axiom reads:
- Given any set A, there is a set such that, given any set B, B is a member of if and only if every element of B is also an element of A.
Subset is not used in the formal definition because the subset relation is defined axiomatically; axioms must be independent from each other. By the axiom of extensionality this set is unique, which means that every set has a power set.
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 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.