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
- Shielding from the famous set theoretical paradoxes
- ${\mathfrak U}_\mathrm{Sets}$ in the object language, which easily lets one define a category of sets, Set.
Predicates
predicate | $X$… small set $\equiv X\in{\mathfrak U}_\mathrm{Sets}$ |