= New Foundations with urelements
{c}
{title2=$\mathsf{NFU}$}
= NFU
{c}
{synonym}
NFU has a universal domain, a predicate $S$ distinguishing sets from atoms, extensionality restricted to sets, and comprehension for <stratified formulas>. Atoms have no members. Every stratified predicate has a set extension, including the always-false predicate, so there is a distinguished empty set even when atoms exist. Permitting atoms removes the full-extensionality obstacle in <New Foundations>.
Back to article page
