power set (changes) in nLab

Showing changes from revision #33 to #34: Added | Removed | Changed

Definition

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 X S X S 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

In material set theory

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:

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

Alternatively, one could include a powerset structure, a primitive unary operator 𝒫(S)\mathcal{P}(S) such that for all sets SS, if for all sets AA and sets BB, B∈AB \in A implies that B∈SB \in S, then A∈𝒫(S)A \in \mathcal{P}(S).

In structural set theory

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 dependent type theory

In dependent type theory, it is possible to define a Tarski universe (V,∈)(V, \in) of pure sets which behaves as a material set theory. The universal type family of the Tarski universe is given by the type family x:V⊢∑ y:Vy∈xx:V \vdash \sum_{y:V} y \in x. The axiom of power sets is given by the following inference rule:

ΓctxΓ⊢powersets V:∏ S:V∑ 𝒫:V∏ A:V(∏ x:V(x∈A)→(x∈S))→(A∈𝒫)\frac{\Gamma \; \mathrm{ctx}}{\Gamma \vdash \mathrm{powersets}_V:\prod_{S:V} \sum_{\mathcal{P}:V} \prod_{A:V} \left(\prod_{x:V} (x \in A) \to (x \in S)\right) \to (A \in \mathcal{P})}

Status in predicative mathematics

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.

Relation to function sets and the set of truth values

The existence of power sets is equivalent to the existence of function sets and a set of truth values.

In dependent type theory

In dependent type theory, this is equivalent to the existence of function types and a univalent type of all propositions. If one has a univalent type of all propositions (Prop,El)(\mathrm{Prop}, \mathrm{El}), then given a type SS, the power set of SS is the function type 𝒫S≔S→Prop\mathcal{P}S \coloneqq S \to \mathrm{Prop}. The power set of a type is always a set, because Prop\mathrm{Prop} is always a set by univalence; and if the codomain of a function type is a set, then the function type itself is a set.

An element of a power set P:𝒫SP:\mathcal{P}S is a predicate. The type

∑ x:SEl(P(x))\sum_{x:S} \mathrm{El}(P(x))

is the corresponding subtype of SS, with canonical embedding given by the first projection function defined in the elimination rules of the negative dependent sum type.

π 1:(∑ x:SEl(P(x)))→S\pi_1:\left(\sum_{x:S} \mathrm{El}(P(x))\right) \to S

There is also a local membership relation (−)∈ S(−):𝒫(S×𝒫S)(-)\in_S(-):\mathcal{P}(S \times \mathcal{P}S) defined by a∈ SB≔B(a)a \in_S B \coloneqq B(a) for all a:Sa:S and B:𝒫SB:\mathcal{P}S, where B(a)B(a) is defined in the elimination rules for function types.

Properties

General

• The power set 𝒫S\mathcal{P}S canonically carries a partial order by containment, making it a poset: AA precedes BB means that AA is a subset of BB (A⊆BA \subseteq B).

• Cantor's theorem states that there exists no surjection from SS to 𝒫S\mathcal{P}S; as there does exist such an injection, one concludes that

  |S|<|𝒫S| {|S|} \lt {|\mathcal{P}S|}

  in the usual arithmetic of cardinal numbers.

• Power sets live in the category Set. Given an object SS of any category, one can similarly form a poset of subobjects of SS; the category is called well-powered when this poset is small. One also has an internal notion of power set (a power object) in a topos.

• The power set construction constitutes an equivalence of categories between the opposite category Setop^{op} and that of complete atomic Boolean algebras. See at Set – Properties – Opposite category and Boolean algebras. Restricted to finite sets, the power set construction constitutes an equivalence of categories between the opposite category of FinSet and that of finite Boolean algebras. See at FinSet – Opposite category.

Power set functor

The power set construction gives rise to two functors, the contravariant power set functor Set op→SetSet^op \to Set and the covariant power set functor Set→SetSet \to Set. The first sends a function f:S→Tf\colon S\to T to the preimage function f *:P(T)→P(S)f^*\colon P(T) \to P(S), whereas the second sends ff to the image function f *:P(S)→P(T)f_*\colon P(S) \to P(T).

• A closure operator on a power set is a Moore closure.

• power object

• poly-morphism