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

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 odel 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?

closed as unclear what you're asking by Emil Jeřábek, RP_, Jan-Christoph Schlage-Puchta, Henry.L, Yoav KallusSep 1 '17 at 13:47

Please clarify your specific problem or add additional details to highlight exactly what you need. As it's currently written, it’s hard to tell exactly what you're asking. See the How to Ask page for help clarifying this question. If this question can be reworded to fit the rules in the help center, please edit the question.

• If one can prove the existence of non constructive sets in ZF then one can prove in ZF that $V \neq L$ but this contradicts the consistency of ZF+V=L. – Mohammad Golshani Aug 14 '17 at 15:29
• No! This was already explained to you in a previous version of this question: $\mathsf{ZF}+V=L$ is not a model, minimal or otherwise. It is a theory. You need to be more careful with these basic distinctions. – Andrés E. Caicedo Aug 14 '17 at 16:43
• Also, I have the feeling your use of $\mathcal P_{\mathrm{Def}}(x)$ is somewhat non-standard. What precisely do you mean by this: $\mathcal P(x)\cap L[x]$, $\mathcal P(x)\cap L(x)$? $L_{\alpha+1}\cap \mathcal P(x)$ for $x\in L$ and $\alpha$ least such that $x\in L_\alpha$? Something else? – Andrés E. Caicedo Aug 14 '17 at 16:46
• Also, what exactly do you mean by your question? Are you asking whether, if $\mathsf{ZF}$ proves that a formula defines a set, then the set is in $L$? (This is false.) Is it something more subtle? – Andrés E. Caicedo Aug 14 '17 at 16:48
• If you are asking about the ZF-provability of a specific statement $\varphi$ (such as "there are nonconstructible sets" or "all sets are constructible"), then please tell us what $\varphi$ is. (For the two examples I gave, the answers are "no" and "no", assuming that ZF is consistent.) – Goldstern Aug 17 '17 at 0:09

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

• +1. To clarify your last paragraph for the OP with an example: note that every real in $L_{\omega+1}$ is arithmetic; however, $0^{(\omega)}$ is a non-arithmetic real which is in $L_{\omega+2}$. – Noah Schweber Aug 14 '17 at 16:46
• @Thomas: That some sets exist. I don't understand your question. And frankly, I think that you don't understand your question either. – Asaf Karagila Aug 16 '17 at 14:18
• @Thomas: If ZF proves some set exists, then it proves that its power set exists; that its Hartogs and Lindenbaum numbers exist; that a bunch of other sets which have canonical definitions exist. The question has no "concrete" answer. Unlike PA, which has some nontrivial terms and can prove the existence of every natural number but not much more, ZF has only one relation symbol in the language of set theory so there are no non-trivial terms, and in particular there is no easy way to explain "which sets exist". Even more so, since "existence" is a semantic property, and provability is syntactic. – Asaf Karagila Aug 16 '17 at 17:42
• @Thomas: Until you actually suggest a predicative power set operation, this is all moot. Yes, any operation which is a reasonable "power set" one would not be $\mathcal P_{\rm def}$. At the very least, it would have to capture all the subsets in one shot, otherwise it is not quite a power set operation. You seem to continuously ignore this, despite this being pointed out by several people. So I am going to reserve my energy and do something else, and I encourage the others to do so as well. – Asaf Karagila Aug 25 '17 at 18:31
• @ThomasBenjamin What we should call $\mathcal{P}_{def}$, or what the phrase "predicative powerset" means, is irrelevant to the mathematics; do you understand why $\mathcal{P}_{def}$ cannot be the same as $\mathcal{P}$ in any model of ZF (including one satisfying "V=L")? And even this doesn't really have anything to do with your question, which Asaf has (I also have, but more confusingly) thoroughly addressed. You are trying to form a big web of ideas, but you still don't understand the basics and wind up mixing several confusions. You should stick to your question, which has been answered. – Noah Schweber Aug 25 '17 at 21:50

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.

• Also, take $\varphi(x)$ to be "$x$ is the power set of $\omega$" works. Which is what I was driving at. And you don't even need to exceed the consistency strength of ZFC for that either. :P – Asaf Karagila Aug 14 '17 at 17:08
• I think the OP would benefit from thinking carefully about what (if anything) is meant by saying, of a set $S$ (as opposed to something like a definition of $S$), that "ZF proves that $S$ exists." – Andreas Blass Aug 17 '17 at 2:29
• @ThomasBenjamin Yes, it is definable - in fact, it's a $\Pi^1_2$ singleton. This is because it doesn't code truth in $V$, but rather in $L$, and it only exists if $V\not=L$ (and indeed if the theory of $V$ is quite different from that of $L$ - in particular, if $0^\sharp$ exists then the theory of $V$ contains "there is a measurable cardinal" while of course the theory of $L$ can't!). So there is no way that $0^\sharp$ exists and describes truth in $V$. – Noah Schweber Aug 25 '17 at 16:17
• @Noah No, it contains "there is an $L$-measurable cardinal", or some such. But that is too informal. Thomas does not appear too clear yet on how weaker in consistency strength $0^\sharp$ is from a measurable, so that comment would probably increase confusion. – Andrés E. Caicedo Aug 25 '17 at 17:44
• @Todd " what I'm really interested in seeing is an explicit example " That has been addressed explicitly several times: $x=\mathcal P(\omega)$ is an obvious example. It was pointed out at the beginning of the thread and in the answers. The issue about definability of $0^\sharp$ will probably be much more confusing than illuminating in this context. If you are interested, I suggest you ask it as a separate question. – Andrés E. Caicedo Aug 25 '17 at 20:25