The powerset as a function

Question

I understand that the existence of the powerset is usually taken as an axiom in ZFC, but why not simply view the powerset a function?

I know that you can define the powerset to be a function $P : V_\kappa \rightarrow V_{\kappa +1} $ where $V_{\kappa}$ is a stage on the Neumann universe, but recall that the stages of the Neumann universe are defined using the powerset. Is there any way to define the powerset as a function, without using the powerset itself in the definition? I guess that might be why its existence is taken as an axiom...?

Answer 1

As you know the collection of all sets is not a set at all.

Thus defining the power set as a function requires some domain different from the collection of all sets.

The power set is well defined but as if we try to define power set as a function with a domain and a codomain we will get into paradoxes.

Answer 2

You can take some other presentation of set theory as a basis where powersets aren't taken as axiomatic. For example, the presentation of an elementary topos as a finitely complete, cartesian closed category with a subobject classifier effectively takes the set of functions as a primitive notion and then power objects can be defined as $\mathsf PX\equiv\Omega^X$ where $\Omega$ is the subobject classifier.

However, what you're describing seems like you just want an operator corresponding to the powerset construction. We can just Skolemize the Axiom of Powerset and take $\mathsf P$ as the Skolem function witnessing the Axiom of Powerset. This is just a slight variation on the presentation of ZFC, and to some extent is what we do in practice informally. To be clear, the Skolem function is not a set-theoretic function but instead a new function symbol in the logic. It would make no more sense to ask if $(x,y)\in\mathsf P$ than it would to ask if $z\in\exists$.

Answer 3

Let $P$ denote the Power Set Axiom. We have Con($ZF - P)\implies$ Con (($ZF -P)+(\neg P)).$

Otherwise $P$ would be a theorem of ($ZF - P$) and $ZF$ would be euivalent to $(ZF -P).$ But in $ZF$ we can show that $H_{\omega_1},$ the set of hereditarily countable sets, is a model for $(ZF-P)+(\neg P).$

So any def'n, in $ZF- P,$ of power sets, that guarantees their existence, will require an extra axiom. Unless $ZF-P$ is already inconsistent.

Footnote. A set $x$ is hereditarily countable iff the transitive closure TrCl$( x)$ is countable. Let $x_0=x$ and $x_{n+1}=\cup x_n.$ Then TrCl$(x)=\cup_{n\in \omega}x_n.$