Quantification over uncountable sets

Question

If some statements below are too imprecise/peculiar, please note that this is mostly due to my own lack of knowledge/understanding. Nevertheless, I will try to phrase the actual question in a more precise way.

Background: Consider a statement of the form: $\forall x \in \omega_1 \, [P(x)]$. Suppose that we don't want all statements with the form in previous sentence to be necessarily either true or false. I suppose the idea here is that $\omega_1$, since it isn't countable, should be consider "too big" (so similar points would also apply to $\omega_2$, $\omega_3$ etc.).

Now, I should perhaps mention here (at the risk of sounding very very confusing) that I have read (at few occasions) suggestions that something like $\omega_1$ should be treated as a proper class. I suppose I see some similarity of this suggestion with previous paragraph that perhaps (very loosely) we want to say that: "$\omega_1$ is something like $\mathrm{Ord}$". However, in terms of actual logic, I have no idea whether it does or does not relate to what I wrote in previous paragraph (I simply don't have enough facility with logic for this).

I have added the previous paragraph that perhaps if someone wants to enlighten the link (in the case there is one) between the previous two paragraphs for laymen, it would be quite useful.

Actual question: Consider $\mathrm{ZF}$ set theory where: (1) we remove the power-set axiom (2) we add the constructibility axiom. I want to know what is known about the proof-theoretic work along the lines of such a theory as a whole or perhaps some of its "fragments". Not sure if "fragments" is the right word but what I want to imply, loosely speaking, is weaker subsystems of the theory (that try to cover some important parts of it).

Also, a silly side question (which unfortunately also reveals my lack of understanding/knowledge). Since we are also removing power-set axiom (on top of adding constructibility), does the removal or non-removal of $\mathrm{AC}$ make any difference to the question in previous paragraph? My uneducated "guess" is probably not, but please correct if it does.

Answer 1

There are several things one can say.

The theory of ZFC without powerset is often denoted by $\newcommand\ZFCm{\text{ZFC}^-}\ZFCm$. One has to be a little careful with what it means, since collection and replacement are no longer equivalent without powerset (Zarach), and things break down without collection---see further discussion in Gitman, Hamkins, Johnstone, What is the theory ZFC without power set?, Math. Log. Q. 62, No. 4-5, 391-406 (2016). ZBL1375.03059. Meanwhile, once you add the axiom of constructibility, one can recover the equivalence of collection and separation, as $V=L$ provides global choice and hence definable Skolem functions (and this observation addresses your question at the end of the post about AC).

There are many natural models of $\ZFCm$, including especially the hereditarily countable sets $H_{\omega_1}$, in which indeed $\omega_1$ constitutes the class of all ordinals. This is a very robust model, in which every ordinal and indeed every set is countable. Some mathematicians and philosophers of mathematics find the prospect appealing that only countable objects exist, and this model is a very natural realm for exploring that view.

More generally $H_{\kappa^+}$ for any cardinal $\kappa$ is a model of $\ZFCm$.

But you want the axiom of constructibility. In this case, $L_{\omega_1}$ is a very natural model of your theory, and this model is highly studied in set theory. We build the constructible universe up to $\omega_1$ and then call it a day. This is the same, of course, as $H_{\omega_1}^L$, the hereditarily countable sets of the constructible universe.

Theorem.

1. (Levy absoluteness) Every $\Sigma_1$ assertion in set theory is absolute between $V$ and $L_{\omega_1}$.

2. (Schoenfield absoluteness) Every $\Sigma^1_2$ assertion in descriptive set theory (about the reals) is absolute between $V$ and $L_{\omega_1}$.

What this shows is that certain kinds of mathematical statements will get the same value in the full set-theoretic universe as they do in $L_{\omega_1}$. One interesting example is that this smaller universe has transitive models of all the same large cardinal theories that $V$ does. Even though supercompact cardinals, for example, are inconsistent with $V=L$, nevertheless if there is a transitive model of ZFC with a supercompact cardinal, then there is one in $L_{\omega_1}$.

Another interesting theorem is the Barwise extension theorem.

Theorem. (Barwise extension theorem) Every countable model $M\models\text{ZF}$ has an end-extension to a model $M\subseteq_e N$ to a model of $N\models \text{ZFC}+V=L$.

In fact, the elements of $M$ all become countable in $N$, and so we also get $M$ end-extended by $L_{\omega_1}^N$, which is a model of your theory. In other words:

Corollary. Every countable model of ZF has an end-extension to a model of your theory.