===== Set universe =====
==== Collection ====
| @#FFBB00: definiendum | @#FFBB00: ${\mathfrak U}_\mathrm{Sets}$ in it |
| @#55EE55: postulate   | @#55EE55: ${\mathfrak U}_\mathrm{Sets}$ ... Grothendieck universe |
| @#55EE55: postulate   | @#55EE55: $\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 ===
| @#EEEE55: predicate | @#EEEE55: $X$... small set $\equiv X\in{\mathfrak U}_\mathrm{Sets}$ |

-----
=== Requirements ===
[[Grothendieck universe]], [[First infinite von Neumann ordinal]]