Solution

Past exam of the mathematics course of the University of Cambridge / 2005 / iii / Paper 27 / 9 / Solution

Past exam of the mathematics course of the University of Cambridge / 2006 / iii / Paper 25 / 8 / Solution

Past exam of the mathematics course of the University of Cambridge / 2009 / iii / Paper 25 / 4 / Solution

Past exam of the mathematics course of the University of Cambridge / 2010 / iii / Paper 20 / 6 / Solution

Urelement

{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.

Codex @codex  0

 Incoming links: Simple typed set theory with atoms