I am interested in asking the following question:



> 
> What sets can be proven to exist in $ZF$ without the benefit of extra assumptions? (Thanks to Toshiyasu Arai for inspiring me to ask this variation of his question from his slide presentation, ["Proof Theory for Set Theory"](http://www.helsinki.fi/lc2015/materials/slides_arai.pdf).)
> 
> 
> 


I ask this question for the following reasons:


(i). The model of $ZF$ + $V$=$L$ is the smallest inner model of $ZF$ for any model of $ZF$, so it would seem that in every model of $ZF$, constructible sets exist, and in fact, every model $\mathfrak M$ of $ZF$ believes that its constructible sets form 'the' constructible universe $L$ (and in fact they do, relative to $\mathfrak M$).


(ii). Since every hereditarily finite set is constructible (i.e., $V\_{\omega}$ = $L\_{\omega}$ so that for finite sets, $\mathscr P\_{Def}$ = $\mathscr P$-- see Peter Koepke's ["Simplified Constructibility Theory"](http://www.math.uni-bonn.de/people/koepke/Preprints/Simplified_constructibility_theory_minicourse_Helsinki.pdf), for the distinction between $\mathscr P\_{Def}$, the "predicative power-set operation" and $\mathscr P$, the "impredicative power-set operation"), one might reasonably abstract $\mathscr P\_{Def}$ from the finite sets as the 'correct' means for generating 'the' cumulative hierarchy of sets of $ZF$ from $\emptyset$.


(iii) Since it is known that $V\_{\omega}$ $\vDash$ $ZF$ $-$ *Infinity* (where in this case, $V\_{\omega}$ and $L\_{\omega}$ are, because *Infinity* is absent, proper classes), $L\_{\omega}$ $\vDash$ $ZF$ $-$ *Infinity* so that one might use the following lemma of Michael Rathjen (from his paper, "A Proof-Theoretic Characterization of the Primitive Recursive Set Functions", *JSL* Vol. 53, No.3, Sept. 1992)(my comments will be in square brackets):



> 
> Lemma 2.5. For each $\Delta\_0$-formula $\varphi$($x\_1$,...,$x\_n$) [in the language of set theory] with free variables among $x\_1$,..., $x\_n$ and each variable $x\_j$, 1$\le$$j$$\le$$n$, there is a term $\mathscr F$ on $n$ arguments built from $\mathscr F\_1$,...,$\mathscr F\_{10}$ [Jech's version of the G$\ddot o$del operations from his *Millemium Edition*, Chapt. 13] so that
> 
> 
> $KP^{-}$ [Kripke-Platek set theory with Foundation replaced with Set Foundation] $\vdash$ $\mathscr F$($a$,$x\_1$,...,$x\_{j-1}$,$x\_{j+1}$,...,$x\_n$) = {$x\_j$$\in$a| $\varphi$($x\_1$,...,$x\_n$)}
> 
> 
> Proof: All of the functions $\mathscr F\_1$,..., $\mathscr F\_{10}$ can be obtained on the basis of $KP^{-}$. For instance, $KP^{-}$ is strong enough to prove the existence of the Cartesian product $a$ $\times$ $b$ of sets $a$ ans $b$ (see [Barwise: *Admissible Sets ane Structures*, Chapt. I, Theprem 3.2]). The result now follows from [Barwise, Ibid., Chapt II, Assumption 5.2(v)] because inspection of the proof of [Barwise, Ibid., Chapt. II, Assumption 5.2(v)] reveals that all of its steps can be done within $KP^{-}$.
> 
> 
> 


Since $KP^{-}$ is a subtheory of $ZF$ $-$ *Infinity*, Lemma 2.5 holds for $ZF$ $-$ *Infinity* as well. Not that if one chooses to add *Infinity* back to $ZF$ $-$ *Infinity* one has that the proper class $V\_{\omega}$ (= $L\_{\omega}$) is now a set and is also constructible. Since $ZF$ $\vdash$ $\mathscr P\_{L}$($\omega$) $\subseteq$ $\mathscr P$($\omega$) ($\mathscr P\_{L}$ is the power-set for $L$ and is just $\mathscr P$($x$) $\cap$ $L$), Asaf's observation in his excellent answer (which is tantamount to saying that the constructibility or nonconstructibility of $\mathscr P$($\omega$) is independent of the axioms of set theory, i.e that though $\mathscr P$($\omega$) exists, it cannot be proven from the axioms of $ZF$ what subsets of $\omega$ are members of $\mathscr P$($\omega$)) seems to suggest (with the help of Rathjen's Lemma) that $ZF$ $\vdash$ $\mathscr P\_{L}$($\omega$) = $\mathscr P$($\omega$) unless one adds the axiom "There exists a non-constructible set of integers".


Considering these reasons, I can refine the question as follows:



> 
> Are the constructible sets the only sets that the axioms of $ZF$ alone can prove to exist?
> 
> 
> 



Can only the constructible sets be proven to exist in $ZF$ without benefit of extra assumptions?
$\sf ZF$ can prove that $\mathcal P(\omega)$ exists, but it cannot prove whether or not every subset of $\omega$ is constructible. In other words, there are sets which provably exist, but it is not provable that they are constructible. 


At the same time, as Mohammad writes, if one can prove that there exists a non-constructible set, then one disproves $V=L$, which means that $\sf ZF$ is already inconsistent to begin with.




---


Also, it is not true that $\mathcal P\_{\rm def}$ is the "right" power set, since if you look at the $L$-hierarchy, you'll find that new subsets of $\omega$ are added in unboundedly many countable steps below $\omega\_1$. So it is not right to say that $\mathcal P\_{\rm def}(\omega)$ is "the right power set of $\omega$", if we can prove that the "second power set also adds subsets".


