Processing math: 100%

Power set

Set

context X … set
definiendum YP(X)
postulate YX

Here we define

P(X){YYX}

which is sensible in our set theory if, for each set X, we have

!P.P={YYX}

or, more formally,

X.!P.P={YYX}

which is short for

X.!P.Y.(YPYX)

Discussion

The above is short for

X.!P.Y.(YPZ.(ZYZX))

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


Context

Link to graph
Log In
Improvements of the human condition