power set

Power sets


Given a set SS, the power set of SS is the set 𝒫S\mathcal{P}S of all subsets of SS. Equivalently, it is

  • the set TV S\TV^S of all functions from SS to the set TV\TV of truth values. This is often written 2 S2^S, since there are (at least in classical logic) exactly 22 truth values;

  • the collection of subobjects of XX in the topos Set.

  • the slice category Inj/SInj/S, where Inj is the wide subcategory of Set with morphisms restricted to injections. This is similar to the subobject definition but is more unpacked. Inj/SInj/S has objects that are injections to SS and morphisms that are commuting triangles of injections.

Foundational status

One generally needs a specific axiom in the foundations of mathematics to ensure the existence of power sets. In material set theory, this can be phrased as follows:

Axiom (power sets)

If SS is a set, then there exists a set 𝒫\mathcal{P} such that Aβˆˆπ’«A \in \mathcal{P} if AβŠ†SA \subseteq S.

One can then use the axiom of separation (bounded separation is enough) to prove that 𝒫\mathcal{P} may be chosen so that the subsets of AA are the only members of 𝒫\mathcal{P}; the axiom of extensionality proves that this 𝒫\mathcal{P} is unique.

In structural set theory, we state rather that there exists a set 𝒫\mathcal{P} which indexes the subsets of AA and prove uniqueness up to unique isomorphism.

In predicative mathematics, the existence of power sets (along with other β€œimpredicative” axioms) is not accepted. However we can still speak of a power set as a proper class, sometimes called a power class.

One can use power sets to construct function sets; the converse also works using excluded middle (or anything else that will guarantee the existence of the set of truth values). In particular, power sets exist in any theory containing excluded middle and function sets; thus predicative theories which include function sets must also be constructive.


Last revised on April 15, 2015 at 22:31:01. See the history of this page for a list of all contributions to it.