# Can ZFC + Classes + definability rule manage to prove all classes countable?

Working in bi-sorted $$L_{\omega_1,\omega} (=, \in)$$, if we write $$\sf ZFC + Classes$$ as it is; i.e., in bi-sorted $$L_{\omega, \omega} (=,\in)$$, and add the following definability rule written in bi-sorted $$L_{\omega_1,\omega} (=, \in)$$ :

Definability rule: if $$\phi_1,\phi_2,\phi_3,...$$ are all formulas in bi-sorted $$L_{\omega,\omega}(=,\in)$$, in which only symbol "$$y$$" occurs free, and it never occurs bound, then: $$\forall X: \bigvee_{i \in \mathbb N} X=\{y \mid \phi_i\}$$ This would ensure that all classes are pointwise definable in bi-sorted $$L_{\omega,\omega}(=,\in)$$

Would "$$\sf ZFC + Classes + Definability \ rule$$", manage to prove that all classes are countable?

• But there are uncountably many formulas in $L_{\omega_1,\omega}$. Dec 26, 2022 at 21:55
• @JoelDavidHamkins, all classes here are pointwise definable in $L_{w,w}(=,\in)$, which has countably many formulas. Dec 26, 2022 at 22:00
• Ah, I see now what you intend. Dec 26, 2022 at 22:01

Since I don't have a good understanding of your Classes axiom/theory, let me answer instead for Gödel-Bernays set theory GBC, for which the answer is negative.

We know that there are pointwise definable models of GBC, and every such model will satisfy your definability axiom, since every class there is definable. But none of these models think that every set or class is countable.

The main explanation is that merely knowing that every class is definable is not sufficient to build the definability map $$\text{class }X\quad\to\quad\text{defining formula }\phi.$$ It is this map and not the pointwise definability itself that leads to the conclusion that there are only countably many classes.

We discuss this issue at length in our paper:

But I am unsure how much of this analysis applies to your theory Classes.

• Both MK and GBC are not compatible with all classes being countable because $V$ is provably uncountable in them! Actually $V$ is provably inaccessible. This is a consequence of the axiom of limitation of size. And even its weaker version stating that the range of every class partial function from a set is a set is still powerful enough to prove that $V$ is uncountable. With ZFC + Classes we don't have that. Dec 27, 2022 at 0:50
• Yes, I know all that. My point was that the definability property doesn't in general imply countability. Dec 27, 2022 at 1:06
• Ah! I see, Nice! Dec 27, 2022 at 1:08
• I thought the stronger logic background used here may make such a proof possible? Dec 27, 2022 at 1:12