Paul Gorbow: Algebraic Set Theory for NF and some of its variants

Abstract: NFU is a set theory allowing for atoms, axiomatized as stratified comprehension + extensionality for sets + infinity. Any model of ZF that admits a non-trivial automorphism, may be turned into a model of NFU, by a simple reinterpretation of membership. NF is NFU + everything is a set. INF(U) is intuitionistic NF(U).  In this presentation we give theories in the language of categories equiconsistent to each of (I)NF(U).

Just as the theory of topoi generalizes set theory, the theory of categories of classes generalizes class theory. This is essentially a first order theory in the language of categories augmented with a predicate that distinguishes between small and large objects and morphisms. The restriction of a category of classes to its small objects and morphisms, is a topos; and conversely, any topos embeds as the small objects and morphisms in a category of classes. Categories of classes facilitate direct interpretation of traditional set theory. For example, Awodey et al. (2014), used them to interpret Basic Intuitionistic Set Theory (BIST).

We focus on presenting the theory HC + PT in the language of categories augmented with a predicate distinguishing between homogeneous and non-homogeneous morphisms, and we show that it is equiconsistent to INFU. The subcategory of homogeneous morphisms stands in the analogous relation to INFU as a topos stands to BIST. (Moreover, it has a natural subcategory of “Cantorian” objects, which is a topos.) The argument is easily modified for (I)NF(U). As a corollary, we obtain a new proof of Con(NF) iff Con(NFU + |V| = |P(V)|).