Set universe

Collection

definiendum ${\mathfrak U}_\mathrm{Sets}$ in it
postulate ${\mathfrak U}_\mathrm{Sets}$ … Grothendieck universe
postulate $\omega_{\mathcal N}\subseteq {\mathfrak U}_\mathrm{Sets}$

Discussion

A set universe ${\mathfrak U}_\mathrm{Sets}$ is a Grothendieck universe containing all sets generated by the first infinite von Neumann ordinal $\omega_{\mathcal N}$. It contains a model for the natural numbers, their powerset, the powersets of those etc. etc. I didn't specify what's not in such a universe, but for doing “normal non-foundational mathematics”, one hardly ever needs anything that goes beyond a set obtained by a finite number of iterations of the applications of the power set operation on $\omega_{\mathcal N}$.

In set theory, the Tarski axiom states that there is a Grothendieck universe for every set. Note that this axiom implies the existence of strongly inaccessible cardinals and goes beyond ZFC.

Motivation

When one writes down a proposition in set theory, e.g.

$\forall x.\exists y.\,P(x,y)$,

where $P$ is some 2-ary predicate, then the quantifiers range over the whole logical domain of discourse ${\mathfrak D}_\mathrm{Sets}$, see Sets. For most mathematics one can instead restrict oneself to some very large set, like ${\mathfrak U}_\mathrm{Sets}$, and only consider propositions with quantifiers over bounded domains

$\forall (x\in{\mathfrak U}_\mathrm{Sets}).\exists (y\in{\mathfrak U}_\mathrm{Sets}).\,P(x,y)$.

The advantages are

Predicates

predicate $X$… small set $\equiv X\in{\mathfrak U}_\mathrm{Sets}$

Requirements

Grothendieck universe, First infinite von Neumann ordinal