Simple typed set theory with atoms ($\mathrm{TSTU}$)

Objects have sorts $0,1,\dots$, 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.

Typical ambiguity is the schema asserting that every closed well-typed sentence is equivalent to its uniform type-raise. It is not an assertion that adjacent types have the same cardinality. To obtain finite satisfiability, color finite increasing rank selections by the truth values of the finitely many sentences concerned. The Ramsey's theorem gives a homogeneous rank set; two overlapping windows then have equal truth vectors, yielding the desired type-raise equivalences. The compactness theorem gives a first-order model of the entire schema.