Local theory of sets as a foundation for category theory and its connection with the Zermelo-Fraenkel set theory (Q2462035)

In [``Locally small categories and the foundations of set theory,'' in: Infinitistic methods. Proc. Symp. Foundations Math., Warsaw 1959, 25--43 (1961; Zbl 0116.00902)], \textit{S. MacLane} posed the ``general problem of constructing a new and more flexible axiomatic set theory that could serve as an adequate logical foundation for naive category theory.'' The present paper addresses that problem via the local theory of sets (LTS), a first-order axiomatic framework in which one may express such notions as the ``category of all categories,'' etc., in a relatively consistent way. The approach assumes no formal mathematical logic on the part of the reader, and this makes the paper more accessible to advanced students and nonlogicians who care about foundational issues. The main results are: (1) that ``proper class'' notions of category theory -- functor categories, the category of all categories -- are formalizable, to a limited extent, within LTS; and (2) that LTS is equiconsistent with Zermelo-Fraenkel set theory (ZF). Here is a brief description of LTS: While the alphabet of ZF has the binary predicates of membership (\(\in\)) and equality (\(=\)) as its only nonlogical symbols, the alphabet of LTS adds to these the unary predicate of universality (\(\bowtie\)), and the constants empty set (\(\emptyset\)) and infra-universe (\(\mathfrak a\)). (These symbols are actually definable within the confines of ZF; and ultimately, after suitable explicative LTS axioms are provided, serve as abbreviations.) Elements of any model of LTS are called classes. A class is a universe if each of its elements is also a subclass. (This definition serves to explicate the predicate symbol \(\bowtie\).) When class \(A\) is a member of class \(B\), \(A\) is called a \(B\)-set. Every class is postulated to be a \(U\)-set for some universe \(U\); the constant \(\mathfrak a\) refers to the (unique) universe that is a subclass of every universe. The idea is that every notion from ``usual'' mathematics may be formalized within the infra-universe \(\mathfrak a\), but that certain ``illicit'' formulations -- in the sense of ZF -- need a hierarchy of universal classes to be made intelligible. This is, of course, a brand of type theory: One postulates the notion of \(\alpha\)-category, where all objects and arrows are \(\alpha\)-sets for a universal class \(\alpha\); then the category of all \(\alpha\)-categories is a \(\beta\)-category for suitable universe \(\beta\) containing \(\alpha\) as one of its elements. [Reviewer's comment: This is a notation-rich paper, and the reader should be on the lookout for minor typos: for example, on line 9 of page 5768, the symbol \(\equiv\) is introduced as abbreviation for the biconditional. This symbol is never used again in that capacity; rather it appears frequently later on to indicate equality in the meta-language.]