A local two-sorted theory of classes and sets: MacLane's problem and Mostowski's program (Q1780370)

The well-known theories ZF and NBG, with the axiom of choice, are adequate for all of modern mathematics except category theory. Category theorists have proposed a host of theories aimed at filling this gap, but none of them turned out to be completely satisfactory. In the paper under review, the authors claim to have largely solved the problem with a more inclusive theory of sets and classes in a language that allows reference to formulas of the theory itself. The basic language and axioms describe the `totality of local two-sorted object-propositional universes \(\mathfrak{A}\)'. Proofs are provided for some of the simpler results. Enough seems to be said to indicate that ZF and NBG are obtainable. Finally, the authors outline how what might be called `naive category theory' can be embedded in the new theory. Speaking roughly, we can define the constructions `category of categories' and `category of functors from one \(\mathfrak{A}\)-category into another \(\mathfrak{A}\)-category'. Some other advantages claimed for the new approach are: (i) there are no cardinality constraints on objects, (ii) one can easily define the notions of `indexed \(\mathfrak{A}\)-category' and `fibered \(\mathfrak{A}\)-category'; (iii) various categories important in mathematical logic can be dealt with (as an illustration, the category of all propositional formulas of the theory and all inferences between them is treated in detail).