View source for Axiom of power set

{{short description|Concept in axiomatic set theory}}
{{More footnotes|date=May 2020}}
[[Image:Hasse diagram of powerset of 3.svg|thumb|250px|The elements of the power set of the set {{nowrap|{{mset|''x'', ''y'', ''z''}}}} [[order theory|ordered]] with respect to [[Inclusion (set theory)|inclusion]].]]

In [[mathematics]], the '''axiom of power set'''<ref>{{Cite web|url=https://www.britannica.com/science/axiom-of-power-set|title=Axiom of power set {{!}} set theory {{!}} Britannica|website=www.britannica.com|language=en|accessdate=2023-08-06}}</ref> is one of the [[Zermelo–Fraenkel axioms]] of [[axiomatic set theory]]. It guarantees for every set <math>x</math> the existence of a set <math>\mathcal{P}(x)</math>, the [[power set]] of <math>x</math>, consisting precisely of the [[subset]]s of <math>x</math>. By the [[axiom of extensionality]], the set <math>\mathcal{P}(x)</math> 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]].

== Formal statement ==
The subset relation <math>\subseteq</math> is not a [[primitive notion]] in [[formal set theory]] and is not used in the formal language of the Zermelo–Fraenkel axioms. Rather, the subset relation <math>\subseteq</math> is defined in terms of [[set membership]], <math>\in</math>. Given this, in the [[formal language]] of the Zermelo–Fraenkel axioms, the axiom of power set reads:
:<math>\forall x \, \exists y \, \forall z \, [z \in y \iff \forall w \, (w \in z \Rightarrow w \in x)]</math>
where ''y'' is the power set of ''x'', ''z'' is any element of ''y'', ''w'' is any member of ''z''.

In English, this says:
:[[Given any]] [[Set (mathematics)|set]] ''x'', [[Existential quantification|there is]] a set ''y'' [[such that]], given any set ''z'', this set ''z'' is a member of ''y'' [[if and only if]] every element of ''z'' is also an element of ''x''.

== Consequences ==

The power set axiom allows a simple definition of the [[Cartesian product]] of two sets <math>X</math> and <math>Y</math>:

:<math> X \times Y = \{ (x, y) : x \in X \land y \in Y \}. </math>

Notice that
:<math>x, y \in X \cup Y </math>
:<math>\{ x \}, \{ x, y \} \in \mathcal{P}(X \cup Y) </math>

and, for example, considering a model using the [[Ordered_pair#Defining_the_ordered_pair_using_set_theory|Kuratowski ordered pair]],

:<math>(x, y) = \{ \{ x \}, \{ x, y \} \} \in \mathcal{P}(\mathcal{P}(X \cup Y)) </math>

and thus the Cartesian product is a set since

:<math> X \times Y \subseteq \mathcal{P}(\mathcal{P}(X \cup Y)). </math>

One may define the Cartesian product of any [[finite set|finite]] [[class (set theory)|collection]] of sets recursively:

:<math> X_1 \times \cdots \times X_n = (X_1 \times \cdots \times X_{n-1}) \times X_n. </math>

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]].

== Limitations ==

The power set axiom does not specify what subsets of a set exist, only that there is a set containing all those that do.<ref>{{cite book |last1=Devlin |first1=Keith |title=Constructibility |date=1984 |publisher=Springer-Verlag |location=Berlin |isbn=3-540-13258-9 |pages=56–57 |url=https://projecteuclid.org/eBooks/perspectives-in-logic/constructibility/toc/pl/1235419477 |access-date=8 January 2023}}</ref> Not all conceivable subsets are guaranteed to exist. In particular, the power set of an infinite set would contain only "constructible sets" if the universe is the [[constructible universe]] but in other models of ZF set theory could contain sets that are not constructible.

== References ==
{{Reflist}}
* [[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}}.

{{PlanetMath attribution|id=4399|title=Axiom of power set}}

{{Set theory}}

[[Category:Axioms of set theory]]

[[de:Zermelo-Fraenkel-Mengenlehre#Die Axiome von ZF und ZFC]]