Proper classes in Bounded Zermelo set theory

I want to know if there is a standard terminology for this among set theorists working with element-based set theories like ZFC. I will follow the convention that a class in any given set theory is a definable class--it is all the sets that have some property $$\phi(x)$$ expressible in the theory. So it is generally not a legitimate entity in the theory, but we can talk about it in the theory.

Then I call a class a proper class if it is not coextensive with any set. In ZFC that is well expressed by saying a proper class is too big to be a set. But that already fails in Zermelo set theory. Zermelo set theory has a definable class of all finitely iterated power sets of the natural numbers, which is not provably a set but is provably countable. In Zermelo set theory we can still say a proper class is a class not contained in any set (since the axiom scheme of separation says the intersection of any class with a set is a set).

The matter is yet more complex in Bounded Zermelo set theory, where the separation axiom scheme only holds for defining conditions wilh all quantifiers bounded. In this theory a definable subclass of a set need not be a set. For example Bounded Zermelo set theory can define the class of all natural numbers $$n$$ such that there exists an $$n$$-th iterated power set of the natural numbers. But it cannot prove this class is a set. (See: A.R.D. Mathias, The Strength of Mac Lane Set Theory, Annals of Pure and Applied Logic 110 (2001) 107–234 doi:10.1016/S0168-0072(00)00031-2)

So definable class in Bounded Zermelo can be too complex to be a set (in the sense of quantifier complexity) even when it is contained in some set. But do people in the field use some other term than "too complex"?

• And $Z$ (which contains the separation schema) cannot prove that set exists.. In particular $V_{\omega+\omega}$ models $Z$ and does not contain the set $\{ \mathcal{P}^n(\omega): n\in \omega\}$ – Not Mike Jan 6 at 23:54
• @NotMike The language of $Z$ certainly can express: "$X$ is the last entry in some length $n$ sequence of sets where the first entry is $\omega$ and each successive entry is the power set of the one before." And $Z$ proves there are such sequences for every $n\in \mathbb{N}$. Again, of course, it does not prove there is one set of all of them. – Colin McLarty Jan 7 at 4:03
• @NotMike Good point. Luckily i am not asking for a formula describing the union of the class, just describing the class. – Colin McLarty Jan 7 at 5:23
• @NotMike The class $\{\mathcal{P}^n(\omega)\mid n\in \omega\}$ is defined by the following formula $\varphi(x)$: There exists $f$ such that $f$ is a function, $\text{dom}(f) \in \omega\setminus \{0\}$, $f(0) = \omega$, $f(\text{dom}(f)-1) = x$, and for all $n< \text{dom}(f)-1$, $f(n+1) = \mathcal{P}(f(n))$. – Alex Kruckman Jan 7 at 5:30
• I don't know if it is used by bounded Zermelo people, but in some circles, subclasses of sets are called semisets. – Emil Jeřábek Jan 7 at 12:09