Power set
Set
context | X … set |
definiendum | Y∈P(X) |
postulate | Y⊆X |
Here we define
P(X)≡{Y∣Y⊆X}
which is sensible in our set theory if, for each set X, we have
∃!P.P={Y∣Y⊆X}
or, more formally,
∀X.∃!P.P={Y∣Y⊆X}
which is short for
∀X.∃!P.∀Y.(Y∈P⇔Y⊆X)
Discussion
The above is short for
∀X.∃!P.∀Y.(Y∈P⇔∀Z.(Z∈Y⟹Z∈X))
and this is, apart from the exclamation mark,exactly the Axiom of power set.
Like in the case of the empty set, uniqueness follows from extensionality.
Examples
We can prove
∀Y.(Y∈{∅}↔Y⊆∅)
Therefore, for X being ∅, we can show that the job of P is done by {∅}. In other words
P(∅)={∅} |
---|
Remarks
Generally, ∅∈P(X) for any X. Hence no power set is empty.
One also writes P(X)≡2X≡ΩX.
Reference
Wikipedia: Axiom of power set