New Foundations with Urelements (NFU) is a theory that extends Quine’s original theory (New Foundations) by adding “urelements” (atoms). It was discovered by Jensen in 1969, who proved that NFU is relatively consistent with Peano arithmetic and consequently with Zermelo–Fraenkel set theory (ZF). Jensen’s proof is rather hard to follow, so Boffa introduced a more straightforward method of constructing models for NFU from a model of ZF. However, Boffa’s presentation of his construction is extremely terse with many essential details omitted, since he probably only wanted to emphasize the differences from Jensen’s construction. Our main goal is to elaborate on this construction in great detail, and also to prove that the said construction yields some results that are either not present in the contemporary literature, or are accepted as true at face value. Namely, besides proving that this construction gives a model for NFU, we will also use it to define models for NFU with the Axiom of Infinity, NFU with the Axiom of Choice, and NFU with both of those axioms.
