Can only the constructible sets be proven to exist in $ZF$ without benefit of extra assumptions? [closed]

Question

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".)

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", 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?

Answer 1

$\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".

Answer 2

There are several issues with this question; Andres has pointed out one glaring one, which is the conflation of theories and models. There is another issue, however, around what you are asking in the first place. Asaf has addressed one interpretation of your question, but there is another one:

Suppose $\varphi$ is a formula such that ZF proves "there is exactly one $x$ such that $\varphi(x)$ holds." Then does ZF prove "the unique $x$ such that $\varphi(x)$ holds is constructible?"

This matches more closely with e.g. Arai's theorem in his paper on lifting proof theory, where the focus is on when elements of definable, (ZF+V=L)-provably-nonempty sets enter $L$.

The answer to this question is very much no, for trivial reasons. Take $\varphi(x)$ to be "either $x=0^\sharp$, or $x=\emptyset$ and $0^\sharp$ doesn't exist." ZF proves that there is exactly one $x$ such that $\varphi(x)$ holds, but it is consistent with ZF that this $x$ is non-constructible.