Finite Axiomatizability of Local Set Theory

The need for modifying axiomatic set theories was caused, in particular, by the development of category theory. The $\mathrm{ZF}$ and $\mathrm{NBG}$ axiomatic theories turned out to be unsuitable for defining the notion of a model of category theory. The point is that there are constructions such as the category of categories in naïve category theory, while constructions like the set of sets are strongly restricted in the $\mathrm{ZF}$ and $\mathrm{NBG}$ axiomatic theories. Thus, it was required, on the one hand, to restrict constructions similar to the category of categories and, on the other hand, adapt axiomatic set theory in order to give a definition of a category which survives restricted construction similar to the category of categories. This task was accomplished by promptly inventing the axiom of universality ($\mathrm{AU}$) asserting that each set is an element of a universal set closed under all $\mathrm{NBG}$ constructions. Unfortunately, in the theories $\mathrm{ZF}+\mathrm{AU}$ and $\mathrm{NBG}+\mathrm{AU}$, there are too many universal sets (as many as the number of all ordinals), whereas to solve the problem stated above, a countable collection of universal sets would suffice. For this reason, in 2005, the first-named author introduced local-minimal set theory, which preserves the axiom $\mathrm{AU}$ of universality and has an at most countable collection of universal sets. This was achieved at the expense of rejecting the global replacement axiom and using the local replacement axiom for each universal class instead. Local-minimal set theory has 14 axioms and one axiom scheme (of comprehension). It is shown that this axiom scheme can be replaced by finitely many axioms that are special cases of the comprehension scheme. The proof follows Bernays' scheme with significant modifications required by the presence of the restricted predicativity condition on the formula in the comprehension axiom scheme.