= Simple typed set theory with atoms
{title2=$\mathrm{TSTU}$}
Objects have sorts $0,1,\ldots$, with membership allowed only from sort $i$ to sort $i+1$. A set predicate distinguishes sets from atoms; atoms have no members, extensionality applies to sets, and every well-typed formula defines a set in the next sort by comprehension. First-order models may have only a specified collection of subsets, as in <Henkin semantics>. For a full finite-type model, take $D_i=V_{r_i}$ at widely separated increasing ranks, represent sets at level $i+1$ by $\mathcal P(D_i)\subseteq D_{i+1}$, and treat the remaining objects as atoms under typed membership.
Back to article page
