Äîêóìåíò âçÿò èç êýøà ïîèñêîâîé ìàøèíû. Àäðåñ îðèãèíàëüíîãî äîêóìåíòà : http://halgebra.math.msu.su/wiki/lib/exe/fetch.php/staff:bunina:fulltext1.pdf Äàòà èçìåíåíèÿ: Wed Feb 13 11:26:38 2013 Äàòà èíäåêñèðîâàíèÿ: Sun Apr 10 00:10:00 2016 Êîäèðîâêà: IBM-866 Ïîèñêîâûå ñëîâà: transit

Journal of Mathematical Sciences, Vol. 138, No. 4, 2006

LOCAL THEORY OF SETS AS A FOUNDATION FOR CATEGORY THEORY AND ITS CONNECTION WITH THE ZERMELOíFRAENKEL SET THEORY V. K. Zakharov, E. I. Bunina, A. V. Mikhalev, and P. V. Andreev UDC 510.223, 512.581

CONTENTS Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1. First-Order Theories and LTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.1. Language of first-order theories . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.2. Deducibility in a first-order theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1.3. An interpretation of a first-order theory in a set theory . . . . . . . . . . . . . . . . . . . 2. Local Theory of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2.1. Proper axioms and axiom schemes of the local theory of sets . . . . . . . . . . . . . . . . 2.2. Some constructions in the local theory of sets . . . . . . . . . . . . . . . . . . . . . . . . 3. Formalization of the Naive Category Theory within the Framework of the Local Theory of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.1. Definition of a local category in the local theory of sets . . . . . . . . . . . . . . . . . . . 3.2. Functors and natural transformations and the "category of categories" and the "category of functors" in the local theory of sets generated by them . . . . . . . . . . . . . . . . . . 4. ZermeloíFraenkel Set Theory and Mirimanovívon Neumann Sets . . . . . . . . . . . . . . . . 4.1. The proper axioms and axiom schemes of the ZF set theory . . . . . . . . . . . . . . . . 4.2. Ordinals and cardinals in the ZF set theory . . . . . . . . . . . . . . . . . . . . . . . . . 4.3. Mirimanovívon Neumann sets in the ZF set theory . . . . . . . . . . . . . . . . . . . . . 5. Universes, Ordinals, Cardinals, and Mirimanovívon Neumann Classes in the Local Theory of Sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.1. The relativization of formulas of the LTS to universal classes. The interpretation of the ZF set theory in universal classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2. The globalization of local constructions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.3. Ordinals and cardinals in the local theory of sets . . . . . . . . . . . . . . . . . . . . . . 5.4. Mirimanovívon Neumann classes in the local theory of sets and their connection with universal classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.5. The structure of the assemblies of all universal classes and all inaccessible cardinals in the local theory of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6. Relative Consistency between LTS and the ZF Theory . . . . . . . . . . . . . . . . . . . . . . 6.1. Additional axioms on inaccessible cardinals in the ZF theory . . . . . . . . . . . . . . . . 6.2. "Forks" of relative consistency . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7. Proof of Relative Consistency by the Method of Abstract Interpretation . . . . . . . . . . . . 7.1. Abstracts of a set theory . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.2. The abstract interpretation of a first-order theory in a set theory . . . . . . . . . . . . . 8. Undeducibility of Some Axioms in LTS . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8.1. The undeducibility of the axiom scheme of replacement . . . . . . . . . . . . . . . . . . . 5764 5767 5767 5768 5770 5772 5772 5775 5776 5776 5777 5779 5779 5782 5786 5791 5791 5793 5795 5798 5801 5803 5803 5807 5816 5816 5817 5818 5818

Translated from Itogi Nauki i Tekhniki, Seriya Sovremennaya Matematika i Ee Prilozheniya. Tematicheskie Obzory. Vol. 119, Set Theory, 2004. 1072í3374/06/1384í5763 c 2006 Springer Science+Business Media, Inc. 5763


8.2. The nondependence of axiom ICU on the axioms of the LTS . . . . . . . . . . . . . . . . 5826 8.3. Locally-minimal theory of sets . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5827 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5828

Intro duction The crises that arose in naive set theory at the beginning of the 20th century brought to the fore some strict axiomatic constructions of theories of mathematical totalities. The most widely used of them are the theory of sets in ZermeloíFraenkel's axiomatics (ZF) (see [23]) and the theory of classes and sets in von NeumanníBernaysíGè odel's axiomatics (NBG) (see [20] and [28]). These axiomatic theories eliminated all the known paradoxes of naive set theory at the expense of a sharp restriction on possible expressive means. At the same time, they provided an opportunity to include almost all the then existing mathematical ob jects and constructions within the framework of these theories. In 1945, a new mathematical notion of category was introduced by Eilenberg and MacLane in the initial paper [11]. From that time, category theory became an independent field of mathematics. But from the very beginning of its origin, category theory encountered the unpleasant circumstance that it did not fall not only within the framework of the theory of sets in ZermeloíFraenkel's axiomatics but even within the framework of the theory of classes and sets in von NeumanníBernaysíGè odel's axiomatics (NBG) (see [11]). For this reason, in 1959, in the paper [25], MacLane pose the general problem of constructing a new and more flexible axiomatic set theory that could serve as an adequate logical foundation for the whole naive category theory. Different variants of new axiomatic theories of mathematical totalities, adjusted for one or another need of category theory, were proposed by Ehresmann [10], Dedecker [9], Sonner [29], Grothendieck [14], da Costa ([6] and [7]), Isbell [18], MacLane ([26] and [27]), Feferman [12], Herrlich and Strecker [17], and others. Ehresmann, Dedecker, Sonner, and Grothendieck introduced an important notion of (categorical) universe U , i. e., a totality of ob jects which satisfies the following properties of closedness: (1) (2) (3) (4) (5) X X X, Y X U X U (EhresmanníDedecker did not propose this property); U P (X ), X U ; U X Y, {X, Y }, X, Y ,X ½ Y U ; U (F U X ) rng F U ; U ( = {0, 1, 2,... } is here the set of all finite ordinal numbers).

Within the framework of such a universe, it is possible to develop a quite rich category theory, in particular, the theory of categories with direct and inverse limits. To satisfy all needs of category theory, these authors proposed to strengthen the ZF or NBG set theories by the strong universality axiom postulating that every set belongs to some universal set. In MacLane's axiomatics, the existence of at least one universal set is postulated. Similar versions were proposed by Isbell and Feferman. HerlichíSrecker's axiomatics dealt with ob jects of three types: sets, classes, and conglomerations. Within the framework of each of these axiomatics, some definitions of category and functor are given. But the notions of category given in [12, 17, 18, 26, 27] are not closed with respect to such important operations of naive category theory as the "category of categories" and the "category of functors" (see [16], 8.4). Within the framework of the axiomatic theories [9, 10, 14, 29] the definition of U -category, U -functor, and natural U -tranformation consisting of subsets of a universal set U is given. This notion of category is closed with respect to such operations as the V -category of U -categories and the V -category of U -functors, where V is some universal set containing the universal set U as an element. 5764


The axiomatics from [6] and [7] also give definitions of a category and a functor closed under the mentioned operations of naive category theory. But da Costa uses the logic with the nonconstructive rule of deduction (V1 ), (V2 ), (V3 ), § § § t(t), where V1 ,V2 ,...,Vn ,... is an infinite sequence of constants, which denotes universes like the NBG-universe (see [7]). In connection with the logical difficulties of conctructing a set-theoretical foundation for the whole naive category theory, different attempts to construct purely arrow-axiomatic foundations were undertaken (see Lawvere [24], Blanc and Preller [2], and Blanc and Donadieux [3]). But in attempts at an arrowaxiomatic description of indexed categories and fiber categories, their own logical difficulties appeared (see [16], 8.4). Now let us consider more precisely what the formulation of MacLane's problem mentioned above means. To do this, we need to have a strict definition of category. This definition became possible after the elementary ( first-order) category theories Tc took shape. There are many such theories, two-sorted and one-sorted (see, for example, [27, I.3, I.8], [16, 8.2], [30, 2.3, 11.1]). But for every set theory S , there exist canonical one-to-one correspondences between the totalities of models of these theories in the theory S . Therefore, for the strict definition of a category one can use any elementary theory Tc . According to the definition of Lawvere [24] (see also [16, 8.2]), a category in some set theory S is any model of the theory Tc in the S theory (see 1.3 below). The complete (partial) formalization of naive category theory C in the set theory S is an adequate translation of all (some) notions and constructions of naive category theory C into strict notions and constructions for categories (as models of the theory Tc ) in the set theory S . Along with the notion of a category in the set theory S , there also exists the notion of abstract category in S . An abstract category in the set theory S is any abstract model of the theory Tc in the set theory S (see 7.1. below). The complete (partial) abstract formalization of naive category theory C in the set theory S is an adequate translation of all (some) notions and constructions of naive category theory C into strict notions and constructions for abstract categories (as abstract models of the theory Tc ) in the S set theory. According to these definitions abstract categories in the ZF set theory can be considered also on classes (as abstracts of the ZF theory), and abstract categories in the NBG set theory can be considered also on assemblies (as abstracts of the NBG theory). However, the complete abstract formalization of naive category theory C in any S set theory is impossible, because it is impossible to take abstracts of abstracts. Only a partial abstract formalization of C in S is possible. This means that the notions of an abstract category in S and a partial abstract formalization of C in S have only an auxiliary significance with respect to the notions of a category in S and the complete formalization of C in S . Therefore, more precisely MacLane's problem is understood as constructing a set theory that admits a complete formalization of naive category theory C in this set theory. According to the definitions mentioned above, categories in the ZF set theory can be considered only on sets, but categories in the NBG set theory can be considered also on classes. But a complete formalization of naive category theory C in these set theories is impossible, because it is impossible to define the operations "category of categories" and "category of functors" (at least nowadays, we have no methods of approash to this formalization). For this reason, Ehresman, Dedecker, Sonner, and Grothendieck proposed the idea of formalization of naive category theory C within the framework of a ZF+U set theory stronger than the ZF set theory with the axiom of universality U. Using the totality of universal sets, we can make a complete and adequate translation of all notions and constructions of naive theory C to the strict notions and constructions for categories in the ZF+U set theory. This also holds for the sets theories of da Costa. For the other mentioned set theories such a complete translation is impossible. Therefore, the ZF+U set theory and the set theories of da Costa are the most adequate with respect to MacLane's problem. Moreover, in virtue of the deficiency of da Costa's set theories mentioned above, the ZF+U set theory is preferred. However the ZF+U theory is too strong for a complete formalization of category theory in virtue of the redundancy of the totality of all universal sets, because for formalization of the operations "category 5765


of categories" and "category of functors", it is sufficient to have only a countable totality of universal sets as is done in da Costa's axiomatics. The ZF+U( ) theory with the axiom of -universality U( ) postulating the existence of an infinite totality of universal sets is weaker than ZF+U and satisfies all the needs of the theory C . But it leaves behind the limits of categorical consideration such mathematical systems that are not elements of universal sets from this infinite totality. Therefore, there arises a necessity to create a set theory S having an infinite totality U of some ob jects of the theory S , called universes and satisfying the following conditions: (1) S must be in some sense weaker than the redundant ZF+U theory; (2) S must satisfy all the needs of the theory C to such an extent as the ZF+U( ) theory does; (3) Contrary to ZF+U( ), the theory S must have ob jects occurring outside of the totality of universes U. In 2000, V. K. Zakharov proposed the local theory of sets (LTS) in the capacity of a more adequate foundation of category theory satisfying all these conditions (see anouncements in [30] and [1]), and in 2003, he proposed its equiconsistent strengthening: the local ly-minimal theory of sets (LMTS). The main idea of LTS and LMTS is that for the construction of a set theory with properties (1)í(3) it is not necessary to assign a global set-theoretical structure, but it is sufficient to assign only local variants of this structure in each universe U. The local theory of sets tries to maintain all positive that is contained in the globally-internal concept of EhresmanníDedeckeríSonneríGrothendieck. The locally-external ideology of LTS is that it is necessary to take the NBG-universe as the basic one and external ly duplicate its local copies, therefore, to obtain some hierarchy of universes with the following properties: (1) every class belongs as a set to some universal class, which is the usual NBG-universe; (2) all subclasses of a given universal class are sets of any larger universal class (property of value change ); (3) there exists the least universal class ( the infra-universe ) belonging to all other universal classes. The first of these properties is similar to the axiom of universality mentioned above. Thus, in the LTS, the notion of a large totality becomes relative: totalities that are "large " in one universe become "smal l " in any larger universe. The first section of the given paper describes the structure of an arbitrary first-order theory (including LTS) and contains necessary notions from mathematical logic (see [28]). In the second section, all proper axioms and axiom schemes of LTS are stated and the important set-theoretical constructions are defined. In the third section, in LTS such key categorical constructions as the "category of categories" and the "category of functors" is formalized. As in the globally-internal concept here, all categorical notions and consructions are defined only within the framework of local NBG-universes. Therefore, the categories under consideration are said to be local. In the fourth section, the proper axioms and axiom schemes of the ZF theory (ZermeloíFraenkel with the choice axiom) are cited, the notions of ordinals, cardinals, and inaccessible cardinals are introduced, and properties of Mirimanovívon Neumann sets are studied. In the fifth section, the notions of ordinals, cardinals, and inaccessible cardinals in LTS are introduced, Mirimanovívon Neumann classes are constructed, and the connection between the universal classes and the Mirimanovívon Neumann classes with indices that are inaccessible cardinals is stated. By means of this, it is proved that the assembly of all universal classes in the LTS is well-ordered with respect to the order by inclusion U V , and also its structure is investigated. Here, for the assembly of all classes ( globalization ), we also define almost all local set-theoretical constructions, except for the most important construction of the full union, which is basic for the construction by transfinite induction. 5766


In the sixth section, the relative consistency between LTS and the ZF theory with some additional axioms is stated. Finally, the independence of the introduced additional axioms and the undeducibility in the LTS of the global axiom scheme of replacement are stated. For the reader's converjence, this paper contains all the necessary notions. Proofs are given in detail, so that they can be useful for young mathematicians. The authors are very thankful to S. I. Adyan, N. K. Vereschagin, A. G. Vladimirov, P. V. Golubtsov, V. G. Kanovey, V. A. Lyubetskiy, N. N. Nepejvoda, M. A. Pentus, V. A. Uspensky, and A. D. Yashin for their interest in this work and for a series of valuable consultations. 1. First-Order Theories and LTS

1.1. Language of first-order theories. The proposed theory is a first-order theory. We will give the definition of a first-order theory based on [28]. Special symbols of every first-order theory T are the following symbols: parentheses (, ); connectives ("implies") and ì ("not"); quantifier (for all); a countable set of variables vi (i 0) (in our case, the variables are denoted by the letters x, X , y , Y , z , Z , u, U , v , V , w, W , and also these letters with primes); a nonempty countable set of predicate letters Pin (n 1, i 0) (LTS contains the unary predicate symbol and the binary symbol ); a countable set of functional letters Fin (n 1, i 0) (in LTS, this set is empty); finally, a countable set of constants ai (i 0) (in LTS, this set consists of symbols and a). General symbols are symbols that are not special but are often used in mathematics. The special and general symbols compose the initial alphabet. A symbol-string is defined by induction in the following way: (1) every symbol of the initial alphabet, except for the blank-symbol, is a symbol-string ; (2) if and are symbol-strings, then and are symbol-strings. A designating ( shortening ) symbol-string for a symbol-string is introduced in the form of the symbol-string or ( is a designation for ). If a symbol-string is a part of a symbol-string staying at one of the following three positions: ..., ... , ...... , then is an occurrence in ( occurs in ). A text is defined by induction in the following way: (1) every symbol-string is a text; (2) if and are texts, then and are texts. If a text is a part of a text staying at one of the following three positions: ... , ... , ... ... , then is an occurrence in ( occures in ). Some symbol-strings constructed from the special symbols mentioned above are called terms and formulas of the first-order theory T . Terms are defined in the following way: (1) a variable is a term ; (2) a constant symbol is a term ; (3) if Fin is an n-placed functional letter and t0 ,...,tn-1 are terms, then Fin (t0 ,...,tn-1 ) is a term ; (4) a symbol-string is a term if and only if it follows from rules (1)í(3). In the LTS theory, because of lack of functional symbols, terms are constant symbols and variables. If Pin is some n-placed predicate letter and t0 ,...,tn-1 are terms, then the symbol-string Pin (t0 ,...,tn-1 ) is called an elementary formula. 5767


Formulas of the first-order theory T are defined in the following way: (1) every elementary formula is a formula ; (2) if and are formulas and v is a variable, then every symbol-string (ì), ( ), and v () is a formula ; (3) a symbol-string is a formula if and only if it follows from rules (1) and (2). Let introduce the following abbrevations: ( ) for ì( ì ); ( ) for (ì) ; ( ) for ( ) ( ); v is an abbrevation for (ì(v (ì))). Introduce the notion of free and connected occurrence of a variable in a formula. An occurrence of a variable v in a given formula is said to be connected if v is either a variable of the quantifier v occurring in this formula or is under the action of the quantifier v occurring in this formula; otherwise an occurrence of a variable in a given formula is said to be free. Thus, one variable can have free and connected occurrences in the same formula. A variable is said to be a free (connected ) variable in a given formula if there exist free (connected) occurrences of this variable in this formula, i. e., a variable can be free and connected in one formula at the same time. A sentence is a formula with no free variables. If is a term or a formula, is a term, and v is a variable, then (v ) denotes a symbol-string obtained by replacing every free occurrence of the variable v in the symbol-string by the symbol-string . The substitution v in is said to be admissible if for every free occurrence of a variable w in the symbol-string , every free occurrence v in is not a free occurrence in some formula occurring in some formulas w (w) and w (w) occurring in the symbol-string . In the sequel, if the substitution v in is admissible, then, along with (v ), we will write (). If is a term or a formula, is a term, and v is a variable such that the substitution v in is admissible, then the substitution (v ) is a term or a formula, respectively. Every free occurrence of some variable u (except for v ) in a symbol-string and every free occurrence of some variable w in a symbol-string are free occurrences of these variables in the symbol-string (v ). 1.2. Deducibility in a first-order theory. A symbol-string equipped with some rule is called a formula scheme of a theory T , if: (1) this rule marks some letters (in particular, free and connected variables) occurring in ; (2) this rule determines the necessary substitution of these marked letters in by some terms (particularly variables); (3) after every such a substitution in , some propositional formula of the theory T is obtained. Every such a propositional formula is called a propositional formula obtained by the application of the formula scheme . A text consisting of symbol-strings separated by blank-symbols is called an axiom text if every symbol-string occurring in is either a formula or a formula scheme of the theory T . If is a formula, then is called an explicit axiom of the theory T . If is a formula scheme, then it is called an axiom scheme of the theory T . Every formula obtained by the application of the axiom scheme is called an implicit axiom of the theory T . Axioms and axiom schemes of every (in particular, the LTS) first-order theory are divided into two classes: logical and proper (or mathematical ). Logical axiom schemes of any first-order theory are cited below: LAS1. LAS2. LAS3. LAS4. 5768 ( ); ( ( )) (( ) ( )); ( ) ; ( ) ;


LAS5. ( ( )); LAS6. ( ); LAS7. ( ); LAS8. ( ) (( ) (( ) )); LAS9. ( ) (( ì ) ì); LAS10. (ì(ì)) ; LAS11. (v) (v ) if v is a variable and is a term such that the substitution v in is admissible. LAS12. (v ) (v) under the same conditions as in LAS11; LAS13. (v ( (v ))) ( (v)) if does not contain a free variable v ; LAS14. (v ((v ) )) ((v) ) under the same condition as in LAS13. Proper axioms and axiom schemes cannot be formulated in the general case because they depend on a theory. The first-order theory which does not contain any proper axioms is called the first-order predicate calculus. Proper axioms and axiom schemes of LTS are stated in the next section. The deduction rules in the first-order theory are as follows: (1) the implication rule ( modus ponens (MP)): from and , it follows that ; (2) the generalization rule (Gen): from , it follows that v. Let be a totality of formulas, and let be a formula of the theory T . A sequence f (i |i n +1) (0 ,...,n ) of formulas of the theory T is called a deduction of the formula from the totality if n = , and for any 0 < i n, one of following conditions holds: (1) i belongs to ; (2) there exist 0 k < j < i such that j is (k i ), i.e., i is obtained from k and k i by the implication rule MP; (3) there exists 0 j < i such that i is xj , where x is not a free variable of every formula from , i.e., i is obtained from j by the generalization rule Gen with the given structural requirement. Denote this deduction either by f (0 ,...,n ) : , or by (0 ,...,n ) : , or by f : . A totality a is called a totality of axioms of the theory T if a consists of all explicit proper axioms of the theory T , all implicit proper axioms of the theory T , and all implicit logical axioms of the predicate calculus. If there exists a deduction f : a , then the formula is said to be deducible in the axiomatic theory (T, a ), and the deduction f is said to be a proof of the formula . A totality of formulas is said to be contradictory ( non-consistent ) if every formula of the theory T is deducible from it. In the opposite case, is said to be noncontradictory ( consistent ). An axiomatic theory (T, a ) is said to be contradictory (noncontradictory ) if the totality of its axioms a is contradictory (noncontradictory). Lemma 1. A totality of formulas is contradictory if and only if the formulas and ì for some sentence are deducible from . Proof. If the totality is contradictory, then every sentence of the theory T is deducible from it, in partcular, and ì for an arbitrary sentence are deducible. Now suppose that sentences and ì are deducible from the totality and is an arbitrary formula. Let us show that the formula can be deduced from and ì. Actually, this is the following deduction: 1. (ì ) (LAS1); 2. ì (ì ì) (LAS1); 3. ; 4. ì; 5. ì (MP, 1, and 3); 6. (ì ) (ì ì) ì(ì )) (LAS9); 7. (ì ì) ì(ì ) (MP, 5, and 6); 5769


8. 9. 10. 11.

ì ì (MP, 2 and 4); ì(ì ) (MP, 7, and 8) (ì(ì )) (LAS10); (MP, 9, and 10).

1.3. An interpretation of a first-order theory in a set theory. The consistency of first-order theories is often proved by the method of interpretations going back to Tarski (see [28]). A first-order theory S is called a set theory if the binary predicate symbol belongs to the set of its predicates symbols. This symbol denotes belonging ( (x, y ) is read as "x belongs to y ," "x is an element of y ," and so on.) Let some ob ject D be shosen by means of the set theory S . This chosen ob ject D of the set theory S is said to be equipped if in S , for all n 1, the notions of n-finite sequence (xi D|i n) of elements of the ob ject D, n-placed relation R Dn , n-placed operation O : Dn D, and also the notion of an infinite sequence x0 ,...,xq ,... of elements of the ob ject D are defined. Let S be some fixed set theory with some fixed equipped ob ject D. An interpretation of a first-order theory T in the set theory S with the equipped object D is a pair M consisting of the ob ject D and some correspondence I that assigns some n-placed operation to every predicate letter Pin relation I (Pin ) in D, to every functional letter Fin some n-placed operation I (Fin ) in D, and to every constant symbol ai some element I (ai ) of D. Let s be an infinite sequence x0 ,...,xq ,... of elements of the ob ject D. Define the value of a term t of the theory T on the sequence s under the interpetation M of the theory T in the set theory S (denoted by tM [s]) by induction in the following way: -- if t vi , then tM [s] xi ; -- if t ai , then tM [s] I (ai ); -- if t F (t0 ,...,tn-1 ), where F is an n-placed functional symbol and t0 ,...,tn-1 are terms, then tM [s] I (F )(t0 M [s],...,tn-1 M [s]). Define the translation of a formula on the sequence s under the interpretation M of the theory T in the set theory S (denoted by M [s]) by induction in the following way: -- if (P (t0 ,...,tn-1 )), where P is an n-placed predicate symbol and t0 ,...,tn-1 are terms, then M [s] ((t0 M [s],...,tn-1 M [s]) I (P )); -- if (ì), then M [s] (ìM [s]); -- if (1 2 ), then M [s] (M 1 [s] M 2 [s]); -- if (vi ), then M [s] (x(x D M [x0 ,...,xi-1 ,x, xi+1 ,...,xq ,... ])). Using the abbriviations cited above, we also have the following: -- if (1 2 ), then M [s] (M 1 [s] M 2 [s]); -- if (1 2 ), then M [s] (M 1 M 2 [s]); -- if (vi ), then M [s] (x(x D M [x0 ,...,xi-1 ,x, xi+1 ,...,xq ,... ])); -- if (1 2 ), then M [s] (M 1 [s] M 2 [s]). If, in the theory S , the symbol-string (s) ((t0 M [s],...,tn-1 M [s]) I (P )) is a formula of the theory S , then this definition implies that M [s] is always a formula of the theory S . Further, in this section we will consider the set theory S for which all symbol-strings (s), are formulas of the theory S for every sequence s from D. All concrete set theories considered later in this paper will possess this property. An interpretation M is called a model of the axiomatic theory (T, a ) in the axiomatic set theory (S, a ) with the chosen equipped object D if for every sequence s from D, the translation M [s] of every axiom of the theory T is a deducible formula in the theory (S, a ). of the formula from the Define now the translation of the deduction f (0 ,...,n ) : totality of formulas of the theory T on the sequence s under the interpretation M of the theory T in 5770


the set theory S in the form of the sequence g (M 0 [s],...,M n [s]), which is a D-bounded deduction of the formula M [s] from the totality M [s] {M [s]| } in such a sense that is used in the following D-bounded form : the generalization rule Gen x GenD , x(x D ) where x and are a variable and a formula of the theory T , respectively. n [s]) can be canonical ly extended to some sequence Lemma 2. A sequence g (M 0 [s],...,M gext (M 0 [s],...,M n [s])ext so that gext : M [s] M [s], i.e., gext is a usual deduction of the formula M [s] from the totality M [s]. Proof. We will look through all j from 1 to n. Let j be yi for some i < j , where y is not a free variable of every formula of the totality . The parameters of every formula M [s] from M [s] are only some members of the sequence s. Then M j [s] is x(x D M i [s]), where x differs from all the parameters of the totality M [s]. To the right after the formula M i [s], we insert in g the explicit axiom (M i (s) (x D M i [s])) obtained from the logical axiom scheme LAS1. Then applying the rule MP to the two previous formulas M i [s] and , after , we can insert in g the formula (x D M i [s]). Then the formula M j [s] x is obtained as the usual application of the rule Gen to the formula . This lemma implies that the translation of a deduction f (0 ,...,n ) : leads to the deduction gext (M 0 [s],...,M n [s])ext : M (s) M [s]. This procedure is always used without any stipulations. Lemma 3. Let every formula from the translation M [s] of a totality of formulas of the theory T be deducible in the axiomatic theory (S, a ) from the totality a of axioms of the theory S . Moreover, let f (0 ,...,n ) : . Then the deduction gext : M (s) M [s] can be extended to some deduction h : a M [s] in the theory (S, a ). [s] M [s]. Let gext = (0 ,...,m ). Every formula Proof. Consider the deduction gext : M [s] or follows i of the theory S in this deduction is either one of the formulas of the totality M from the previous formulas of this sequence as a result of application of one of the rules of deduction. First, we consider only i such that they do not follow from previous formulas of the deduction. These formulas belong to the totality M [s]. By the condition of the lemma, each of these formulas i is deduced in the theory (S, a ) from the totality a of axioms of this theory, i.e., for each i , there exists k 0 a deduction gi (i ,...,i i ) : (a )i i , where (a )i is some finite subtotality of the totality a . In the finite subtotality (a )0 ,..., (a )m , change all free variables in such a way that they become different from those variables which were touched by the application of the generalization rule in the deduction 0 gext . For i m + 1 such that i is a consecuence of the previous formulas, we set ki 0, i i . Then k k 0 0 0 kn h (0 ,...,0 0 ,1 ,...,1 1 ,...,m ,...,m ) is a deduction of the formula M [s] from the totality a in the theory (S, a ). Lemma 4. Let, for every sequence s from D, every formula from the translation M a [s] of axioms of the theory (T, a ) be deduced in the theory (S, a ) from the totality a of axioms of the theory (S, a ), i.e., M is a model of the theory (T, a ) in the theory (S, a ). Under this condition, if the theory (S, a ) is consistent, then the theory (T, a ) is also consistent. Proof. Suppose that the theory T is contradictory, i.e., there exist some formula of the theory T and some deduction f (0 ,...,n ) : a ì . On an arbitrary sequence s from D, consider its translation g (M 0 [s],...,M n [s]) and its canonical extension gext : M a [s] (M [s] ìM [s]) from Lemma 2. Then according to Lemma 3, there exists a deduction h : a (M [s] ìM [s]). 5771


However, by the consistency of the theory S , such a deduction is impossible. Therefore, the theory T is consistent. 2. Lo cal Theory of Sets

2.1. Prop er axioms and axiom schemes of the lo cal theory of sets. The local theory of sets is a first-order theory with two predicate symbols: the binary predicate symbol of belonging (write A B ) and the unary predicate symbol of universality (write A ), and also with two constants (empty class ) and a (infra-universe ). Ob jects of the LTS are called classes. The notation (u) is used for the formula (u0 ,...,un-1 ), where u0 , . . . , un-1 are free variables of the formula . For technical reasons, it is useful to consider the totality C of all classes A satisfying a given formula (x). This totality C is called the assembly defined by the formula . The totality C of all classes A satisfying a formula (x, u), is called the assembly defined by the formula through the parameter u. Along with these words, we will use the notation A C (A), and C {x|(x)}, C {x|(x, u)}. If C {x|(x)} and contains only one free variable x, then the assembly C is said to be wel l-defined by the formula . Assembles will be usually denoted by semibold Latin letters. Every class A can be considered as the assembly {x|x A}. The universal assembly is the assembly of all classes V {x|x = x}. An assembly C {x|(x)} is called a subassembly of an assembly D {x| (x)} (denoted by C D) if x((x) (x)). Assemblies C and D are said to be equal if (C D) (D C) (denoted by C = D). We will use the notation {x A|(x)} {x|x A (x)}. A1 (extensionality axiom). y z ((y = z ) (X (y X z X ))). Let be some fixed class. A class A will be called a class of class ( -class ) called a set of class ( -set ) if A . Aformula is said to be -predicative (see [28], ch. 4, ç 1) if for all variables x, all x, occurring in the formula stay only at the following positions: x(x ... AS2 (ful l comprehension axiom scheme). Let (x) be an X -predicative formula tion (x y ) is admissible and does not contain Y as a free variable. Then X (Y (y ((y Y ) (y X (y ))))). This axiom scheme postulates the existence of -classes, which will be denoted as the assemblies {x |(x)}. Let A be a class, and let the assembly C {x|(x)} be defined by an A-predicative formula . If C A, then the assembly C is a class. Actually, by AS2, there exists a class B {x A|(x)}. If x C, then x((x) x A) implies x B . Therefore, C B . Conversely, if x B , then, by AS2, x A (x), i.e., x C. Hence C = B . A3 (empty class axiom). Z ((x(x Z )) Z = ). / Lemma 1. X ( X ). Proof. Denote the formulas x and x X by and , respectively. Apply the theorem ì ( ). From A3, it follows that ì. Hence, by the implication rule, it follows that . Applying the generalization rule, we obtain x (x x X ). 5772 if A . A class A is symbol-strings x and ) and x(x ... ). such that the substituA C (A, u)


A class is said to be universal if A4 (equiuniversality axiom).

. V )).

U V ((U = V ) (U

This axiom postulates that equal classes are simultaneously universal or not universal. A5 (infra-universality axiom). a U (U a U ). This axiom postulates that the class a is the "smallest" universal class. We will call it infra-universal or the infra-universe. A6 (universality axiom). X U (U X U ). This axiom postulates that every class A is an element of some universal class. The following axioms explain what the notion "universality" means. A7 (transitivity axiom). U (U X (X U X U )). This axiom postulates that if is a universal class, then every -set is an -class. A8 (quasitransitivity axiom). U (U X Y (X U Y X Y U )).

This axiom postulates that if is a universal class, then every subclass of every -set is an -set. Within the framework of every class , we can define all basic set-theoretical constructions. For every class A, the -class P (A) {x | x A} is called the ful l -ensemble of the class A. A9 (ful l ensemble axiom). U (U X (X U PU (X ) U )). This axiom postulates that if is a universal class and A is an -set, then P (A) is an -set. For classes A and B , the -class A B {x | x A x B } is called the -union of the classes A and B ; the -class A B {x | x A x B } is called the -intersection of the classes A and B. A10 (binary union axiom). U (U X Y (X U Y U X U Y U )).

This axiom postulates that if is a universal class, then the binary -union of -sets is an -set. A10 and A8 imply that the same also holds for the binary -intersection. For a class A, consider the solitary -class {A} {x | x = A}. Call the -class {A, B } {A} {B }


the unordered -pair, and the -class A, B and B .



{{A} , {A, B } } the coordinate -pair of the classes A


Lemma 2. Let be a universal class, and let a, b . Then {a} , {a, b} , and a, b

are -sets.

Proof. If a is an -set, then by A9, P (a) . From {a} P (a), by A8, it follows that {a} is an -set. From A10, we now have {a, b} . According to the proved property, this fact, together with {a} , implies a, b . Corollary. Let be a universal class, and let a, a ,b,b and a, b b=b.


= a ,b



. Then a = a and

5773


For classes A and B , the -class A B {x | y z (y A z B x = y, z )} will be called the coordinate -product of classes A and B . Lemma 3. Let be a universal class and A, B . Then A B . Proof. Let a A and b B . Then {a} A B and {b} A B implies {a, b} A B . By A10, A B . According to Lemma 2, {a} P (A B ) and {a, b} P (A B ). For the same reason, a, b = {{a} , {a, b} } P (A B ). Hence a, b P (P (A B )). Therefore, A B P (P (A B )) . By A8, we have A B . Further, A and B will denote some fixed -classes. An -subclass u of the -class A B will be called an -correspondence from the -class A into the -class B and will be also denoted by u : A B . The formula u A B will be denoted also by u A B . For the -correspondence u : A B , consider the -classes dom u {x | x A ((y (y B x, y and rng u {y | y B ((x (x A x, y u))}. The -subclass Ba u a {y | y B a, y u} of the -class B will be called the -class of values of the -correspondence u on the element a A, and the -subclass u[A ] {y | y B (x (x A x, y u)} of the class B the image of the subclass A of the class A with respect to the -correspondence u. It is clear that u[{a} ] = u a for each a A and u[A] = rng u. If u a contains a single element b B (in such a sense that y (y B u a = {y } )), then this single element b is called the value of the -correspondence u on the element a A and is denoted by u(a) or by ba . An -correspondence u is said to be total if dom u = A and single-valued if u a = {u(a)} for every a dom u. A single-valued -correspondence is also called an -mapping ( -function ). A total single-valued -correspondence u : A B is called an -mapping ( -function ) from the -class A into the -class B and is denoted by u : A B . The formula expressing the property for the -class u to be an -mapping from the -class A into the -class B will be denoted by u A B . An -mapping u : A B is said to be -- injective if x, y A(u(x) = u(y ) x = y ) (this is denoted by u : A B ); -- surjective if rng u = B (this is denoted by u : A B ); -- bijective (one-to-one ) if it is injective and surjective (this is denoted by u : A B ). The -class {x |x A B } of all -mappings from the -class A into the -class B which are A -sets will be denoted by B() or by Map (A, B ). A11 (ful l union axiom). U (U X Y z (X U Y U (z X U Y ) (x(x X z x U ))) (rngU z U ))). An -correspondence u from -class A into -class B will be also called a (multivalued ) -col lection of -subclasses Ba of the -class B , indexed by the -class A. In this case, the class u and the formula Ba B |a A , respectively. An u A B will be also denoted by Ba B |a A and u -mapping u from A into B will also be called a simple -col lection of the elements b of the -class B indexed by the -class A. In this case, the class u, the class rng u and the formula u A B are also (ba B |a A) , respectively. denoted by (ba B |a A) , {ba B |a A}, and u The -class {y |x A(y Bx )} is called the -union of -col lection Ba B |a A and is denoted by Ba B |a A . The -class {y |x A(y Bx )} is called the -intersection of -col lection Ba B |a A and is denoted by Ba B |a A . 5774


u))}


In these terms and notation, the axiom of full union means that if is a universal class and Ba B |a A is an -collection of -subsets Ba of the -class B , indexed by the -set A, then its -union Ba B |a A is an -set. With -class A, in the canonical way, one associates the -col lection a |a A of one-element -sets of the -class A (according to Axiom A7, a A implies a ). The -union of this collection a |a A is called the -union ( -sum ) of the -class A and is denoted by A. If is a universal class and A is an -set, then A is also an -set. With every -class, A, in the canonical way, one associates the simple -col lection (a A|a A) of elements of the -class A. It is clear that {a A|a A} = A. The next axiom serves, in particular, for exclusion of the possibility for a set to be its own element. A12 (regularity axiom). U (U X (X U X = x (x X x U X = ))).

The next axiom postulates the existence of an infinite set. A13 (infra-infinity axiom). X (X a X x (x X (x a {x}a X ))). Denote the postulated a-set by . This axiom implies that the class is an a-set. By Axiom A5, is an -set for every universe . Consider the a-class

{Y a | Y Y y (y Y (y a y a {y }a Y ))}.
Since Pa ( ), Axioms A9 and A8 imply that is an -set. Consider the a-class {y a | Y (Y y Y )}. Since is an a-set. Call it the a-set of natural numbers. By Axiom A5, is Consider the initial natural numbers 0 , 1 0 a {0}a , 2 1 and , it follows that 0, 1, 2, §§§ . By Axiom A7, 0, 1, 2, §§§ The last axiom postulates the existence of a choice function. A14 (axiom of choice). U (U X (X U X = z ((z , by Axiom A8, we infer that an -set for every universe . a {1}a ,... . From the definitions of for every universe .

PU (X )\{}U U X )Y (Y PU (X )\{}U z (Y ) Y )))).

The description of mathematical axioms and axiom schemes is completed. 2.2. Some constructions in the lo cal theory of sets. Almost all modern mathematics (except for the naive category theory and the naive theory of mathematical systems) can be formalized within the framework of the infra-universe a. Only the mentioned naive theories require the use of other higher universes. To show that all naive category theories can be formalized within the framework of the local theory of sets, we need to introduce an analog of the coordinate -pair A, B also working with improper -classes A and B (see the corollary of Lemma 2). Now, let be some fixed universal class. Let A, A , A , . . . be -classes, where the prime symbol ( ) is used only for the sake of uniformity of the notation. The -collection i | i 2 such that 0 A and 1 A will be called the (multivalued) sequential -pair of -classes A and A and will be denoted by A, A . The -collection i | i 3 such that 0 A, 1 A , and 2 A will be called the (multivalued) sequential -triplet of -classes A, A , and A and will be denoted by A, A ,A . And so on. Now let a, a , a , ...be -sets. The simple -collection (ai | i 2) such that a0 a and a1 a will be called the simple sequential -pair of -sets a and a and will be denoted by (a, a ) . The simple -collection (ai | i 3) such 5775


that a0 a, a1 a , and a2 a will be called the simple sequential -triplet of -sets a, a , and a and will be denoted by (a, a ,a ) . And so on. If A, A , B , and B are -classes and A, A = B, B , then A = B and A = B . If a, a , b, and b are -sets and (a, a ) = (b, b ) , then a = b and a = b . Similar properties also hold for every finite -collections. Thus, the -pairs A, A and (a, a ) possess the mentioned property of the Kuratowski -pair a, a (see the corollary of Lemma 2). However, in contract to the latter, the -pair A, A works also for improper -classes. Multivalued sets were introduced in [31] and [32]. Let some -collection u Ai | i I be indexed by -class I = . The -class Ai | i I {z | (z : I ) (x (x I z (x) Ax ))} will be called the -product of the -col lection u. In a particular case, if A, A , A , . . . are -classes, then the -classes A, A , ,...will b e called the -product of the -pair A, A , the -triplet A, A ,A , . ..and A, A ,A will be denoted by A ½ A , A ½ A ½ A , . . . One can verify that A ½ A = {x |(y y (y A y A x = (y, y ) ))}. It is seen from this equality that the -product A ½ A is similar to the coordinate -product A A , but in contrast to the Ai |i I . latter, it is a particular case of the general product If A = A = A = ... , then A ½ A = A2) Map (2,A), A ½ A ½ A = A3) Map (3,A), ...At ( ( the same time, A A = A2) , and between the -classes A A and A2) , there exists only a bijective ( ( -mapping of the canonical form a, a (a, a ). Precisely this stipulates the necessity of introducing the noncoordinate -product A ½ A , A ½ A ½ A , . . . If n , then an -subclass R of the -class An) Map (n, A) is called n-placed -correspondence ( on -class A. The -mapping O : An) A is called n-placed -operation on -class A. Note that (


+1 O An) A = An) . Therefore an n-placed operation O cannot be considered as an (n + 1)-placed ( ( correspondence.

3.

Formalization of the Naive Category Theory within the Framework of the Lo cal Theory of Sets

3.1. Definition of a lo cal category in the lo cal theory of sets. By the naive notion of a category we mean the notion of metacategory given by MacLane in [27]. According to [27], a metacategory consists of objects a, b, c,... , arrows f , g , h,... , and four operations f dom f , f codom f , a ia , and f , g g f satisfying some additional conditions. Unfortunately, even such a pathological ob ject as the metacategory of al l metacategories satisfies this definition. The problem of formalization of the naive category theory appeared because of the internal contradictoriness of the notion of metacategory. The aim of such a formalization consists in that in some precisely described axiomatics (set-theoretical, arrow or mixed), it is necessary to give some strict definitions of some notion that, first, corresponds to the naive understanding of a category, second, is closed with respect to all operations and constructions of naive category theory, third, includes in itself all known important concrete examples of categories, and fourth, cuts off such naive pathological examples as the metacategory of all metacategories. Using the notation of the previous section we can formalize the naive notion of a category in the following way. For a universe , we define an -category as a large two-sorted algebraic system with two relations and one operation (see [32] and [4]). For this purpose, we will use the notion of -collection of -classes and -pair of -classes introduced in the previous sections. Consider a fixed a-set c , consisting of three elements of class denoted by the signs #, , and and called the symbol of partition, the symbol of composition, and the symbol of identification, respectively. The set c is called the signature of the category. Since a , we infer that c is also an -set for every universe . Fix some universe . 5776


Consider an -pair A Obj, Arr containing two -classes Obj and Arr and the -collection sc A | c with the three components sc # #A , sc A , and sc A . An -class C A, sc will be called an -category ( a category of the class ) if the -classes Obj , Arr, , , and occur in the sequential conjunction of the following formulas (written in an informal way): Pc 1. ( (Obj ½ Obj ) Arr) ( (Arr ½ Arr) Arr) ( Obj Arr); This formula postulates that to every pair of elements of Obj , the partition assigns some -class of elements of Arr; to every pair of elements of Arr, the composition assigns some third element Arr, and to every element of Obj , the identification assigns some element of Arr. Pc 2. (rng = Arr) (x, y Obj ½ Obj (x = y x y = )); is usually written in the form of the -collection Arr(, ) Arr | (, ) Obj ½ Obj ; in this notation, the indicated property means that the -class Arr is equal to the -union of this pairwise disjoint -collection. Pc 3. (dom = {x | u v w v w ((u, v , w Obj ) (v ,w Arr) (v Arr(u, v )) (w Arr(v, w)) (x = (v ,w ) ))}) ( : dom Arr); Pc 4. ( : Obj Arr) (X Obj ((X ) Arr(X, X ))) (f Obj ((f ) Arr(f, f ))); is usually written in the form of the simple -collection (i Arr | Obj ) , where i ( ); Pc 5. Arr(, ) ½ Arr(,) Arr(, ) for every elements , , Obj ; Pc 6. ( (F, G),H )) = (F, (G, H )) for every element , ,, Obj and every element F Arr(, ), G Arr(,) and H Arr(, ); Pc 7. (F, i ) = F and (i ,G) = G for every element , , Obj and every element F Arr(, ) and G Arr(, ). -Categories defined in such a way are said to be local. Elements F of the class Arr(, ) are called arrows from the object to the object . The formula . F Arr(, ) is also denoted by F : - . The correspondence is called the composition and is usually denoted simply by ; in this case, along with (F, G), we also write G F . An -category C is said to be smal l if C is an -set. An -category C is said to be locally small if every -class Arr(, ) is an -set. Remark. In category theory the rejection of the term a "morphism F from an object to an object " was due to the following reason. For algebraic systems U and V , the notion of a homomorphism f from U to V is usual; for smooth manifolds U and V the notion of a diffeomorphism f from U to V is usual and so on; the generalization of all these notions is the notion of a morphism of mathematical systems (see [4, 31, 32]). However mathematical systems U , V ,... of type C and morphisms f from U to V of status S do not form a category, because the morphism f does not uniquely define the system V ; therefore, for some systems, the property U, V = U ,V Mor(U, V ) Mor(U ,V ) = is possible. But this property contradicts the property Pc 2. To form the corresponding category, it is necessary to take not morphisms f from U into V but triplets f, U, V , which can be naturally called arrows from the system U into the system V , defined by the morphisms f (see. [27], I.8). 3.2. Functors and natural transformations and the "category of categories" and the "category of functors" in the lo cal theory of sets generated by them. Let C and D be -categories. An -class O , T is called a (covariant) -functor ( a functor of class ) from the -category C to the -category D if: (1) O is an -mapping from the -class Obj C into the -class Obj D; (2) T is an -mapping from the -class ArrC into the -class ArrD; (3) T (F ) ArrD (O ( ), O ()) for every ob ject , Obj C and every arrow F ArrC (, ); (4) T (G F ) = T (G) T (F ) for every ob ject , , Obj C and every arrow F ArrC (, ) and G ArrC (,); (5) T (i ) = iO () for every ob ject Obj C . Usually -mappings O and T are denoted by the same symbol . 5777


-Functors are exactly homomorphisms between -categories considered as algebraic systems. The composition of an -functor O , T from C to D and an -functor O , T from D to E is the -functor O O , T T from C to E . The identity -functor IC for the -category C is the -functor idObj C ,idArrC containing the two identical mappings for the -classes Obj C and ArrC , respectively. Now we will formalize the operation of the naive category theory known as the "category of categories." Take any universe such that . Consider the -class Cat {X | X is a -category} of all -categories C . Also, consider the -class f Arr {X | x Y Z ((Y, Z are -categories) (x is an -functor from Y to Z ) (X = x, Y , Z ))} of all -functorial arrows F , C , D . For every simple -pair (C , D) of -categories C and D, consider the -class f Arr (C , D) {X | x Y Z ((Y, Z are -categories) (x is an -functor from Y to Z ) (X = x, Y , Z ))}. Also, consider the -collection f Arr (C , D) f Arr | (C , D) Cat ½ Cat . Consider the -correspondence from f Arr ½ f Arr to f Arr generated by the composition of -functors and consider the -mapping from Cat to f Arr such that (C ) = IC , C , C . These -classes give the opportunity to consider the -correspondence sc from c into such that sc # , sc , and sc . As a result, we obtain the -category C Cat , f Arr ,sc . It will be called the -category of al l -categories and al l -functorial arrows between them. Now let C and D be fixed -categories. Suppose that and are -functors from C to D. A simple -collection T = (t ArrD | Obj C ) will be called a (natural) -transformation from the -functor to the -functor if: (1) t ArrD (( ), ( )) for every ob ject from Obj C ; (2) (F ) t = t (F ) for every ob jects , from Obj C and every arrow F from ArrC (, ). The composition U T of an -transformation T = (t ArrD | Obj C ) from to and an -transformation U = (u ArrD | Obj C ) from to is the -transformation (u t ArrD | Obj C ) from to . The identity -transformation I from the -functor to the -functor is the -transformation (I() ArrD | Obj C ) from to . Finally, we will formalize the operation of naive category theory known as the "category of functors." Consider the -class F unct (C , D) of all -functors from the -category C to the -category D. Also, consider the -class c Arr {X | x Y Z ((Y, Z are -functors from C to D) (x is an transformation from Y to Z ) (X = x, Y , Z ))} of all -transformational arrows F T, , . For every simple -pair (, ) of -functors and from C to D, consider the -class c Arr (, ) {X | x ((x is an -transformation from to ) (X = x, , ))}. Consider the -collection c Arr (, ) c Arr | (, ) F unct C , D) ½ F unct (C , D) . c Ar r ½ c Ar r to c Ar r generated by the comp osition of Consider the -correspondence from -transformations. Also, consider the -mapping from F unct (C , D) to c Arr such that () = I , , . These -classes give the opportunity to consider the -correspondence sc from c into such that sc # , sc , and sc . As result, we obtain the -category F (C , D) F unct (C , D), c Arr ,sc . It will be called the -category of al l -functors from the -category C to the -category D and al l -transformational arrows between -functors. The constructions C and F (C , D) show that the notion of -category is closed with respect to such im portant operations of naive category theory as the "category of categories" and the "category of functors." Thus, the notion of -category has all the good properties of the notion of U -category. 5778


4.

ZermeloíFraenkel Set Theory and Mirimanovívon Neumann Sets

4.1. The prop er axioms and axiom schemes of the ZF set theory. To begin with, we will cite the list of proper axioms and axiom schemes of the ZF theory (Zermelo-Fraenkel's set theory with the axiom of choice; see [13, 19, 21, 22, 33]). This theory is a first-order theory with two binary predicate symbols of belonging (we write A B ) and equality = (we write A = B ). The predicate of equality = satisfies the following axiom and axiom scheme: (1) x(x = x) (reflexivity of equality ); (2) (x = y ) ((x, x) (x, y )) (replacement of equals ), where x and y are variables, (x, x) is an arbitrary formula, and (x, y ) is constructed from (x, x) by changing some (not necessarily all) free occurences of x by occurrences of y with the condition that y is free for occurences of x that are changed. Ob jects of the given theory are called sets. As above, it is useful to consider the totality C of all sets A satisfying a given formula (x). The totality C is called the class (ZF ), defined by the formula . The totality C(u) of all sets A satisfying a formula (x, u) is called the class (ZF ) defined by the formula through the parameter u. Along with these words, we will use the notation A C (A), and C {x|(x)}, C(u) {x|(x, u)}. If C {x|(x)} and contains only one free variable x, then the class C is called wel l-defined by the formula . Every set A can be considered as the class {x|x A}. A class C {x|(x)} is called a subclass of a class D {x| (x)} (denoted by C D) if x((x) (x)). Classes C and D are called equal if (C D) (D C). Further, we will use the notation {x A|(x)} {x|x A (x)}. If a class C is not equal to any set, then C is called a proper class. Not every class is a set: the class / {x|x x} is a proper class. The universal class is the class of all sets V {x|x = x}. For classes C {x|(x)} and D {x| (x)} define the binary union C D and the binary intersection C D as the classes C D {x|(x) (x)} and C D {x|(x) (x)}. A1 (extensionality axiom ). X Y (u(u X u Y ) X = Y ). This axiom postulates that if two sets consist of the same elements, then they are equal. For sets A and B define the unordered pair {A, B } as the class {A, B } {z |z = A z = b}. A2 (pair axiom ). A2 For -- -- uv xz (z x z = u z = v ). and A1 imply that an unordered pair of sets is a set. sets A and B define: the solitary set {A} {A, A}; the ordered pair A, B {{A}, {A, B }}; From the previous assertions, we infer that {A} and A, B are sets. if and only if A = A and B = B . 5779 A C(u) (A, u)

Lemma 1. A, B = A ,B


AS3 (separation axiom scheme ). X Y u(u Y u X (u, p)), where the formula (u, p) does not contain Y as a free variable. This axiom scheme postulates that the class {u|u X (u, p)} is a set. This set is unique by A1. Actually, suppose that there exist some sets Y and Y such that u(u Y u X (u, p)) and u(u Y u X (u, p)). Then, by LAS11, u Y u X (u, p) and u Y u X (u, p). Whence, by LAS3 and LAS4, u Y u X (u, p), u Y u X (u, p), (u, p) u X u Y , and u X (u, p) u Y . Consequently, u Y u Y , and by the generalization Gen rule, u(u Y u Y ), whence, by A1, Y = Y . Consider the class C = {u|(u, p)}. Then the scheme AS3 can be expressed in the following form: X Y (Y = C(p) X ). For classes A and B, define the If A is a set, then, by AS3, the Since A B = {x A|x B } A B is a set. For a class C {x|(x)} define A4 (union axiom ). X Y u(u Y z (u z z X )) z X )). We can deduce fromA4 and AS3 that for every set A, its union A is a set. We have the equality A B = {A, B }. Therefore, for every set A and B , their binary union A B is a set. We will call the ful l ensemble of a class C the class P (C) {u|u C}. A5 (power set ( ful l ensemble ) axiom). X Y u(u Y u X ). If A is a set, then, according to A5 and A1, P (A) is a set. For classes A and B, define the (coordinate ) product A B {x|uv (u A v B x = u, v }. The fact that A B is a set for sets A and B follows from AS3, because A B P P (A B )). A class (in particular, a set) C is called a correspondence if u(u C xy (u = x, y ))). For a correspondence C, consider the following classes: dom C {u|v ( u, v C)}; rng C {v |u( u, v C}. If C is a set, then dom C C, by A4 and AS3, implies that dom C also is a set. A correspondence F is called a function ( a mapping ) if xy y ( x, y F x, y F y = y ). For a class F, the formula expressing the property to be a mapping will be denoted by func(F). For the expression x, y F, we also use the notations y = F(x), F : x y , etc. A correspondence C is called a correspondence from a class A into a class B if dom C A and rng C B (denoted by C : A B). A function F is called a function from a class A into a class B if dom F = A and rng F B (denoted by F : A B). The class {f |func(f ) dom f = A rng f B } 5780 difference A \ B as the class A \ B {x A|x B }. / difference A \ B is a set. A, by AS3, we infer that for any sets A and B , the binary intersection the union C as the class C {z |x((x) z x)}.


of all functions from a class A into a class B which are sets is denoted by B B A P (A B ), we infer that the class B A is a set for any sets A and B . The restriction of the function F to the class A is defined as the class F|A {x|uv (x = u, v x F u A}.

A

or by Map(A, B). Since

The image and the inverse image of the class A with respect to the function F are defined as the classes F[A] {v |u A(v = F(u))} and F-1 [A] {u|F(u) A}. A correspondence C from a class A into a class B is also called a (multivalued ) col lection of subclasses Ba C a {y |y B a, y C} of the class B indexed by the class A. In this case, the correspondence C and the class rng C are also denoted by Ba B|a A and Ba B|a A , respectively. The class Ba B|a A is also called the union of the col lection Ba B|a A . The class {y |x A(y Bx )} is called the intersection of the col lection Ba B|a A and is denoted by Ba B|a A . With every class A, in a canonical way, one associates the col lection a V|a A of element sets of the class A. For this collection, the equality A = a V|a A is holds. A function F from a class A into the class B is also called the simple col lection of elements ba F(a) of the class B indexed by the class A. In this case, the function F and the class rng F are also denoted by (ba B|a A) and {ba B|a A}, respectively. The collection (ba V|a A) is also denoted by (ba |a A). With every class A, in a canonical way, one associates the simple col lection (a A|a A) of elements of the class A. It is clear that {a A|a A} = A. AS6 (replacement axiom scheme ). xy y ((x, y , p) (x, y , p) y = y ) X Y x X y ((x, y , p) y Y ), where the formula (x, y , p) does not contain Y as a free variable. To explain the essence of this axiom scheme, consider the class F {u|xy (u = x, y (x, y , p))}. The premise in AS6 states that F is a function. Therefore, Scheme AS6 can be expressed in the following way: func(F) X Y (F[X ] Y ). In other words, if F is a function, then for every set X , the class F[X ] is a set. If A is a set, then by AS6, we infer that the class rng F {ba B|a A} is a set. Then F A ½ rng F implies that the class F (ba B|a A) is also a set. Therefore, if A is a set, then we use the notation F : A B and F (ba B|a A). A7 (empty set axiom ). xz (ì(z x)). Axiom A1 implies that the set containing no elements is unique. It is denoted by . A8 (infinity axiom ). Y ( Y u(u Y u {u} Y )). According to this axiom, there exists a set I containing , {}, {, {}}, and so on. A9 (regularity axiom ). X (X = x(x X x X = )). A function f : P (A) \ {} A is called a choice function for the set A, if f (X ) X for every X P (A) \ {}. The last axiom postulates the existence of a choice function for every nonempty set. 5781


A10 (axiom of choice (AC )). X (X = z ((z P (X ) \ {} X ) Y (Y P (X ) \ {} z (Y ) Y ))). The described first-order theory is called the axiomatic set theory of ZermeloíFraenkel ZF (with the choice axiom ) (see Zermelo [4] and Fraenkel [33]). 4.2. Ordinals and cardinals in the ZF set theory. In the same manner as was done in LTS, changing the word "-class" to the word "class" and the word "-set" to the word "set" in ZF, we define the (multivalued ) sequential pair A, A , the triplet A, A , A , ...of classes A, A , A , ..., the simple Ai A|i I of sequential pair (a, a ), the triplet (a, a ,a ), ...of the sets a, a ,a ,..., the product a col lection Ai A|i I , the product A ½ A , A ½ A ½ A , ...of the pair A, A , the triplet A, A , A , ..., of classes A, A , A ,... , an n-placed relation R An Map(n, A) on the class A, an n-placed operation O : An A on a class A, and so on. It can be verified that A ½ A = {x|y y (y A y A x = (y, y ))} and A2 = A A. A class P is said to be ordered by a binary relation on P if: (1) p P(p p); (2) p, q P(p q q p p = q ); (3) p, q , r P(p q q r p r). If, in addition, (4) p, q P(p q q p), then the relation is called the linear order on the class P. An ordered class P is said to be wel l-ordered if (5) Q( = Q P x Q(y Q(x y ))), i.e., every nonempty subset of the class P has the smallest element. Let P and Q be ordered classes. A mapping F : P Q is said to be monotone ( increasing, order preserving ) if p p implies F(p) F(p ). The mapping F is said to be strictly monotone if p < p implies F(p) < F(p ). The mapping F is said to be isotone if it is monotone and F(p) F(p ) implies p p . It can be verified that: (1) if F is isotone, then F is injective and strictly monotone; (2) if F is isotone and surjective, then F is bijective and the inverse mapping F-1 : Q P is also isotone. Ordered classes P, and Q, are said to be order equivalent (write P, Q, ) if there exists some isotone bijective mapping F : P Q. If a class P is ordered by a relation and A is a nonempty subclass of the class P, then an element p P is said to be the smal lest upper bound or the supremum of the subclass A if x A(x p) y P((x A(x y )) p y ). This formula is denoted by p = sup A. A class S is said to be transitive if x(x S x S). A class (a set) S is called an ordinal (ordinal number ) if S is transitive and well-ordered by the relation = on S. The property of a class S to be an ordinal will denoted by On(S). In the form of the formula, this is On(S) x(x S x S) x, y , z (x S y S z S x y y z x z ) x, y (x S y S x y x = y y x) T ( = T S x(x T y (y T x y ))). Ordinal numbers are usually denoted by Greek letters , , , and so on. The class of all ordinal numbers is denoted by On. The natural ordering of the class of ordinal numbers is the relation = . The class On is transitive and linearly ordered by the relation =. There are some simple assertions about ordinal numbers: (1) if is an ordinal number, A is a set, and A , then A is an ordinal number; 5782


(2) = { | } for every ordinal number ; (3) +1 {} is the smallest of all ordinal numbers that are greater than ; (4) every nonempty set of ordinal numbers has the smallest element. Therefore, the ordered class On is well-ordered. Thus, On is an ordinal. Lemma 2. Let A be a nonempty subclass of the class On. Then A has the smal lest element. Proof. By condition, there exists some ordinal number +1}. By separation axiom Scheme AS3 (ZF) this class is is well-ordered, the set B has the smallest element . Take B, and, therefore, . If > , then > . Thus, (1) the class A is an ordinal number ; (2) A = sup A in the ordered class On. Proof. (1) The set A is transitive. In fact, if x y A, then y A for some ordinal . By the transitivity of , we obtain x , whence x A. It is clear that the set A is well-ordered by the relation =. (2) Let us show that p A satisfies the formula p = sup A. First, p is an ordinal number. Second, assume that there is x A such that p < x, i.e., p x. Since p x and x A, we infer that p A p, but this is impossible. Therefore, x A(x p). Third, let y On((x A(x y )) y p). Since y p, we infer that x A(y x), but it contradicts x A(x y ). Therefore, p = sup A. A. a an is Consider the class B {x|x A x set. Since B On and the class On arbitrary element A. If , then the smallest element of the class A.

Lemma 3. If A is a nonempty set of ordinal numbers, then :

Corollary. The class On is a proper class. An ordinal number is said to be successive if = + 1 for some ordinal number . In the opposite case is said to be limiting. This unique number is denoted by - 1. For an ordinal number , the formula expressing the property of being successive (limiting) will be denoted by Son() [Lon()]. Lemma 4. An ordinal number is limiting if and only if = sup . The smallest (in the class On) nonzero limiting ordinal is denoted by . The existence of such an ordinal follows from A7, AS6, and AS3. Ordinals which are smaller than are called natural numbers. Collections Bn B|n N and (bn B|n N ), where N is an arbitrary subset of , are called sequences. If N n , then these collections are said to be finite ; otherwise, they are said to be infinite. Theorem 1 (principle of transfinite induction). Let C be a class of ordinal numbers such that : (1) C; (2) C +1 C; (3) ( is a limiting ordinal number C) S C. Then C = On. Proof. Let this be not true. Consider the subclass D On \ C. The class D is nonempty, and, therefore, according to Lemma 2, it has the smallest element . Now = , because C. Thus, is either a / successive ordinal number, or limiting. Suppose that = + 1. Since , it follows that D and, therefore, C. Then, by condition (2) of the theorem, = +1 C. Suppose that is a limiting ordinal number. Then C and, by condition (3) of the theorem, C. In both cases, we come to the contradiction with the fact that C. Therefore, C = On. / 5783


Theorem 2 (construction by transfinite induction). For every function G : V V, there exists a unique function F : On V such that for every On the equality F() = G(F|) holds. Proof. Consider the class C {f |func(f ) On(dom f ) x dom f (f (x) = G(f |x))}. Take any function f, g C and consider the numbers dom f and dom g . Let . If = 0, then f = g . If = 0, then consider the set P {x |f (x) = g (x)}. Suppose that the set P is nonempty. Then P contains the smallest element . Since f (0) = G(f |) = G() = G(g |) = g (0), we infer that = 0. By definition, for every x , we have f (x) = g (x), whence f | = g | . This implies f ( ) = G(f | ) = G(g | ) = g ( ). But it follows from P that f ( ) = g ( ). From this contradiction, we infer that the set P is empty. Therefore, f g . Thus, we have proved that implies f g . It follows from this property that = implies f = g . Consider the correspondence E {z | Onf C( = dom f z = , f )}. From what was proved above, we infer that E is a mapping from the class D dom E into the class V. We will consider this mapping in the form of a simple collection E (f C| D). As was proved above, implies f f . Let us prove that D = On by transfinite induction. Since C and 0, E, we infer that 0 D. Let D. Using the function f , we define the function g : + 1 V setting g | f and f () G(f ). From {} = , + 1 = {}, g = f { , G(f ) }, and the union axiom A4, it follows that this definition is correct. Let x + 1. If x , then g (x) = f (x) = G(f |x). By the transitivity, x = dom f . Therefore, f |x = g |x implies g (x) = G(g |x). If x {}, then g (x) G(f ) = G(g |x). Consequently, g C and +1,g E implies +1 D. Let be a limiting ordinal number, and let D. By Lemmas 4 and 3, = sup = . Let x . Then x y for some y D. Let x z . If y = z , then fy (x) = fz (x). If y z , then by of the imbedding fy fz , y z implies fy (x) = fz (x). If z y , then in a similar way, fz (x) = fy (x). Define the function g : V setting g (x) fy (x) for any y such that x y . It is clear that g |y = fy . From = {y |y }, g = fy |y g , the replacement axiom scheme AS6 and the union axiom A4, it follows that this definition is correct. Let us verify that g C. Let x dom g = . Then x y implies g (x) = fy (x) = G(fy |x) = G(g |x), since x y . Now from g C and = dom g , it follows that D. By the principle of transfinite induction, we conclude that D = On. Let x On. Then x x + 1 . Let x and x for some , On. Since , , f f , and f f , we infer that f (x) = f (x) = f (x). It follows that we can correctly define a function F : On V setting F(x) f (x) for every On such that x . It is clear that F| = f V for every On. If x On, then x x +1 and x implies F(x) = f (x) = G(f |x) = G(F|x). It remains to show that the function F is unique. Assume that there is a function F : On V such that F () = G(F |) for any On. Note that by the replacement axiom scheme AS6, F | V for any On. Consider the class A { On|F() = F ()}. Since F(0) = G(F|) = G() = G(F |) = F (0), we infer that 0 A, i.e., this class is nonempty. Assume that the class B On \ A is nonempty. Then it contains the smallest element . If , then A implies F() = F (). So F| = F | . Hence we obtain F( ) = G(F| ) = G(F | ) = F ( ), but this contradicts the inequality F( ) = F ( ). It follows from the obtained contradiction that A = On. In ZF, there exists the following principle of -induction. Lemma 5. If a class C satisfies the condition x C x C, 5784


then C = V. Proof. Suppose that C = D, i. e., D V \ C = . Then there exists P D. If P D = , then we set X P. Let P D = . Consider the set N containing all n satisfying the condition that there exists a unique sequence u u(n) (Rk |k n + 1) of sets Rk such that R0 = P and Rk+1 = Rk for every k n. Since the sequence (Rk |k 1) such that R0 X satisfies this property, we infer that 0 N . Let n N , i.e., for n, there exists a unique sequence u (Rk |k n + 1). Define the sequence v (Sk |k n +2), setting Sk Rk for every k n +1 and Sn+1 Rn = Sn , i.e., v = u { n +1, Rn }. It is clear that the sequence v possesses all the necessary properties. Let us verify its uniqueness. Suppose that there exists a sequence w (Tk |k n + 2) such that T0 = P and k n +1(Tk+1 = Tk ). Consider the set M consisting of all m n + 2 such that Sm = Tm . Let M \ (n + 2) and M M M . Since S0 = P = T0 , we infer that 0 M M . Let m M . If m = n + 1, then m +1 = n +2 M M . If m < n + 1, then m +1 n +2 and Sm+1 = Sm = Tm = Tm+1 implies m +1 M M . If m M , then m +1 M M . Therefore, m M implies m + 1 M . By the principle of transfinite induction, M = . Hence M = n + 2 and v = w, i. e., the sequence v is unique. Therefore, n + 1 N . By the principle of natural induction, N = . Thus, for every n , there exists a unique sequence u(n). By the uniqueness, we can denote it n by (Rk |k n +1). x / Consider the following formula of the ZF theory: (x, y ) (x y = Rx ) (x y = ). By the axiom scheme of replacement AS6, for , there exists a set Y such that x (y ((x, y ) y Y )). n n If n , then (n, Rn ) implies Rn Y . Therefore, in the set ½ Y , we can define an infinite sequence x u (Rn Y |n ) setting u {z ½ Y |x (z = x, Rx )}. The uniqueness property mentioned above implies u(m) = u(n)|(m + 1) for all m n. Thus u|(n +1) = u(n). Hence the sequence u satisfies the following properties: R0 = P and Rk+1 = Rk for every k . Having the set u, we can take the set A rng u {Rn |n } and the set Q A = {y |x (y Rx )} = Rn |n . It is clear that Rn Q for every n and, therefore, P = R0 Q. Since P D = , we infer that R Q D = . By the regularity axiom A8, there exists X R such that X R = . Let us verify that X D = . Actually, suppose that there exists x X D. Since X Q, we infer that X Rn for some n . Therefore, x X Rn implies x Rn = Rn+1 Q. Thus, x R. As a result, we have x X R = , but this is impossible. It follows from this contradiction that X D and X D = . Thus, in both cases, X C. By the condition, X C, but this is impossible, because X D. From this contradiction, we infer that C = V. Sets A and B are said to be equivalent (A B ) if there exists a bijective function u : A B. An ordinal number is said to be cardinal if for every ordinal number , the conditions and imply = . The class of all cardinal numbers will be denoted by Cn. The class Cn with the order induced from the class On is well-ordered. Lemma 6. For every set A, there exists an ordinal number such that A . Now, for a set A, consider the class { | On A}. By Lemma 6, this class is nonempty, and therefore it contains the smallest element . It is clear that is a cardinal number. Moreover, this class contains only one cardinal number . This number is said to be the power of the set A (it is denoted by |A| or card A). Two sets having the same power are said to be equivalent (it is denoted by |A| = |B |). A set of the power is said to be denumerable. Sets of the power n are said to be finite. A set is called countable if it is finite or denumerable. A set is said to be infinite if it is not finite. Note that if is an infinite cardinal number, then is a limiting ordinal number. Actually, if = + 1, then = card = card ( +1) = card < , but this is impossible. Let be an ordinal. A confinality of is the ordinal number cf (), which is equal to the smallest ordinal number for which there exists a function f from into such that rng f = . 5785


A cardinal is said to be regular if cf ( ) = , i.e., for every ordinal number , for which there exists a function f : such that rng f = , holds. A cardinal > is said to be (strongly ) inaccessible if is regular and card P () < for all ordinal numbers < . The property of a cardinal number to be inaccessible will be denoted by Icn( ). The class of all inaccessible cardinal numbers will be denoted by In. The existence of inaccessible cardinals cannot be proved in ZF (see [19], ç 13). 4.3. Mirimanovívon Neumann sets in the ZF set theory. Now we will apply the construction by transfinite induction in the following situation. Consider the class G {Z |X Y (Z = X, Y ) ((X = Y = ) (X = (ìfunc(X ) Y = ) (func(X ) (ìOn(dom X ) Y = ) (On(dom X ) (Son(dom X ) Y = X (dom X - 1) P (X (dom X - 1))) (Lon(dom X ) Y = rng X ))))))}. If we express the definition of the class G less formally, then G consists of all pairs X, Y for which there are the following five disjunctive cases: (1) if X = , then Y = ; (2) if X = and X is not a function, then Y = ; (3) if X = , X is a function, and dom X is not an ordinal number, then Y = ; (4) if X = , X is a function, dom X is an ordinal number, and dom X = + 1, then Y = X () P (X ()); (5) if X = , X is a function, and dom X is a limiting ordinal number, then Y = rng X . By definition, G is a correspondence. Since any set X possesses one of these properties, it follows that dom G = V. Since in each of these five cases the set Y is defined by a set X in a unique way, using the property of an unordered pair from Lemma 1, we infer that G is a function from V into V. According to Theorem 2, for the function G, there exists a function F : On V for which for any On, we have F() = G(F|). From case (1), for the function G, it follows that F() = G(F|) = G() = . From case (4), it follows that if is a successive ordinal number and = + 1, then F( ) = G(F| ) = (F| )() P ((F| )()) = F() P (F()). Finally, from case (5), it follows that if is a limiting ordinal number, then F() = G(F|) = rng (F|) = F( )| . Denote F() by V . Thus, we obtained the collection V V| On , satisfying the following conditions: (1) V0 = ; (2) V = V | , if is a limiting ordinal number; (3) V+1 = V P (V ). This collection is called the Mirimanovívon Neumann col lection, and its elements V are called Mirimanovívon Neumann sets. Let us prove now some lemmas on the sets V , which we will need later. Lemma (1) (2) (3) 7. < = V If and are ordinal numbers then : V V ; V = V ; and V+1 .

Proof. (1) and (2). By the transfinite induction, we will prove that for any ordinal number ( V V ). If = , then this is clear, because ì( ). 5786


If for some ordinal number ( V V ), then consider the ordinal number + 1. From + 1, we infer that = . If , then, by the inductive assumption, V V , and since V +1 = V P (V ), we infer that V V +1 . If = , then V = V V +1 , because V P (V ). Therefore, for + 1, the property +1 V V +1 holds. Suppose now that is a limiting ordinal number and ( V V ). Let belong to . Since is a limiting ordinal number, it follows that +1 . From V = V | , it follows that V+1 V . In this case, V V+1 implies V V . It is clear that = V = V . If V = V , then either < , or = , or < . If < , then V V ; if < , then V V . Therefore, = . If V V , then < , because for = , V = V , and for < , V V . (3) Consider the class C {x|x On x Vx }. Since 0 = V0 , we infer that 0 C. If C, then V implies +1 {} V V+1 . Let be a limiting ordinal number, and let C. By construction, V = V | . If x , then x C means that x Vx . Therefore, x P (Vx ) Vx+1 . Since is a limiting ordinal number, x +1 implies x V . Thus, V , and, therefore, C. By Theorem 1, C = On. The lemma is proved. Lemma 8. For every ordinal number , the condition z x V implies z V . Proof. We will prove this assertion by transfinite induction. Precisely, let C = {| On xz (z x V z V )}. Let us show that C = On. If = , then it is clear that C. Suppose that C. We prove that in this case, +1 C. Let z x V+1 . Since V+1 = V P (V ), we infer that x V or x V . If z x V , then z V by the inductive assumption, and, therefore, z V+1 . If x V and z x, then z V , and, therefore, z V+1 . Thus, +1 C. If is a limiting ordinal number and ( C), then from z x V , we infer that (z x V ), and, by the inductive assumption, we conclude that (z V ). From V = V | , it follows now that z V . Therefore, by the transfinite induction, C = On. This property is similar to the axiom of subset A8 from LTS. Lemma 9. For any ordinal number , x(x V x V ). Proof. This lemma will also be proved by the transfinite induction. For = , the given formula holds, because xì(x V ). Let for some ordinal number , x(x V x V ). Consider the ordinal number +1. If x V+1 , then x V x P (V ), or, more presicely, x V x V . In the case x V , by the inductive assumption, x V , and V V+1 implies x V+1 . If x V , then we infer that x V+1 from V V+1 . Now let be a limiting ordinal number, and let x(x V x V ). Then from x V , we infer that (x V ). By the inductive assumption, (x V ), and, therefore, x V . The lemma is proved. This property is similar to the transitivity axiom A7 from the LTS. Corollary 1. If and are ordinal numbers and , then V V . Corollary 2. For every ordinal number the inclusion V P (V ) and the equality V valid.
+1

= P (V ) are

Proof. If x V , then by the given lemma, x V , i.e., x P (V ). Thus, V P (V ). Therefore, V+1 = V P (V ) = P (V ). 5787


Corollary 3. If and are ordinal numbers and < , then |V | < |V |. Proof. By the previous two corollaries, V P (V ) = V |V | < |P (V )| = |V+1 | |V |. Lemma 10. For every ordinal number , if x V
+1 +1

V . Using Cantor's theorem, we infer that

, th en x V .

Proof. Suppose that x V+1 . This means that x V x V . If x V , then everything is proved. If x V , then by the previous lemma, x V . Lemma 11. For every ordinal number , xy (x V y V x y V ). Proof. We will again use the principle of transfinite induction. If = , then the conclusion of lemma is valid, because xì(x V ). Now let = + 1 for some ordinal number . Then from the formula x V y V , by Lemma 10, we infer that x V y V . Therefore, x y V , whence x y V +1 , i.e., x y V . Now suppose that is a limiting ordinal number and xy (x V y V x y V ). Then x, y V implies (x, y V ). Therefore, by the inductive assumption, (x y V ), and, therefore, x y V . This property is similar to the axiom of binary union A10 from the LTS. Lemma 12. For every limiting ordinal number , the condition x V implies P (x) V . Proof. Suppose that is some limiting ordinal number and x V . Then there exists such that x V . Let us show that in this case, P (x) V . Actually, by Lemma 8, from x V and z x, we infer z V , whence z (z P (x) z V ), and this means that P (x) V . If P (x) V , then P (x) V +1 V . Corollary 1. For every limiting ordinal number , the condition x, y V implies {x}, {x, y }, x, y V . Proof. By Lemma 12, P (x) V . By Lemma 8, {x} P (x) implies {x} V . Now, by Lemma 11, {x, y } V . It follows from the proved properties that x, y V . Corollary 2. For every limiting ordinal number the condition X, Y V implies X Y V . Proof. Let x X and y Y . Then {x} X Y and {y } X Y imply {x, y } X Y . By Lemma 11, X Y V . Since {x} P (X Y )and {x, y } P (X Y ), we infer that x, y {{x}, {x, y }} P (X Y ). Hence x, y P (P (X Y )). Therefore, X Y P (P (X Y )). By Lemmas 11, 12, and 8, X Y V . This property is similar to the axiom of full ensemble A9 from LTS. Lemma 13. If , then V . If > , then V . Proof. By Lemma 7, V V . If > , then by Lemma 8, V V
+1

, implies V

+1

V .

Now we will adduce some assertions about sets V for inaccessible cardinal numbers , which we will need later. Let be an ordinal number. Consider a collection K () M | +1 of the sets M {x||x |P (|V |)|} of all corresponding bijective mappings for all + 1 and the set M () P (|V |) M | +1 . By the axiom of choice there exists a choice function ch() : P (M ()) \ {} M () such that ch()(P ) P for every P P (M ()) \ {}. Since M M () for + 1, we infer that c () ch()(M ) M , i.e., c () is a bijection from P (|V |) onto |P (|V |)|. The following assertion can be called the theorem on initial synchronization of powers of Mirimanovívon Neumann sets. 5788


Theorem 3. Let be an ordinal number. Then for every ordinal number , there exists a unique |V | such that : col lection u() u()() (f | +1) of bijective functions f : V (1) f0 ; (2) if < +1, then f = f |V ; (3) if + 1 and = + 1, then f |V = f and f (x) = c ()(f [x]) for every x V \ V = P (V ) \ V ; (4) if +1 and is a limiting ordinal number, then f = f | . It fol lows from the uniqueness property that u()| +1 = u( ) for every , i.e., these col lections continue each other. Proof. First, let us verify the uniqueness of the collection u u(). For , let there exist a collection |V | possessing properties (1)í(4). Consider the set v (g | + 1) of bijective functions g : V D { + 1|f = g }, the class D On \ ( + 1), and the class D D D . It is clear that 0 D D. Let D. If , then +1 D D. Let < . Then D and +1 + 1. Therefore, by property (3), f +1 (x) = f (x) = g (x) = g +1 (x) for every x V and f +1 (x) = c ()(f [x]) = c ()(g [x]) = g +1 (x) for every x V +1 \ V , i.e., f +1 = g +1 . Therefore, + 1 D D. Thus, D implies +1 D. Let be a limiting ordinal number, and let D. If D = , then there exists such that + 1. Therefore, > + 1 implies D D. Let D = , i.e., D . Then for every , f = g holds. Since + 1, then +1. If = + 1, we infer that D D. Let + 1. If x V = V | , then x V for some . Therefore, by property (2), f (x) = f (x) = g (x) = g (x) for every x V , i.e., f = g . So D D. Thus, the properties Lon( ) and D imply D. By the principle of transfinite induction, D = On. Consequently, D = + 1. Therefore, u = v . Now we will write c instead of c (). Consider the set C consisting of all ordinal numbers for which there exists a collection u() with properties (1)í(4). Also, consider the classes C On \ ( + 1) and C C C . Since V0 = |V 0 | and |V0 | = 0, we infer that the collection u(0) (f | 1) with the bijective function f0 = : V0 possesses all properties (1)í(4), and, therefore, 0 C. Let C. If , then +1 C C. Now let < . Then +1 + 1 means that we can use the function c . Since C , we infer that for , there exists a unique collection u (f | +1). |V | setting g f for every Define the collection v (g | + 2) of bijective functions g : V x V and g+1 (x) c (f [x]) for every x V+1 \ V = P (V ) \ V . Let us verify that v possesses properties (1)í(4). Let +2. If + 1, then properties (1)í(4) are obviously true. Let = + 1. Then g (x) = g+1 (x) = f (x) = g (x) for every x V and g (x) = g+1 (x) = c (f [x]) = c (g [x]) for every x V \ V . Moreover, g |V = f = g . Therefore, < implies g |V = g |V = f |V = f = g . Therefore, +1 C C. Let be a limiting ordinal number, and let C. If C = , then there exists such that + 1. Consequently, > + 1 implies C C. Let C = , i.e., C . Then for |V | every , there exists a unique collection u (f | + 1) of bijective functions f : V with properties (1)í(4). Since + 1, it follows that + 1. If = + 1, then C C. Now let + 1. For every , consider the collection w u | + 1 (f | + 1). The collection w possesses properties (1)í(4). By the uniqueness, which was proved above, w = u . Therefore, u = u | + 1, i.e., f = f for every + 1. In particular, f = f for every . Define the collection v (g | + 1) of functions g setting g f for every and g (x)
f (x) for every x V = V | and every such that x V . It is clear that V |V | for every . Let us verify that g V |V |. By Corollary 1 of Lemma 9, g V V . Consequently, |V | |V |. Therefore, for every x V , g (x) f (x) |V |

5789


|V | |V || |V |. Let x, y V , and let g (x) = g (y ). Then x V and y V for some , . Consider the number , which is the greatest of the numbers and . By definition, f (x) = g (x) = g (y ) = f (y ). From the injectivity of this function, we infer that x = y . Therefore, the function g is surjective. Let z . Then z |V | for some . Since the function f : V |V | is injective, we infer that z = f (x) for some x V V . Consequently, z = g (x). Thus, g is a bijective function from V onto , i.e., V . By Corollary 3 of Lemma 9, |V | |V |. Therefore, there exists a set A {x |V ||y (x = |Vy |)} = {|V || } of all ordinal numbers |V |. Since is a limiting ordinal number, we infer that A = . Therefore, by Lemma 3, the set A = sup A is an ordinal number. If z A = {z |x A(z x)}, then z |V | for some . Conversely, if z , then z |V | A for some . Therefore, z A. Consequently, = A, i.e., is an ordinal number. Prove that is a cardinal number. Let be an ordinal number, , and let . Suppose that < . Then implies |V | for some . Consequently, < |V | = card |V | | | = | |. Since is an ordinal number, we infer that | | . As a result, we come to the inequality < , which is impossible. It follows from this contradiction that = . This means that is a cardinal number. V |V |. Since is a cardinal number and V , we infer that = |V |. Therefore, g Let us verify that the collection v possesses properties (1)í(4). By the definition of this collection, 0 g0 f0 = . Let < +1. If , then the equality f = f , which was proved above, implies g |V = f |V = f = f g . If = , then, by construction, g |V = g |V = f g . Thus, property (2) holds for v . Let + 1, = + 1, and let x V = P (V ). If , then the equality f = f , which was proved above, implies g (x) = f (x) = f (x) = f (x) = g (x) for every x V and g (x) = f (x) =

c (f [x]) = c (f [x]) = c (g [x]) for every x V \ V . Therefore, property (3) holds for v . Property (4) follows from property (2). From the properties, which were already verified, we infer that C C. By the principle of transfinite induction, C = On, and, therefore, C = +1.

Note that since the functions c () depend on the number , we cannot compose the (continuing each other) collections u()() into one global collection indexed by all ordinal numbers. Corollary. For every limiting ordinal number , the equalities |V | = |V || = {|V || } = sup{|V || } hold. Proof. Consider the number . By Theorem 3, there exists the corresponding collection u() (f | + 1). Since is a limiting ordinal number and + 1, by property (4), it follows that f = f | . Therefore, |V | = rng f = rng f | = |V || = {|V || } = sup{|V || }, where the latter equality follows from Lemma 3. Lemma 14. For every inaccessible cardinal number and every ordinal number , the property |V | < holds. Proof. Consider the set C {x ||Vx | < } and the classes C On \ and C C C . Since V0 = , we have |V0 | = 0 < . Therefore, 0 C. Let C. If , then +1 C C. Let < . Then C . If +1 = , then +1 C C. Let +1 < . Since V |V |, we have P (V ) P (|V |). Therefore, |P (V )| = |P (|V |)|. By Corollary 2 of Lemma 9, |V+1 | = |P (V )| = |P (|V |)|. Since |V | < and the cardinal number is inaccessible, we obtain |P (|V |)| < . Hence |V+1 | < . Thus, +1 C C. Let be a limiting ordinal number, and let C. If C = , then there exists such that . Therefore, > implies C C. Let C = , i.e., C . If = , then C C. Let < . By C , for every , we have |V | < . Therefore, sup{|V || } . Using the property |V | , we can correctly define the function f : , setting f ( ) |V |. It is clear that rng f = {|V || }. By Corollary of Theorem 3, rng f = {|V || } = 5790


sup{|V || } = |V | = . Then by initial inequality By the principle

|V |. By the inequality which was proved above, we infer that |V | . Suppose that the regularity of the number , = rng f implies , but this contradicts the < . Therefore, |V | < . Consequently, C C. of transfinite induction, C = On. Thus, C = .

Lemma 15. If is an inaccessible cardinal, then = |V |. Proof. By Lemma 7, V . Therefore, = | | |V |. By Corollary 1 of Theorem 3, |V | = sup(|V || ). Since |V | < , by Lemma 14 we have |V | . As a result, we have = |V |. Lemma 16. If is an inaccessible cardinal number, is an ordinal number such that < , and f is a correspondence from V into V such that dom f = V and f x V for every x V , then rng f V . Proof. Since is a limiting ordinal number, we have V = V | . For x V , there exists such that f x V . Therefore, the nonempty set {y |f x Vy } contains the smallest element z . By the uniqueness of the element z , we can correctly define the function g : V setting g (x) z . V . Consider the mapping Consider the ordinal number |V | and take some bijective mapping h : g h : and the ordinal number rng = sup rng . Suppose that = . Since the cardinal is regular, the supposition rng = implies |V |. But, by Lemma 16, |V | < . It follows from this contradiction that < . Since h is bijective, rng = rng g . Therefore, = sup rng g . If x V , then f x Vz = Vg(x) . From g (x) , by Lemma 7, we infer that Vg(x) V . Consequently, by Lemma 9, f x V implies f x V . Therefore, rng f V . By Lemma 7, rng f V +1 V . Lemma 17. If is an inaccessible cardinal number, A V , and f is a correspondence from A into V such that f x V for every x A, then rng f V .


Proof. Since is a limiting ordinal number, V = V | . Therefore, A V for some . By Lemma 9, A V . Define the correspondence g from V into V setting g |A f and g x V for every x V \ A. Then dom g = V and rng g = rng f . If x A, then g x = f x V , and if x V \ A, then g x = V . Therefore, by Lemma 16, we obtain rng f = rng g V . Consider the class {x| On(x V )} V | On . Lemma 18. = V. Proof. Let us show that satisfies the principle of -induction. Introduce the function ran : On setting ran(x) the smallest ordinal such that x V+1 . It follows from Lemma 7 that all ordinal numbers are contained in . Let us verify that x implies x for every set x. If x = , then, by Lemma 7, x = 0 V1 . Let x = . Consider the following formula of the ZF theory: (y, z ) (y z = ran(y )) (y z = ). By the axiom scheme / of replacement AS6, for the set x, there exists a set B such that y xz ((y, z ) z B ). If y x, then (y, ran(y )) implies ran(y ) B . Therefore, A {z B |y x(z = ran(y ))} B . By the axiom scheme of separation AS3, A is a set. By Lemma 3, A = sup A is an ordinal number. If y x, then z ran(y ) A implies z . Therefore, by Lemma 7, y Vz +1 V+1 . So x V+1 . Whence x P (V+1 ) V+2 . By the principle of -induction, we now infer that = V. 5. Universes, Ordinals, Cardinals, and Mirimanovívon Neumann Classes in the Lo cal Theory of Sets

5.1. The relativization of formulas of the LTS to universal classes. The interpretation of the ZF set theory in universal classes. It is convenient to denote by x a line of variables x0 ,...,xn-1 . Let all free variables of a formula be among y, x. Denote by x U the formula x0 U §§§ xn-1 U . We use the abbreviations x X () for x(x X ) and x X () for x(x X ). By U we 5791


will denote the formula (the relativization of the formula to the class U ) obtained by changing in all subformulas of the form x and x by x U and x U , respectively. Statement 1. Let U be a universal class theory in the LTS in which to the predicate U -correspondences B {z U |x U y U (z = (x, y )U x =LT S y )} on the class U in the LTS. Consider the interpretation M (U, I ) of the ZF symbols ZF and =ZF the correspondence I assigns the binary U (z = (x, y )U x LT S y )} and E {z U |x U y . The interpretation M is a model of ZF in the LTS.

Proof. We need to verify that in the LTS there exists a deduction of the formula or the scheme of formulas M [s] for every proper axiom or axiom scheme of the ZF theory and every sequence s x0 ,...,xq ,... of elements of the class U . On s, Axiom A1 is translated into the formula M A1[s] = A1U X U Y U (u U (u X u Y ) X = Y ). By the definition of equality in the LTS, this formula is evidently deducible. On s, Axiom A2 is translated into the formula M A2[s] = A2U u U (v U x U z U (z x z = u z = v ). For the U -sets u and v , consider the unordered U -pair x {u, v }U . By Lemma 2 of Sec. 2, x U . From the corresponding definitions, we infer that x = {u}U {v }U = {y U |y {u}U y {v }U } = {y U |y = u y = v }. By the axiom scheme AS2 (LTS), we have z U (z x z = u z = v ) and obtain the desired deducibility. On s, the axiom scheme of separation AS3 is translated into the scheme M AS3[s] X U Y U u U (u Y u X U (u, pM [s])), where Y is not a free variable of the formula (u, p). By AS2 (LTS), for the U -predicative formula U (u, pM [s]) and U -set X , there exists an U -class Y {u U |U (u, pM [s]) u X } such that u Y (u U u X U (u, pM [s])). Since Y X U , by the axiom of subset A8 (LTS) we have Y U , and this gives us the desired deducibility. On s, the axiom of union A4 is translated into the formula M A4[s] = A4U X U Y U z U u U (u z z X u Y ). For the U -set X and the corresponding U -predicative formula, by AS2 (LTS), there exists the U -class Z {w U |x, y U (x X y x w = x, y U )} X U U . Since Z x = x U for any x X , by the axiom of full union A11 (LTS), Y U [x U |x X U rngU Z U . If u z X , then u Y , and we obtain the desired deducibility. On s, the axiom of power set A5 is translated into the formula M A5[s] = A5U X U Y U u U (u X u Y ). For the U -set X , by AS2 (LTS), there exists an U -class Y PU (X ) {x U |x X }. By Axiom A8 (LTS), Y U . If u U and u X , then, by AS2, u Y , and we obtain the desired deducibility. On the sequence s, the axiom scheme of replacement AS6 is translated into the scheme M AS6[s] x U y U y U (U (x, y , pM [s]) y U (U (x, y , p[s]) y Y ))))) where pM [s] denotes the line of values of the terms p0 ,...,pm-1 on s under the interpretation M . By AS2 (LTS), for the U -predicative formula U (x, y , p[s]), there exists the U -class F {z U |x, y U (z = x, y U U (x, y , pM [s]))}. From the formula scheme cited above, we infer that the U -class F is an U -function. Consider any U -set X and the U -class Y F [X ]. Consider the U -class G {z U |x, y U (z = / x, y U U (x, y , pM [s]) x X } = F |X X U Y . If x X , then G x = U for x domU F and G x = {F (x)}U for x domU F . Therefore, by the axiom of full union A11 (LTS), Y = rngU G U . If x X , y U , and U (x, y , pM [s]), then x, y U F . Thus, y F [X ] Y . This proves the formula scheme M AS6[s]. 5792 U (x, y , pM [s]) y = y ) X U Y U (x U (x X


On s, the axiom of empty set A7 is translated into the formula M A7[s] = A7U x U z U (ì(z x)). / By axiom A3 (LTS), the empty U -set LT S possesses the necessary property z U (z LT S ). On s, the axiom of infinity A8 is translated into the formula M A8[s] Y U ( Y y U (y Y y U {y }U Y )). Consider the a-set postulated by the axiom of infra-infinity A13 (LTS). By this axiom, , and if y U and y , then y a {y }a . Let us verify that A y a {y }a = y U {y }U B . Let x A. Then x a and x y x = y . Since by Axiom A5 (LTS), a U , it follows x U . Therefore, x B . Conversely, let x B , i.e., x U and x y x = y . Since y a, by axiom A7 (LTS), we have, y a. If x y , then for the same reason x a. If x = y , then x a once again. Therefore, in each case, x a. Therefore, x A. From the equality which was proved above, we infer that y U {y }U . This means that the translation of Axiom A8 (ZF) is deduced in the LTS. On s, the axiom of regularity A9 is translated into the formula M A9[s] X U (X = x U (x X x U X = )). This formula is obviously deduced from the axiom of transitivity A7 (LTS) and the axiom of regularity A12 (LTS). Finally, on s, the axiom of choice A10 is translated into the formula M A10[s] X U (X = z U ((z PU (X ) \ {}U U X ) Y U (Y PU (X ) \ {}U z (Y ) Y ))). If = X U , then by axiom of choice A14 (LTS), there exists the class z such that (z PU (X ) \ {}U U X ) Y (Y PU (X ) \ {}U z (Y ) Y ). By Axiom A9, PU (X ) U , and, by Axiom A8, A PU (X ) \ {}U U . Therefore, by Lemma 3 of Sec. 2, B A U X U . From z B , according to Axiom A8, we infer that z U , and this gives us the required deducibility. According to Statement 1, in every universal class U , we can use all assertions for U -classes and U -sets which can be proved in ZF for the classes and sets. 5.2. The globalization of lo cal constructions. In the same manner as was done in ZF for classes, in the LTS, for assemblies A and B and classes A and B , we define the following assemblies: (1) (2) (3) (4) (5) (6) (7) (8) P (A) {x|x A}; A B {x|x A x B}; A B {x|x A x B}; {A} {x|x = A}; {A, B } {A}{B } = {x|x = A x = B }; A, B {A, {A, B }}; A B {x|y Az B(x = y, z )}; A {x|y A(x y )}.

In the same manner as was done in ZF, changing the word "class" to the word "assembly" and the word "set" to the word "class", in the LTS, we define a correspondence C with the domain dom C and the class of values rng C, a function ( a mapping ) F, a correspondence C : A B, a function F : A B, a (multivalued ) col lection Ba B|a A with the union Ba B|a A and the intersection Ba B|a A , a simple col lection (ba B|a A) with the assembly of members {ba B|a A}, the (multivalued ) sequential pair A, A , triplet A, A , A , ...of assemblies A, A , A ,... , the simple Ai A|i I of sequential pair (a, a ), the triplet (a, a ,a ), ...of classes a, a ,a ,... , the product a col lection Ai A|i I , the product A ½ A , A ½ A ½ A , ...of the pair A, A , the triplet A, A , A , ...of assemblies A, A , A ,... , an n-placed relation R An Map(n, A) on an assembly A, an n-placed operation O : An A on an asembly A, and so on. One can verify that the pairs a, b and (a, b) possesses the usual property: a, b = a ,b a = a b = b and (a, b) = (a ,b ) a = a b = b for every classes a and b. With every assembly A, in a canonical way the col lection a V|a A of element classes of the assembly A and the simple col lection (a A|a A) of elements of the assembly A are associated. The equalities A = a V|a A and A = {a A|a A} are valid for them. 5793


Now we will state the connection between local notions and constructions and corresponding global ones. Lemma 1. Let and be universal classes, let A , and let A . Then P (A) = P (A) = P (A). Proof. Let x P (A), i. e., x and x A. Since A , by Axiom A8, x . Therefore, x P (A). Hence P (A) P (A). The converse implication is verified analogously. It is clear that P (A) P (A). The inclusion P (A) P (A) can be verified as above. Corollary. For every class A, the assembly P (A) is a class. Proof. By the axiom of universality A6, for A, there exists a universal class such that A . Then, by the proved lemma, P (A) = P (A). But by the axiom scheme AS2, P (A) is a class. Lemma 2. Let and be universal classes, A, B , and let A, B . Then A B = A B = A B and A B = A B = A B . Proof. Let x A B , i.e. x and x A x B . Then x , and, therefore, x A B . Thus, A B A B . The converse inclusion can be verified in the same way. It is clear that A B A B . The inclusion A B A B is verified as above. Lemma 3. Let and be universal classes, A, B , and let A, B . Then {A} = {A} = {A}, {A, B } = {A, B } = {A, B }, and A, B = A, B = A, B . Proof. If y {A} {x |x = A}, then y = A , and, therefore, y {x Thus, {A} {A} . The converse inclusion is verified in the same way. It is clear inclusion {A} {A} is verified as was done above. Now according to the proved assertions and Lemma 2, {A, B } {A} {B {A} {B } {A, B } . Similarly, {A, B } = {A, B }. Finally, by Lemma 2 of Sec. 2, {A} , {A} , {A, B } , and {A, B } properties proved above, {A} and {A, B } . Consequently, applying the equality proved above, we obtain A, B Similarly, A, B


|x = A} {A} . that {A} {a}. The } = {A} {B } = . Therefore, by the

{{A} , {A, B } } = {{A} , {A, B } } = {{A} , {A, B } } A, B .

= A, B .

Corollary. For every class A the assembly {A} is a class. Proof. By the axiom of universality A6, for A, there exists a universal class such that A . Then, by the proved lemma, {A} = {A} . But, by the axiom scheme AS3, {A} is a class. Lemma 4. Let and be universal classes, A, B , and let A, B . Then A B = A B = A B . Proof. Let x A B , i. e., x and y . Similarly, z . By Lemmas 2 y z (y A z B x = y, z ), i. e., is verified in the same way. It is clear that A B A B . The y z (y A z B x = y, z ). Since y A , we have of Sec. 2 and 3 x = y, z = y, z . Therefore, x and x A B . Therefore, A B A B . The converse inclusion inclusion A B A B can be verified as above.

Lemma 5. Let and be universal classes, A, B , and let A, B . Then for every class u, the fol lowing assertions are equivalent : A B ]; (1) u A B [respectively u A B ]; (2) u A B [respectively u (3) u A B [respectively u A B ]. Moreover, dom u = dom u = dom u and rng u = rng u = rng u. 5794


Proof. (1) (2). By Lemma 4, u A B = A B . Therefore, dom u A. If x A, then, by (1), x A = dom u. Therefore, x and x, y u for some y B . By Lemma 3, x, y u. Hence x dom u. So A dom u. As a result, dom u = A. Let x, y u and x, y u for some x A. Then y, y rng u B . Since x, y , y and x, y , y , by Lemma 3, we infer that x, y = x, y u and x, y = x, y u. From (1), we now A B . infer that y = y . This means that u All other deducibilities are proved in the same manner. The equalities dom u = dom u = dom u and rng u = rng u = rng u are verified by using Lemma 3 in an obvious way. Lemma 6. Let and be universal classes, A , and let A . Then A = A = A. Proof. By definition, A a |a A {z |y A(z y )}. Therefore, if x A, then by Axiom A7, x y A implies x . Therefore, x A. Thus, A A. The converse inclusion is verified similarly. It is clear that A A. The inclusion A A is verified in the same way as above. Corollary. For every class A the assembly A, is a class. Proof. By the axiom of universality A6, for A, there exists a universal class such that A . Then, by the previous lemma, A = A. But by the axiom scheme AS2, A, is a class. Unfortunately, for classes A and B we cannot yet prove that the assemblies A B , A B , {A, B }, A, B , and A B are classes. This will be done in Sec. 5.4. 5.3. Ordinals and cardinals in the lo cal theory of sets. In the same manner as it was done in ZF, changing the word "class" to the word "assembly" and the word "set" to the word "class," in the LTS, we can define ordered and wel l-ordered assemblies, ordinals, and ordinal numbers. In the same manner as it was done in ZF, changing the word "class" to the word "U -class", the word "set" to the word "U -set," and the word "relation" to the word "U -relation," in the LTS, for every universal class U we can define U -ordered and wel l-U -ordered U -classes, U -ordinals, and U -ordinal numbers with the following change of the definition of a well-U -ordered U -class. Precisely, an U -ordered U -class P is said to be wel l-U -ordered, if Q(Q U = Q P x U (x Q y U (y Q x y ))), which means that every nonempty U -subclass of the U -class P has the smallest element. From x, y Q P U , we infer that this formula is equivalent to the formula Q( = Q P x Q(y Q(x y ))) cited in condition (5) from the definition of a well-ordered class in ZF. But in the LTS, this formula has a wider sense; precisely, this means that every nonempty subclass of the U -class P has the smallest element (compare with Lemma 2, Sec. 4 in ZF). This implies that the following lemma is fulfilled. Lemma 7. Let U be a universal class and U . Then the fol lowing assertions are equivalent : (1) is an ordinal number ; (2) is a U -ordinal number. Now we will infer from this lemma that the assembly On {x|On(x)} of all ordinal numbers in the LTS is well-ordered by the relation =. Lemma 8. The assembly On is wel l-ordered by the relation =. Proof. Let and be ordinal classes, and let = . By the axiom of universality A6, U and V for some universal classes U and V . Then either or . For certainty, let . In this case, by the axiom of subset A8, the nonempty V -set \ = { V | } V has the smallest / element V . We have by the definition of the V -set \ . Since every element is an element / of by the minimality of , we have . By the axiom of subset, U . From , and it / follows that = , i.e., . 5795


We have proved that = is a linear order on the assembly On. Let us show that this assembly is well-ordered with respect to the given order. Suppose that we have some nonempty class S of ordinal numbers. Consider a universe U , containing S . Then, by Axiom A7, S U . By Lemma 7, S is an U -class of U -ordinal numbers. Since, the universe U is a model of the theory ZF by Statement 1, we infer that the U -class S of U -ordinal numbers has the smallest element. The next lemma is similar to Lemma 2, Sec. 4, but it has another proof. Lemma 9. Let A be a nonempty subassembly of the assembly On. Then A has the smal lest element. Proof. By the condition, there exists some ordinal number A. By the axiom of universality A6 (LTS), there exists a universal class U such that U . Consider the assembly B {x U |x A x U {}U }. By the full comprehension axiom scheme AS2 (LTS), this assembly is an U -class. Since B On and the assembly On is well-ordered, we infer that the class B has the smallest element . Take an arbitrary element A. If < , then U . Whence, by the axiom of transitivity A7 (LTS), U . Therefore, B in this case, and hence . If = , then B once again, and, therefore . Finally, if > , then > . Therefore, is the smallest element of the assembly A. Lemma 10. Let be an ordinal number. Then : (1) the assembly + +1 {} is an ordinal number ; (2) + is the smal lest of al l ordinal numbers which are greater than the number .
+ Proof. (1) By Axiom A6, U for some U . Let x U ( +1)U U {}U . Then x U and either x or x = . Therefore, x + . Let y + . In this case either y or y . In both cases, + + y U . This means that y U . Thus, + = U and + is a U -ordinal number and, therefore, an ordinal + > . number. It is clear that (2) Let be an ordinal number such that > . Suppose that + > . Then + , i.e., either or = , but this contradicts the condition > . From this contradiction, we infer that + .

An ordinal number + will be called the successor of the ordinal number . Lemma 11. If A is a nonempty class of ordinal numbers, then : (1) A is an ordinal number ; (2) A = sup A in the ordered assembly On. Proof. By Axiom A6, A U for some universal class U . assembly X A and the U -class Y U A. By Lemma Statement 1, Y is an U -ordinal number, and, therefore, by also an ordinal number. Let a A. If X < a, then X a A implies X A and, therefore, X is an upper bound of the class A. Let a A. Suppose that X > . Then X = A implies impossible. Therefore, X . Thus X = sup A in On. Then, by Axiom A7, A U . Consider the 6, X = Y . By Lemma 3, Sec. 4 from ZF and Lemma 7, it is an ordinal number. Thus, X is = X , but this is impossible. Whence a X , be an ordinal number, and let a for every a for some a A. Hence < a, but this is

A limiting ordinal is an ordinal which is not equal to + for any ordinal number . As in Sec. 4, classes A and B are said to be equivalent (A B ) if there exists a one-to-one ( bijective) function u : A B. An ordinal number wil be called cardinal if for every ordinal number , the conditions and imply = . The assembly of all cardinal numbers will be denoted by Cn. The assembly Cn with the order induced from the assembly On is well-ordered. Let U be a universal class. Two U -classes A and B are said to be U -equivalent (A U B ) if there exists a bijective U -function u : A U B . A U -ordinal number is said to be U -cardinal if for every U -ordinal number , the conditions and U imply = . 5796


Prop osition 1. Let U be a universal class and U . Then the fol lowing assertions are equivalent : (1) is a cardinal number ; (2) is an U -cardinal number. Proof. (1) (2). By Lemma 7, is a U -ordinal number. Let be a U -ordinal number such that and U . This means that there exists a bijective U -mapping f : U . By the axiom of transitivity A7, U . Therefore, by Lemma 5, f . Hence . By condition (1), we obtain = . (2) (1). By Lemma 7, is an ordinal number. Let be an ordinal number such that and . This means that there exists a bijective mapping f : . By Axiom A7, U . Therefore, by Lemma 5, f U , i. e., U . By condition (2), we infer = . The power cardU A of a set A U in a universe U is an U -cardinal U such that there exists a one-to-one U -mapping f : A U . The power card A of a class A is a cardinal such that A . Prop osition 2. Suppose that A U V , U , and V . Then

card A = cardU A = cardV A < cardV U. Proof. Let cardU A = , U . Then V . By definition, there exists a one-to-one function f : A U . By Lemma 5, f A V . By Proposition 1, is a U -cardinal number. Therefore, = cardV A. Similarly, by Lemma 5, f A , and, by Proposition 1, is a cardinal number. Thus, = card A. Let us show now that cardV A < cardV U. According to Statement 1, cardV A cardV U . Suppose that cardV A = cardV U = , V. From the assertions proved above we infer that cardU A = cardV A = implies U . By Axiom A7, U , V and U V . By the definition of V -power, there exists a bijective V -function f : V U . According to Lemma 5 f U U . By the axiom of full union A11, U = rngU f U . We infer that U U , but this is impossible. An inaccessible cardinal number is defined in the LTS as was done in the theory ZF. An U -cardinal number is said to be U -regular if for every U -ordinal number for which there exists a U -function f : U such that U rngU f = , . An U -cardinal number > 0 is said to be U -inaccessible if is U -regular and for every U -ordinal number , from , it follows that PU () . Prop osition 3. Let U be a universal class and U . Then the fol lowing conditions are equivalent : (1) is an inaccessible cardinal number ; (2) is a U -inaccessible U -cardinal number. Proof. (1) (2). By Proposition 1, is an U -cardinal number. Let U , be an U -ordinal number, and let there exist a U -mapping f : U such that U rngU f = . By Lemma 7, is an ordinal number. Since , U , , U by the axiom of transitivity. Therefore, by Lemma 5, f and rngU f = rng f . Whence = U rng f . By Lemma 6, = rng f . Since is a regular cardinal number, we infer that . Hence is a U -regular U -cardinal number. Let U , be an U -ordinal number, and let . By Lemma 7, is an ordinal number. Since is inaccessible, P ( ) . By Lemma 1, PU ( ) = P ( ) . Therefore is a U -inaccessible U -cardinal number. (2) (1). By Proposition 1, is a cardinal number. Let be an ordinal number, and let f : be a mapping such that rng f = . Suppose that U . By the axiom of transitivity A7, U . By Lemma 7, is an U -ordinal number. By A8, , U . Therefore, by Lemma 7, f U and rng f = rngU f . By Lemma 6, = rngU f = U rngU f . Since is a U -regular U -cardinal number, we 5797


infer that < , but this is impossible. From this contradiction, we infer that the case is impossible. Thus, . Hence is a regular cardinal number. Let be an ordinal number, and let . By Axiom A7, U . By Lemma 7, is a U -ordinal number. Since is U -inaccessible, PU ( ) . By Lemma 1 and Proposition 2, card P ( ) = card PU ( ) = cardU PU ( ) . Therefore, is an inaccessible cardinal number. In the LTS, we can use the principle of transfinite induction because of the well-ordering of the assembly of all ordinals. Let us show this. Theorem 1 (principle of transfinite induction in the LTS). Let C be an assembly of ordinal numbers such that : (1) C; (2) C +1 C; (3) ( is a limiting ordinal number C) C. Then C = On. Proof. Suppose that this is not true. Consider the subassembly D On \ C. Since the assembly D is not empty, by Lemma 9, we infer that it has the smallest element. Then = , because C. Therefore is either + for some ordinal number or a limiting ordinal number. Suppose that = + 1. Since , it follows that D, and, therefore, C. By condition / (2) of the theorem, = +1 C. From this contradiction, we infer that = + 1. Now the case remains where is a limiting ordinal number. In this case, = sup and C; therefore, by the condition (3) of the theorem, = sup C. Therefore, the assembly D is empty, and, therefore, C = On. Theorem 2 (principle of natural induction in the LTS). Let C be some assembly in LTS such that : (1) C; (2) for al l n the condition n C implies n +1 C. Then C. Proof. Consider the assembly C = C . This assembly is nonempty, because C C, and, moreover, it contains only ordinal numbers. Suppose that the assertion of the theorem is not fulfilled. / In this case, the assembly C = {x|x x C} is nonempty, because it is a subassembly of On and, therefore, contains the smallest element . We know that = , because C. Since and = , there exists such that = + 1. In this case, C, because is the smallest ordinal number in C. By condition (2) of the theorem, +1 C in this case, i.e., C, and we obtain a contradiction with our assumption. 5.4. Mirimanovívon Neumann classes in the lo cal theory of sets and their connection with universal classes. Using all previous material, we will construct Mirimanovívon Neumann classes in the LTS. Consider an arbitrary universe U . Since it is a model of ZF, using the construction by transfinite U induction, we can, define Mirimanovívon Neumann U -sets V for every U -ordinal number U . By the axiom of universality A6 and Lemma 12, for every ordinal number , we define some Mirimanovívon U Neumann U -set V for every universe U such that U . Lemma 12. Let U and W be universal classes, and let be an ordinal number such that U and U W W . Then V = V . Proof. We will prove this by the transfinite induction. Consider the subassembly C of the assembly U W / / consisting of all ordinal numbers such that either U , W , and V = V , or U , or U = , and V W = , it follows that V U = V W . Therefore, C. Since U , W , V Let C. If U or W , then + 1 U or + 1 W respectively, i.e., + 1 C. / / / / U U U W W W U , W . By the facts proved in Sec. 4, V+1 = V U PU (V ) and V+1 = V W PW (V ). 5798 On W. L et By


U W assumption, V = V V . Since V U and V W , it follows that PU (V ) = PW (V ) by Lemma 1. U W Hence V+1 = V U PU (V ) P and V+1 = V W PU (V ) Q. By Axiom A9 (LTS), PU (V ) U U W and PU (V ) W . Using Axiom A7, we can easily verify that P = Q. Thus, V+1 = V+1 . Therefore, +1 C. Let be a limiting ordinal number such that C. If U or W , then C. Consider the / / U W case U and W . By Axiom A7, U and W . Since C, we have V = V V for all . By the assertions proved in Sec. 4,

V

U

U = U V |

U

and

V

W

= W V

W

|

W

.

U W Since V = V = V and V U , W V = W V | W . Let us show Let x R. Then x U and x V Therefore, x S . Thus, R S . The U W V = R = S = V . This means that By Theorem 3, C = On.

U V W for all , we can write V = U V | U and that R U V | U = W V | W S . for some . Since x V W by Axiom A7, we have x W . innverse implication is verified similarly. Therefore, we infer that C.

Using this lemma, for every On, we can define the Mirimanov ívon Neumann (we draw a line over V to differentiate these classes from the corresponding classes i U V for every universe U satisfying the condition U . As a result, we obtain Neumann col lection V V| On in the LTS. It satisfies properties (1)í(3) of Neumann collection in ZF listed in paragraph 4. Lemma 13. The col lection V V| On (1) = V = V ; (2) < V V . possesses the fol lowing properties :

class V in the LTS n ZF) as the U -class the Mirimanovívon the Mirimanovívon

Proof. First, we show that < implies V V . Suppose that U for some universe U . Then U U U implies V = V and V = V . By Statement 1, our assertion follows from the fact that in ZF, by Lemma 7, Sec. 4, < V V . Now we will prove all the assertions of the lemma. The assertion = V = V is proved above. If V = V , then either < or = , or < . If < , then V V ; if < , then V V ; therefore, = . The assertion < V V is already proved. If V V , then < , because for = , we have V = V , and for < , we have V V . The following theorem shows that all universal classes in the LTS are Mirimanovívon Neumann sets for inaccessible cardinal indices. Theorem 3. Let U be an arbitrary universal class. Then : (1) sup(On U ) = (On U ) U is an inaccessible cardinal number ; (2) U = V ; (3) the correspondence q : U such that U = V is an injective isotone mapping from the assembly U of al l universal classes into the assembly In of al l inaccessible cardinal numbers. Proof. (1) Since A On U is a nonempty class, because it contains the element 0 , by Lemma 11 we infer that is an ordinal number. Suppose that is not a cardinal number. In this case, there exist an ordinal number < and a bijective function f : . Since U and U , by Lemma 4, we have = U . Therefore, f is an U -function f : U . Since U and f (x) U for every x , by the axiom of full union, for the universal class U , we infer that = rngU f U On and, therefore, by the axiom of + + + + binary union, U U { }U U . By Lemma 10, U = + On. Thus, U < U , but this is impossible. From this contradiction, we infer that is a cardinal number. 5799


Suppose that the cardinal is not regular. Then cf ( ) < . By definition, there exists a function f : such that sup f [] = . As above, f is an U -function f : U and rngU f U . It is clear that rngU f f []. Conversely, if y f [], then y = f (x) for some x . Since f (x) U , we have y U . Consequently, y rngu f . As a result, f [] = rngU f U . By the axiom of full union, = sup f [] = f [] = U [y U |y f []]U U. Similarly, as was done before, the property U leads to a contradiction. Therefore, is a regular cardinal. Let be a cardinal number such that < . Since U , by the axiom of full ansemble and by Lemma 1, we have P () = PU () U . Consequently, card P () = cardPU (). According to Proposition 2, this last number is equal to the number cardU PU () U . Therefore, U On. Therefore, . Suppose that = . Then U . But, as above, this property leads to a contradiction. As a result, we infer that < . Now it remains only to show that > . Actually, since a (see the end of Sec. 2.1), we have U , and, therefore, +1 = { } U . Therefore, +1 A implies A = . The assertion (1) is proved. (2) From (1) it follows that is a limiting ordinal number. U Therefore, V = V | . Since U , by the definition, we have V = V U . U Consequently, V U . Conversely, let x U . By Lemma 18, Sec. 4, = V in ZF. Similarly U V | U U On U = U in the LTS. Therefore, x V for some A U . Since V = V , we have x V V . Therefore, U V . As a result, we infer that U = V . (3) From Lemma 13, we infer that is unique. Therefore, we can define a mapping q : U In such that q (U ) = , where U = V . From Lemma 13 we also infer that q is isotone. Corollary 1. If U is a universal class, then card U is an inaccessible cardinal number and U = V . Proof. According to Theorem 3, we need to only show that for any inaccessible cardinal number , card V = . W Consider some universal class W such that W . In this case, V = V W . By Proposition 2, card V = cardW V . Since the universe W is a model of ZF, by Lemma 15, Sec. 4, the property = W cardW V = card V is fulfilled in it. Therefore, if U is a universal class, then, by Theorem 3, U = V , where is an inaccessible cardinal number. Now our assertion follows directly from the property card U = card V = . Corollary 2. In the LTS, the equality V | On = V is valid. Proof. We need to show that for an arbitrary class x in the LTS, the assertion x V | On is valid, i.e., there exists On such that x V . By the axiom of universality, there exists a universe U such that x U , and, by Theorem 3, U = V for some On. Therefore, x V , i.e., our assertion is true. Theorem 3 allows to make the following conclusions about the structure of the assembly U {U |U } of all universal classes. The relation = is an order relation on the assembly U. We will denote it by , i.e., U V if U V or U = V . By Axiom A7, the assembly U is transitive. Therefore, U V implies U V . Thus, U V implies U V . Now we will prove that these relations are equivalent. Prop osition 4. Let U and V be universal classes. Then the relation U V is equivalent to the relation U V. Proof. We need only to verify that U V implies U V . By Theorem 3, U = V and V = V for some inaccessible cardinals and . If = , then U = V = V = V . If < , then, by Lemma 13, U = V V = V . Finally if > , then, by the same lemma, V = V V = U V , but this is impossible. Therefore, U V . 5800


Corollary 1. The infra-universe a is the smal lest element in the assembly U of al l universal classes. Corollary 2. If U is a universal class then either U = a or a U . Corollary 3. With the universal class a is associated a unique inaccessible cardinal number such that a = V . This number is the smal lest in the assembly In of al l inaccessible cardinal numbers. Thus, in the LTS, there exists at least one inaccessible cardinal number. Now let us prove now that in the LTS, there exists more than one inaccessible cardinal number. 5.5. The structure of the assemblies of all universal classes and all inaccessible cardinals in the lo cal theory of sets. Prop osition 5. In the LTS for every ordinal number , there exists an inaccessible cardinal number such that < . Proof. By the axiom of universality, U for some universal class U . By Theorem 3, U = V for U some inaccessible cardinal . By definition, V = V U = V . By Lemma 13, . Suppose that = . Then U . But this property leads to a contradiction, as was shown in the proof of Theorem 3. Therefore, < . This property is similar to the axiom of universality, which postulates that every class in the LTS is an element of some universal class. The parallelism between properties of universal classes and inaccessible cardinals in the LTS is also confirmed by the following assertions. Theorem 4. The assembly U of al l universal classes with respect to the order is wel l-ordered. Furthermore, every subassembly of the assembly U has the smal lest element. Proof. Let = A U. Using the injective and strictly monotone mapping q : U from the assembly U into the assembly On of the form U = V from Theorem 3, we can consider for the assembly A the subassembly B q [A] {x|x On U A(z = q (U))} of the assembly On. By Lemma 9, it has the smallest element , which is an inaccessible cardinal. Since B, we have = q (U ) for some U A, i.e., U = V . Since the mapping q is injective and strictly monotone, it follows that U is the smallest element in the assembly A. Corollary 1. For every class A there exists a universe U (A), which is the smal lest in the assembly of al l universes U such that A U . Corollary 2. The intersection A {x|U A(x U )} of any nonempty assembly A of universal classes is a universal class. Proof. By Theorem 4, the subassembly A of the assembly U has the smallest element U. It is clear that A U . If V A, then U V implies U V . Therefore, U A. So A = U . Theorem 4 allows us to complete the globalization of local constructions, which was started in Sec. 5.2. Corollary 3. For every classes A and B , the assemblies A B , A B , {A, B }, A, B , and A B are classes. Proof. By the axiom of universality A6, for A and B , there exist universal classes and such that A and B . By Theorem 4, either or . Therefore, there exists a universal class ( = or = ) such that , . Therefore, A, B . By the axiom of transitivity A7, A, B . Therefore, by Lemmas 2í5, A B = A B , A B = A B , {A, B } = {A, B } , A, B = A, B , and A B = A B . By the axiom scheme AS2, the right-hand sides of all these equalities are classes, because they are defined by -predicative formulas. Corollary 4. Let n \ 1, and let F be an assembly such that F is a mapping from the class n into the assembly V. Then the assembly F is a class. 5801


Proof. Consider the assembly K n consisting of all natural numbers k n such that the F|(k + 1) is a class. Consider the assembly K \ n and the assembly K K K . Since F|1 = 0, F(0) , by Corollary 3 to Theorem 4, we infer that F|1 is a class. Let k and k K. If k < n - 1, then k +1 n. Since k K in this case, the assembly is a class. By Corollary 3 to Theorem 4, the assembly k + 1, F(k + 1) is also a class. Now equality F|(k +2) = F|(k +1) { k +1, F(k +1) }, by the mentioned corollary, we infer that the F|(k + 2) also is a class. This means that k +1 K K. If k n - 1, then k +1 n implies k +1 K K. Applying Theorem 2, we conclude that K . Therefore, K = n. Consequently n means that the assembly F = F|((n - 1) + 1) is a class.

assembly F|(k +1) from the assembly -1 K

Corollary 5. Let A, A ,A ,... be classes. Then the assemblies (A, A ), (A, A ,A ),...are classes. Proof. By definition, the assemblies (A, A ), (A, A ,A ),... are particular cases of sequences (A0 ,...,An-1 ) when n \ 2. But, by the previous corollary, the sequences (A0 ,...,An-1 ) are classes. Thus, the assembly V of all classes in the LTS allows us to produce almost all set-theoretical constructions which are possible in a universal class or in the NBG-universe, except the construction of full union, which is basic for the construction by the transfinite induction. The fact that the construction of full union is actually impossible in the LTS follows from Statement 1, Sec. 8. This means that the global assembly of all classes in the LTS with respect to its constructive possibilitites is much poorer than local universal classes in it. The next theorem describes the structure of the assembly U of all universes in the LTS. It is proved by using of Theorem 4. Theorem 5. In the LTS, for every n , there exist a unique universal class U and a unique U -sequence of universal classes u(n) (Uk U |k n +1)U such that U0 = a, Uk Ul for every k l n +1 and if V is a universal class and U0 V U , then V = Uk for some k n +1 (the property of uncompressibility ). From the property of uniqueness, it fol lows that u(n)|m + 1 = u(m) for al l m n, i. e., these finite sequences continue each other. Proof. Consider the set N consisting of all n for which there exist a unique universal class U and a unique sequence of universal classes u u(n) (Uk U |k n +1)U such that U0 = a, Uk Ul for any k l n +1 and if V is a universal class and U0 V U , then V = Uk for some k n +1. By Corollary 1 to Theorem 4, for the infra-universe a, there exists a universe U which is the smallest from all universes U such that a U . Since the universe U U and the sequence (Uk U |k 1) such that U0 a satisfies all mentioned properties, we have 0 N . Let n N . Consider the assembly V {i|i u = U k n +1(u = Uk )}. By Axiom A6, for U , there exists a universal class K such that U K . Therefore, the assembly V is nonempty, and, consequently, by Theorem 4, it contains the smallest element V . It is clear that V = U and V U > U0 . Suppose that V U . Then by supposition, U0 V U implies A = Uk for some k n + 1, but this is impossible. Therefore, U V . Thus, in the universe V , we can define a V -sequence v (Vk V |k n +2)V setting Vk Uk for every k n +1 and Vn+1 U . It is clear that V0 = a and Vk Vl for every k l n +2. Let W be a universe, and let V0 W V . Then U0 W V . If W = U , then W = Vn+1 . If W U , then U0 W U implies W = Uk = Vk for some k n + 1. Finally, if U W , then U0 U1 §§§ Un U W implies W V. Therefore, V W . But this case is impossible. From the two previous cases, we infer that W = Vk for some k n + 2. This means that the pair V and v possesses all the necessary properties. Let us verify its uniqueness. Suppose that there exist a universe W and a W -sequence of universes w (Wk W |k n +2)|W such that W0 = a, Wk Wl for all k l n +2 , and if K is a universe and W0 K W , then K = Wk for some k n +2. 5802


Consider the universe U Wn+1 and the U -sequence u (Uk U |k n +1)U such that Uk Wk for every k n + 1. It is clear that U0 = W0 = a and Uk Wk Wk Ul for every k l n + 1. If K is a universe and U0 K U , then U0 K U and W0 K Wn+1 W . By the axiom of transitivity A7, W0 K W . Therefore, by assumption, K = Wk for some k n + 2. Since K Wn+1 , we have K = Wk = Uk for some k n + 1. Thus, the pair U and u possesses all the properties for n mentioned above. Therefore, because of the uniqueness of this pair, we infer that U = U = Wn+1 and u = u = w|n + 1, i. e., Wn+1 = U Vn+1 and Wk = Uk Vk for all k n + 1. Therefore, w = v . If W V , then by the above V0 = W0 W V implies W = Vk = Wk for some k n + 2, but this is impossible. If V W , then W0 = V0 V W in a similar manner implies V = Wk = Vk for some k n + 2, but this is impossible. Therefore, W = V and the uniqueness of the universe V and the sequence v is proved. Therefore, n +1 N . By the principle of natural induction, N = . Therefore, for any n , there exists the mentioned unique pair V and u. Unfortunately, in the LTS, in contrast to ZF, where there is the axiom scheme of replacement, we have no means to combine all these finite sequences into one infinite sequence of universal classes. By using Proposition 5 we can prove the following assertion Theorem 6. In the LTS, for every n , there exists a unique inaccessible cardinals such that 0 = , k l for every k cardinal and 0 < n , then = k for some k n (the prope From the property of uniqueness, it fol lows that c(n)|m + 1 = sequences continue each other. sequence c(n) (k I|k n +1) of l n + 1, and if is an inaccessible rty of incompressibility ). c(m) for al l m n, i.e., these finite

The proof is similar to the proof of the previous theorem. The remark made after Theorem 5 is also valid in this case: in the LTS there are no means to construct from these finite sequences continuing each other one infinite sequence of inaccessible cardinals. In the next section, we show how to do this in the theory ZF. 6. Relative Consistency b etween LTS and the ZF Theory

6.1. Additional axioms on inaccessible cardinals in the ZF theory. To prove the relative consistency, we need to write the axioms on inaccessible cardinals in a more formal way. Therefore, we are forced to adduce the following formal definitions in the ZF theory: -- is an ordinal number On() (x(x y (y x y ))) (x, y , z (x, y , z x y y z x z )) (x, y (x, y x y x = y y x)) z ( = z x(x z y (y z x y ))); -- f is a function func(f ) xy y ( x, y f x, y f y = y ); --f A B func(f ) dom f = A rng f B ; -- is a cardinal number Cn( ) On( ) x(On(x) (x = x ) u(u x ) x = ); -- is a regular cardinal number Rcn( ) Cn( ) x(On(x) u(u x rng u = ) ( = x x )); -- is an inaccessible cardinal number Icn( ) Rcn( ) x(On(x) x card P (x) ); -- IC (inaccessible cardinal ) x(Icn(x)); -- ISIC (infinite set of inaccessible cardinals ) X (x X (Icn(x)) X = x X x X (x x )); -- ISIC2 (infinite set of inaccessible cardinals of type + ) X Y (x X y Y (Icn(x) Icn(y ) x y ) X = Y = x X x X (x x ) y Y y Y (y y )); -- I (inaccessibility ) x(On(x) x (Icn(x ) x x )). Consider the class (possibly empty) In {x|Icn(x)} of all inaccessible cardinal numbers in the ZF theory. The adduced list will allow us later in thwe process of investigation of corresponding interpretations to look accurately at what values some derivative terms such as rng u, rng u, P (x), {x}, x {x}, x, y , 5803


dom f , rng f , and others take under the interpretation, and also what formulas such formulas as z , u x , and others are translated into. Theorem 1. In the ZF theory, the fol lowing assertions are equivalent : (1) ISIC ; (2) for every n there exists a finite set of inaccessible cardinals of the power n +1; (3) for every n there exists a finite sequence u (k |k n +1) of inaccessible cardinals such that k < l for al l k l n +1, i. e., the sequence u is strictly increasing ; (4) there exists an inaccessible cardinal and for every n , there exists a unique finite strictly increasing sequence u(n) (n |k n +1) of inaccessible cardinals such that n = , and from the 0 k fact that is an inaccessible cardinal and n n , it fol lows that = n for some k n +1 n 0 k (the property of uncompressibility ); (5) there exists a denumerable set of inaccessible cardinals : (6) there exists an infinite sequence u (n |n ) of inaccessible cardinals such that k < l for every k l , i. e., the sequence u is strictly increasing ; (7) there exists an infinite strictly increasing sequence u (n |n ) of inaccessible cardinals such that from n , is an inaccessible cardinal, and 0 n , it fol lows that = k for some k n +1 (the property of incompressibility); (8) there exists an infinite set of inaccessible cardinals. Proof. (1) (4). Let I be a nonempty set, existence of which is postulated by Axiom ISIC. Consider the nonempty class I {x|Icn(x) y I (x y )}. If x I, then x y for some y I . By ISIC, for y I , there exists z I such that y < z . Therefore, x < z I. Therefore, the class I possesses all the properties listed in formula ISIC. Since = I In, by Lemma 2, Sec. 4, in I, there exists the smallest element . From y for every y I , we infer that I. The class I possesses the following property: if z In and z y for some y I, then z I. Consider the set N consisting of all n for which there exists a unique sequence u u(n) (k I|k n + 1) such that 0 = , k < l for every k l n +1 and In and = 0 < n imply = k for some k n. Since the sequence (k I|k 1) such that 0 possesses all the mentioned properties, we infer that 0 N . Let n N . By the property of the class I, for n I, there exists z I such that n < z . Therefore, the class J {x I|n < x} is nonempty. Hence, by Lemma 2, Sec. 4 it contains the smallest element . Therefore, we can define a sequence v (k I|k n + 2) setting k k for every k n + 1 and n+1 , i. e., v = u { n +1, }. It is clear that 0 = and k < l for all k l n +2. Let In and 0 < n+1 . Then I and 0 < . If = n , then = n . If < n , then 0 < n implies = k = k for some k n. Finally, if > n , then J. Therefore, , but this contradicts the property < . Therefore, this case is impossible. It follows from the two previous cases that = k for some k n + 1. This means that the sequence v possesses all the necessary properties. Let us verify its uniqueness. Suppose that there exists a sequence w (k I|k n + 2) such that 0 = , k < l for all k l n + 2, and In and 0 < n+1 imply = k for some k n + 1. Since the sequence w|n +1 (k I|k n + 1) possesses all the mentioned properties for n, by the uniqueness of the sequence u, we infer that u = w|(n + 1), i.e., k = k k for all k n +1. If n+1 < n+1 , then by the above 0 = 0 n+1 < n+1 implies n+1 = k = k for some k n + 1, but this is impossible. If n+1 < n+1 , then in a similar way, 0 = 0 n+1 < n+1 implies n+1 = k = k for some k n +1, but this is also impossible. Therefore, n+1 = n+1 . Hence the uniqueness of the sequence v is proved. Consequently, n + 1 N . By the principle of natural induction, N = . Thus, for every n , there exists an unique mentioned sequence u(n). By its uniqueness, we can denote it by (n |k n +1). k / (4) (7). Consider the following formula of the ZF theory: (x, y ) (x y = x ) (x x y = ). By the axiom scheme of replacement AS6 (ZF), for , there exists a set Y such that 5804


x (y ((x, y ) y Y )). If n , then (n, n ) implies n Y . Therefore, in the set ½ Y , we n n can define an infinite sequence u (n Y |n ) setting u {z ½ Y |x (z = x, x )}. It x follows from the above-mentioned property of uniqueness that u(m) = u(n)|m +1 for all m n. Hence u|n +1 = u(n). It is clear that the sequence u possesses all the necessary properties. / (6) (1). Consider the following formula of the ZF theory: (x, y ) (x y = x ) (x y = ). By the axiom scheme of replacement AS6 (ZF), for , there exists a set Y such that x (y ((x, y ) y Y )). If n , then (n, n ) implies n Y . By the axiom scheme of separation AS3 (ZF), a class X {n |n } {y |x (y = x )} = {y |y Y x (y = x )} is a set. Since the sequence u is strictly increasing, then the set X satisfies the axiom ISIC. Deducibilities (7) (6) (5) (2) are obvious. Deducibilities (4) (3) (2) are also obvious. (2) (3) and (2) (6). Consider the nonempty class A of all finite sets of inaccessible cardinals. Then the class I A is also nonempty, and, therefore, by Lemma 2, Sec. 4, in I there exists the smallest element . Consider the set N consisting all n for which there exists a unique sequence u u(n) (k I|k n + 1) such that 0 = , k < l for all k l n +1 and I and 0 < n imply = k for some k n (the property of I-uncompressibility ). Since the sequence (k I|k 1) such that 0 possesses all the listed properties, we have 0 N . Let n N , i.e., for n, the sequence u (k I|k n + 1) is constructed. Consider the finite set A {k I|k n +1} of power n + 1. By condition (2), for n + 2, there exists a finite set B A of power n +2. In B take, the smallest element a and the greatest element b. By definition, a . Suppose that b n . Then for every c B , the inequality 0 = a c b n is valid. If c < n , then from c I, by the property of I-uncompressibility, we infer that c = k for some k n, i.e., c A. If c = n , then c A once again. As a result we come to the inclusion B A, but this is impossible. From this contradiction, we infer that n < b. Since b I, the class J {x I|n < } is nonempty. Therefore, by Lemma 2, Sec. 4 it contains the smallest element . Consequently, we can define the sequence v (k I|k n + 2) setting k k for every k n +1 and n+1 , i. e. v = u { n +1, }. Then in almost the same manner as in the inference (1) (4) changing In by I, we make sure that the sequence v possessses all the necessary properties and that it is unique. Therefore, n +1 N . By the principle of natural induction, N = . Therefore, for every n , there exists the unique mentioned sequence u(n). By its uniqueness, we can denote it by (n |k n +1). k Therefore, inference (2) (3) is finished. Now as in deducibility (4) (7) using the sequences (n |k n + 1), we construct an infinite strictly k increasing sequence u (n |n ) of inaccessible cardinals. It gives the inference (2) (6). Thus, the following deducibilities and equivalences are proved: (1) (4) (7) (6) (1) and (6) (5) (2) (6) and (2) (3). This immediately implies the equivalence of all assertions (1)í(7). (8) (6). Let I be an infinite set of inaccessible cardinals. By Lemma 2, Sec. 4 in I there exists the smallest . Consider the set N consisiting of all n for which there exists a unique sequence u u(n) (k I |k n + 1) such that 0 = , k < l for every k l n +1, and I and 0 < n imply = k for some k n (the property of I -incompressibility ). Since a sequence (k I |k 1) such that 0 = possesses all the listed properties, we infer that 0 N . Let n N . Consider the set J I \ {k |k n + 1}. It is nonempty because in the opposite case, the set I must be finite; therefore, it contains the smallest element . It is clear that = n and = 0 . Suppose that < n . Then by the condition n N , 0 < n implies = k for some k n, but this is impossible. Therefore, n < . Therefore, we can define a sequence v (k I |k n + 2) setting k k for every k n + 1 and n+1 , i.e., v = u { n +1, }. It is clear that 0 = and k < l for all k l n +2. Let I , and let 0 < n+1 . Then 0 < . If = n , then = n . If < n , then 0 < n implies = k = k for some k n. Finally, if > n , then > k for all k n + 1. Hence J . Therefore, , but this contradicts the property < . Therefore, this case is impossible. This follows from the 5805


two previous cases that = k for some k n + 1. This means that the sequence v possesses all the necessary properties. Let us verify its uniqueness. Suppose that there exists a sequence w (k I |k n + 2) such that 0 = , k l for all k l n +2, and I and 0 < n+1 imply = k for some k n +1. Since the sequence w|n + 1 (k I |k n + 1) possesses all properties for n mentioned above, by the uniqueness of the sequence u, we infer that u = w|n + 1, i. e., k = k k for all k n + 1. If n+1 < n+1 , then, by the above, 0 = 0 n+1 < n+1 implies n+1 = k = k for some k n + 1, but this is impossible. If n+1 < n+1 , then in a similar way, 0 = 0 n+1 < n+1 implies n+1 = k = k for some k n + 1, but this is also impossible. Therefore, n+1 = n+1 . Therefore, the uniqueness of the sequence v is proved. Consequently, n +1 N . By the principle of natural induction N = . Hence for every n , there exists a unique mentioned sequence u(n). By its uniqueness, we can denote it by (n |k n + 1). Further, as in the inference (4) (7), using the sequences (n |k n + 1), we construct the k k infinite strictly increasing sequence u (n |n ) of inaccessible cardinals. (6) (8). In the same manner as in the proof of deducibility (6) (1) for the sequence u, consider the set X {n |n } of its members. Suppose that the set X is finite. Then X contains the greatest element , but this contradicts the fact that the sequence U is strictly increasing. It becomes clear from assertion (6) of this theorm why in the mathematical literature, the axiom ISIC is also denoted by I ( ) and is called the axiom of -inaccessibility. Prop osition 1. In the ZF theory, the fol lowing assertions are equivalent : (1) ISIC2 ; (2) there exist infinite sequences u (m |m ) and v (n |n ) of inaccessible cardinals such that k < m < l < n for every k m and l n , i. e., the sequences u and v are strictly increasing and continue each other. Proof. (1) (2). By ISIC2 , there exist sets X and Y satisfying Axiom I there exist strictly increasing infinite sequences u (m X |m ) and k < l for all k, l . (2) (1). Similarly as in the proof of the deducibility (6) (1) from classes X {m |m } and Y {n |n } are sets. These sets satisfy SIC. Therefore, by Theorem 1, v (n Y |n ). By ISIC2 , Theorem 1, we verify that the Axiom ISIC2 .

It becomes clear from assertion (2) of this proposition why in the mathematical literature the axiom IS IC2 is denoted also by I ( + ). Roughly speaking, ZF+ISIC2 ensures the existence of + different inaccessible cardinals. Now we will clear up the correlation of the axioms on inaccessible cardinals: -- IC (inaccessible cardinal ) there exists at least one inaccessible cardinal ; -- ISIC there exists an infinite set of inaccessible cardinals ; -- ISIC2 there exist two infinite sets of inaccessible cardinals following one after another; -- I (inaccessibility ) for every ordinal there exists an inaccessible cardinal which is greater than . Prop osition 2. In the ZF theory, the deducibilities LI C IS IC2 IS IC IC are valid.

Proof. Let us prove that from I , we can infer property (2) from Proposition 1. The arguments completely repeats the proof of deducibility (1) (2) from Proposition 1 and deducibility (1) (2) from Theorem 1. Using now the equivalence of (2) and IS IC2 , we obtain the proof of deducibility I IS IC2 . All other deducibilities are obvious. In the [8], it is proved that in the ZF theory, the axiom of inaccessibility I is equivalent to the axiom of universality U. Therefore, the set theories ZF+I and ZF+U are equivalent. It can be also proved that in the ZF theory, the axiom of -inaccessibility I ( ) IS IC is equivalent to the axiom of -universality U ( ) X (U X (U 5806 ) X = U X V X (U V ))


postulating the existence of an infinite set of universal sets where U denotes the property of a set U to be universal. Therefore, the set theories ZF+ISIC and ZF+U( ) are also equivalent. 6.2. "Forks" of relative consistency. Using the globalization of local constructions in the LTS, which was made above, we can prove the following statement. Statement 1. Al l axioms of the ZF theory, except the axiom scheme of separation AS3 and the axiom scheme of replacement AS6, are deducible in the LTS as formulas of the LTS. Proof. For every formula in the first-order theory, the formula scheme is deduced. By the definition of equality in the LTS, this gives the formula u(u X u Y ) X = Y . Formula A1 is inferred from it by the rule Gen. For classes u and v , by Corollary 3 to Theorem 4, Sec. 5, there exists the class {u, v }. By definition, z {u, v } z = u z = v . Using the scheme , we obtain the formula (z {u, v }) z = u z = v . By the rule Gen, the logical axiom scheme LAS12, and the rule MP, we can infer from it the formula xz (z x z = u z = v ). Formula A2 (ZF) is inferred from it by the rule Gen. For a class X , by Corollary to Lemma 6, Sec. 5, there exists a class X . By definition, u X z (u z z X ). Using the formula scheme , we obtain the formula (u X ) z (u z z X ). By the rule Gen, the logical axiom scheme LAS12, and the rule MP, the formula Y u(u Y z (u z z X )) is inferred from it. Formula A4 (ZF) is inferred from it by the rule Gen. For a class X , by Corollary to Lemma 1, Sec. 5, there exists the class P (X ). By definition, u P (X ) u X . As was done above, we consecutively infer the formulas u P (X ) u X , u(u P (X ) u X ), Y u(u Y u X ), and A5 (ZF). Consider the class , which exists by the axiom of infra-infinity A13 (LTS). Let u . Then u a by the axiom of transitivity A7 implies u a. Therefore, by Lemma 3, Sec. 5, {u}a = {u}. By Lemma 2, Sec. 2, {u} a. By A7, u, {u} a. Hence, by Lemma 2, Sec. 5, u {u} = u a {u} = u a {u}a. By A13, we infer u {u} . Since we did not apply the rule of generalization, then by the theorem of deduction (see [28], Ch. 2, ç 4) and by the rule Gen, the formula u(u u {u} ) is deduced. Since, by A13, = , we infer that by the derivative rule of conjunction, the formula = u(u u {u} ) is deduced. Using logical axiom scheme LAS12 and the rule MP, we infer from it formula A7 (ZF). For every nonempty class X , by the axiom of universality A6, there exists a universal class such that X . By the axiom of transitivity A7, X . From the axiom of regularity A12 (LTS) the formula x(x X x X = ) is deduced. Since x X , by A7, we have, x . Hence, by Lemma 2, Sec. 5, x X = x X . Thus, the formula x(x X x X = ) is deduced. By the theorem of deduction, the formula X = x(x X x X = ) is deduced. By the rule Gen we infer from it formula A8 (ZF). In the LTS, consider the empty class . From A3 (LTS), the formula z (z ) is deduced. Using / LAS12 and MP, we infer formula A9 (ZF) from it. For every nonempty class X , by A6, there exists a universal class such that X . From the axiom of choice A14 (LTS), we infer the formula z ((z P (X ) \ {} X ) Y (Y P (X ) \ {} z (Y ) Y )). By the Lemmas 1, Sec. 5, and 3, Sec. 5, P (X ) = P (X ) and {} = {}. Therefore, z P (X ) \ {} X . By the axiom of transitivity A7, X and . Consequently by, Lemma 5, Sec. 5, z P (X ) \ {} X . Thus, the formula z (z P (X ) \ {} X ) Y (Y P (X ) \{} z (Y ) Y )) is deduced. By the theorem of deduction and the rule Gen, formula A10 (ZF) is deduced from it. The undeducibility of the axiom scheme of replacement in the LTS will be proved later. The existence of inaccessible cardinal numbers in the LTS proved in the previous section allows to prove the following statement. Statement 2. If the LTS is consistent, then the ZF+IC theory is consistent, where IC denotes the axiom postulated the existence of at least one inaccessible cardinal number. 5807


Proof. By the axiom of universality, for a fixed universe U0 , there exists a universe U such that U0 U . Consider the interpretation M (U, I ) of the ZF theory in the LTS, described in the proof of Statement 1, Sec. 5. Let us prove that this interpretation is a model of the ZF+IC theory. According to the proof of Statement 1, Sec. 5, we need to only consider the translation of Axiom IC and prove its deducibility in the LTS. We will use the notation of the proof of Statement 1, Sec. 5. On the sequence s Axiom IC is translated into the formula -- 0 M IC [s] = IC U x U (x is an inaccessible cardinal number)U , where -- 1 (x ) (Icn(x ))U (Rcn(x ))U x U ((On(x ))U x x cardU PU (x ) x ), where x U x U rngU u = -- 2 (x ) (Rcn(x ))U (Cn(x ))U x U ((On(x ))U u U (u x ) (x = x x x )); where -- 3 (x ) (Cn(x ))U (On(x ))U x U ((On(x ))U (x = x x x ) u U (u x U x ) x = x ), where -- 4 (x ) (On(x ))U x U (x x y U (y x y x ))) (x, y , z U (x, y , z x x y y z x z )) (x, y U (x, y x x y x = y y x)) z U (z = x U (x z x x ) x U (x z y U (y z x y ))), -- (On(x ))U = 4 (x x ) 4 (x ), -- (On(x ))U = 4 (x x ) 4 (x ). Comparision of the formula 4 (x ) with the definition shows that the subformula x U (x z x x ) is unusual in it. But in the place where it is staying, it is equivalent to the formula z x . Actually, if x z , then from z U , by the axiom of transitivity A7 (LTS), it follows that x U , and, therefore, x x . Therefore, we can substitute for . Under this substitution, we see that the formula 4 (x ) means that x is an U -ordinal number in the universal class U . Consequently, 4 (x ) and 4 (x ) mean that x and x are U -ordinal numbers. This leads to the following form of the formula 3 (x ): 3 (x ) = (x is an U -ordinal number)x U ((x is an U -ordinal number)(x x ) u U (u x U x ) x = x ). In this formula, the subformula u U (u x U x ) is unusual. Since x ,x U , we infer that, by the axiom of subset A8, u x U x U implies u U . Therefore, is equivalent to the x U x ). Substituting for , we see that 3 (x ) means that x is an U -cardinal formula u(u number. This leads to the following form of the formula 2 (x ): x U 2 (x ) = (x is an U -cardinal number)x U ((x is an U -ordinal number)u U (u x U rngU u = x ) (x x )). For the same reasons as above, in 2 , the quantifier prefix u U can be changed by u. But then the formula 2 (x ) means that x is an U -regular U -cardinal number. This leads to the following form of the formula 1 (x ): 1 (x ) = (x is an U -regular U -cardinal number)x U ((x is an U -ordinal number)x x cardU PU (x ) x ). This means that x is an U -inaccessible U -cardinal number in the universe U . Thus, Axiom IC was translated into the formula 0 M IC [s] = x U (x is a U -inaccessible U -cardinal number). Let us infer this formula in the LTS. By Corollary 3 to Proposition 4, Sec. 5, there exists an inaccessible cardinal number such that a = V . Since a U0 U , by the axiom of subset A8, we have, U . By Proposition 3, Sec. 5, is an U -inaccessible U -cardinal number. As a result, we deduced the desired formula. Statement 2 was proved by constructing a model of the ZF+IC theory in the LTS. It follows from Theorem 6, Sec. 5 that to construct a model of the LTS in the ZF theory, it is necessary to have the n "metasequence" c(0),c(1),...,c(n),... of finite incompressible sequences c(n) (k |k n +1) of inaccessible cardinals in ZF at least the same as in Theorem 6, Sec. 5. But in ZF, this metasequence can be 5808


n globalized by the axiom scheme of replacement into the usual unfinite sequence c (n n |n ). As Theorem 1 shows, the existence of such an infinite sequence of inaccessible cardinals is equivalent to Axiom ISIC. Using Theorem 1, we can prove the following statement.

Statement 3. If the ZF+ISIC theory is consistent, then the LTS is consistent. Proof. Consider the sequence (n |n ) from Theorem 1 and the set A {n |n }. By Lemma 3, Sec. 4, A = sup A is an ordinal number. Further, instead of Vn we will write Wn . Since n , we have Wn V . Therefore, D Wn |n V . By AS3, D is a set. Since 0 < n < n +1 n+1 , by Lemma 7, Sec. 4, we obtain, = V0 Wn Wn+1 D for every n . The set D is transitive. Actually, if y D, then by Lemma 9, Sec. 4, y Wm for some m implies y Wm D. Similarly, using Lemma 8, Sec. 4, we can verify that if x y D, then x D. Later, we will often use these two properties. Choose the set D in the capacity of the domain of interpretation of the LTS in the set ZF+ISIC theory. Consider the subset R {x D|n (x = Wn )} in D. Define a correspondence I assigning to the predicate symbol in the LTS the two-placed relation B {z D ½ D|x, y D(z = (x, y ) x y )}, to the symbol in LTS the one-placed relation R, and to the constant symbols and a in the LTS the elements and W0 of the set D, respectively. [s] of Let s be some sequence x0 ,...,xq ,... of elements of D. We will consider translations M axioms and axiom schemes of the LTS on the sequence s under the interpretation M and will prove their deducibility in the ZF+ISIC set theory. Instead of M [s] and M [s], we will write t and t for terms and formulas , respectively. To make our further account more simple, consider, first, the translations of some basic formulas. Let u and v be some classes in the LTS. The formula u v is translated into the formula (u v )t = ((ut ,v t ) B ). Denote this last formula by . By definition, this formula is equivalent to the formula (xy (x D y D (ut ,v t ) = (x, y ) (x y )). Using the property of a sequential pair, we conclude that ut = x and v t = y . Consequently, the formula (ut v t ) is deduced from . By the theorem of deduction, . Conversely, consider the formula . In the ZF theory, one can prove that for sets ut and v t , there exists a set z such that z = (ut ,v t ). By LAS3, the formula (z = (ut ,v t ) ut D v t D z = (ut ,v t ) ut v t ) is deduced from . Since the formula z = (ut ,v t ) is deduced from axioms, we infer that the formula (ut D v t D z = (ut ,v t ) ut v t ) is also deduced. By LAS12, the formula xy (x D y D z = (x, y ) x y ) is deduced, and it is equivalent to the formula z B and, therefore, to the formula . By the theorem of deduction, . Thus, the first equivalence (u v )t ut v t is valid. The formula v w is translanted into the formula (v w)t . Denote this last formula by . By the equivalence proved above it is equivalent to the formula u D(u v t u wt ). According to LAS11, the formula (x D (x v t x wt )) is deduced from the formula . If x v t , then v t D, and the transitivity of the set D implies x D. Then the formula implies x v t x wt . Consequently, by the theorem of deduction, the formula ( (x v t x wt )) is deduced. By the rule of generalization, the formula x( (x v t x wt )) is deduced. By LAS13, we infer the formula ( x(x v t x wt )), i.e., the formula ( v t wt ). Conversely, let the formula v t wt be given. Using the logical axioms, we can consecutively infer from it the formulas (u v t u wt ) and (u D (u v t u wt )). By the rule Gen, the formula is deduced. Therefore, by the theorem of deduction, the formula (v t wt ) is deduced. Thus, the second equivalence (v w)t v t wt is valid. It follows from this equivalence that we obtain the equivalence (v =LT S w)t (v t wt ) (wt v t ). By the axiom of extensionalty A1 (ZF), the last formula implies v t =ZF wt . By the theorem of deduction, in the ZF theory, the formula ((v t wt ) (wt v t ) v t = wt ) is deduced. Conversely, if v t =ZF wt , then, by the principle of changing equals (see Sec.4.1), the formula (u v t u wt ) is deduced. By the rule Gen, the formula v t wt is deduced. Similarly the formula wt v t is deduced. Therefore, 5809


the formula (v t wt ) (wt v t ) is also deduced. By the theorem of deduction, in the ZF theory, the formula (v t =ZF wt (v t wt ) (wt v t )) is deduced. Thus, we obtain the third equivalence (v =LT S w)t v t =ZF wt . Further, we will write not literal translations of axioms and axiom schemes but their equivalent variants, which are obtained by using the proved equivalences (u LT S v )t ut ZF v t , (v LT S w)t v t ZF wt , and (v =LT S w)t v t =ZF wt . We will denote these equivalent variants using the sign " " over them. At 1. y Dz D((y = z ) (X D(y X z X ))). In ZF, the formula y = z z = y can be proved in the following way. By the property of changing equals, we have (y = z (y = y z = y )). Since the formula y = y is valid for any y , we obtain y = z z = y . Moreover, by the property of changing equals, (y = z ) (y X z X ) and (z = y ) (z X y X ) are deduced. By using y = z z = y , (y = z ) (y X z X ) and (y = z ) (y X z X ) are deduced. Now, by LAS1 and the rule of generalization, X D((y = z ) (y X z X )) is deduced. Whence, by LAS13 and the rule of generalization, the formula At 1 is deduced. ASt 2. Let (x) be an X -predicative formula of the LTS such that the substitution (x y ) is admissible and does not contain Z as a free variable. Then X D(Z D(y D((y Z ) (y X (y ))))), [s ] in which by s we denote the corresponding change of the where denotes the formula M sequence s under the translation of the quantifier over formulas X (... ), Y (... ) and y (... ) indicated above. Since is a formula of ZF, we infer that ASt 2 is deduced from AS3 (ZF). Actually, by AS3 (ZF), for X D, there exists Z such that y (y Z y X (y )). Therefore, Z X D. By the definition of D, there exists n such that X Wn . By Lemma 8, Sec. 4, Z Wn D. Thus, for X D, there exists Z D such that y D(y Z y X (y )). / At 3. Z D((x D(x Z )) Z = ). Fix the condition Z D. Consider the formula x(x D x Z ). If x Z then, by the / condition, x D and then implies x Z . If x Z , then, obviously, implies x Z . Consequently, / / / under our condition, from is deduced x Z . By the rule of generalization, from is deduced x(x Z ). / / By Axioms A1 and A7 (ZF), x(x Z ) implies Z = . Thus, from the totality Z D and , Z = / is deduced. By the theorem of deduction, Z D implies the formula Z = . Conversely, by A1 and A7, Z = implies x(x Z ). Therefore, from the totality Z D and Z = , we can infer . / By the theorem of deduction, from Z D, we can infer the formula Z = . Therefore, from the condition Z D, the formula Z = is deduced. By the theorem of deduction, the formula Z D ( Z = ) is deduced. Therefore, by the rule of generalization, the formula At 3 is deduced. At 4. U DV D((U = V ) (U R V R)). By the property of changing equals, we have (U = V ) (U R V R). By the proved above, (U = V ) (V = U ), and, therefore, (U = V ) (V R U R). It follows that (U = V ) (U R V R), and by the rule of generalization, we infer the formula At 4. At 5. W0 R U D(U R W0 U ). The formula W0 R is deduced in ZF+ISIC by AS3. Therefore, we need to only deduce the formula U D(U R W0 U ). We can write this formula in another form as U D(n (U = Wn ) W0 U ). By Corollary 1 to Lemma 9 from Sec. 4.3, 0 n implies W0 Wn for every n . It follows from this assertion that the mentioned formula is deduced in ZF+ISIC. At 6. X DU D(U R X U ). It follows from X D that X Wn for some n . Consider U = Wn . Then X D implies U D U R X U , and it gives At 6 as a result. 5810


At 7. U D(U R X D(X U X U )). It follows from U R that U = Wn for some n , and X Wn implies X Wn by Lemma 9, Sec. 4. This gives the desired formula. At 8. U D(U R X DY D(X U Y X Y U )). Since from U R it follows that U = Wn for some n , we need only to prove that for any X, Y from D (X Wn Y X Y Wn ) holds. But this directly follows from Lemma 8, Sec. 4. At 9. U D(U R X D(X U PU (X ) U )), where the set Z PU (X ) is defined by the formula Z D(y D((y Z ) (y U y X ))). First, let us verify that if U R, X D, and X U , then Z = P (X ). Let y Z . Since Z D, it follows from the transitivity property that Z D. Consequently, y D. But, in this case, y D and y Z imply y X , i.e., y P (X ). Conversely, let y P (X ), i.e., y X . From X D, by the property of the set D proved above, we obtain y D. It follows from U R that U = Wn for some n . Consequently, by Lemma 8, Sec. 4, y X Wn implies y Wn = U . But then y D, y U , and y X imply y Z , and this proves the desired equality. By Lemma 12, Sec. 4, X Wn implies Z = P (X ) Wn = U . From here, the formula At 9 is deduced by the logical means. At 10. U D(U R X DY D(X U Y U (X U Y ) U )), where the set Z (X U Y ) is defined from the formula Z D(y D((y Z ) (y U (y X y Y )))). In the same way as in the deduction of the formula At 9, we verify that the conditions U R, X D, Y D, X U and Y U imply the equality Z = X Y , and also U = Wn for some n . By Lemma 11, Sec. 4, X, Y Wn implies Z = X Y Wn = U . From here, the formula At 10 is deduced. At 11. U D(U R X DY Dz D((X U Y U (z (X U Y ) ) (x D(x X z x U ))) ((rngU z ) U ))), where: -- the set Z1 (X U Y ) is defined from the formula Z1 D(y D((y Z1 ) (y U (u Dv D(u X v Y y = u, v ))))), U -- the set Z2 Z2 (x) z x is defined from the formula Z2 D(y D((y Z2 ) (y U y Y x, y z ))), U -- the set Z3 (rngU z ) is defined from the formula Z3 D(y D((y Z3 ) (y U y Y (x D(x X x, y z ))))). U As before, we verify that the conditions U R, u D, v D, u U , and v U consecutively imply the equalities {u} = {u}, {u, v } = {u, v }, and u, v = u, v , where U = Wn for some n . By U U U Corollary 1 to Lemma 12, Sec. 4 u, v Wn implies u, v = u, v Wn = U . U Therefore, in turn, we infer that the conditions U R, X D, Y D, X U , Y U , x D, and x X imply the equalities Z1 = X Y , Z2 = z x and Z3 = rng z . Let us also have the condition x D(x X z x U ). Since z is a correspondence from X into Y U , it follows that z is a correspondence from X into Wn . If x X D, then from the transitivity of D follows x D. Therefore, this additional condition implies z x = z x Wn . Since X Wn , by Lemma 17, Sec. 4, it follows that (rngU z ) = rng z Wn = U . From here, by logical means, we infer the formula At 11. At 12. U D(U R X D(X U X = x D(x X (x U X ) = ))), where the set Z (x U X ) is defined from the formula Z D(y D((y Z ) (y U (y x y X )))). If we fix some U R, i. e., U = Wn for n , then we need to prove the formula X D(X Wn X = x D(x X (x Wn X ) = )). Since X Wn implies X D, and x X implies x D, it follows that this formula can be transformed in to the formula X (X Wn X = x(x X (x Wn X ) = )). For x, X Wn , we have ((x Wn X ) = x X ); therefore, we need only to prove 5811


that X Wn (X = x(x X x X = )). But it is a direct consequence of the axiom of regularity in ZF. At 13. X D(X W0 X x D(x X ((x W0 {x}
W
0

) X ))), where:

-- the set Z1 (x W0 {x}W0 ) is defined from the formula Z1 D(y D((y Z1 ) (y W0 (y x y {x} 0 )))), W -- the set Z2 {x} 0 is defined from the formula Z2 D(y D((y Z2 ) (y W0 y = x))). W From the conditions X D, X W0 , x D, and x X , it follows that Z2 = {x}, and, therefore, Z1 = x {x}. In ZF, consider the set X . This set obviously satisfies the condition X x X (x {x} X ). We need to prove that W0 . Actually, since W0 = V0 and 0 > , by the definition of an inaccessible cardinal, by Lemma 13, Sec. 4, it follows that W0 . At 14. U D(U R X D(X U X = z D((z D(Y (PU (X ) \ {}U ) z (Y ) Y )))), where: PU (X ) \ {}U U X ) Y

-- the set Z1 (PU (X ) \ {}U ) is defined from the formula Z1 D(y D((y Z1 ) (y / U (y PU (X ) y {} )))), U -- the set Z2 z (Y ) is defined from the formula Z2 U Y, Z2 z . U -- denotes the formula M [s ] in which s denotes the corresponding change of the sequence s under the translation of the quantifier over-formulas U (... ), X (... ), and z (... ) indicated above. Fix the conditions U D, U R, X D, and X U . Denote PU (X ) \ {}U by S and P (X ) \{} by T . We have proved above that X U and U imply PU (X ) = P (X ) and {} = {}. Since U R, it U follows that U = Wn for some n . Therefore, by Lemma 12, Sec. 4, X U implies P (X ) U , and, by Lemma 8, Sec. 4, it implies T U . By Lemma 9, Sec. 4, y T U implies y U . All these properties imply Z1 = T . If Y D and Y Z1 , then Y T U implies Y U . As was stated above, Z2 U and Y U imply Y, Z2 = Y, Z2 . Then Y, Z2 z implies Z2 z Y . From here and from the previous conditions, we U cannot yet infer that Z2 = z (Y ). Consider the formula (z PU (X ) \ {}U U X ). It is the conjunction of the three following formulas: 1 (z S U X ), 2 (domU z = S ), and 3 (x(x S y (y X y (y X ( x, y U z x, y U z y = y ))))). Therefore, = . Since 1 = (u(u z u U xy (x S y X u = x, y U ))), 1 2 3 it follows that (u D(u z u U x Dy D(x Z1 y X u = x, y ))). Similarly, 1 U 2 = (x(x S x U x S y (y X x, y U z ))) implies (x D(x Z1 x 2 U x Z1 y D(y X x, y z ))). U Finally, (x D(x Z1 y D(y X y D(y X ( x, y z x, y z 3 U U y = y ))))). For X , by the axiom of choice A10 (ZF), there exists z such that (z P (X ) \ {} X ) Y (Y P (X ) \ {} z (Y ) Y ). Consider the formula (z P (X ) \ {} X ). As above, = 1 2 3 , where 1 = (u(u z xy (x T y X u = x, y ))), 2 = (x(x T x T y (y x, y z ))) and 3 = (x(x T y (y X y (y X ( x, y z x, y z y = y ))))). Since T U , by Corollary 2 to Lemma 12, Sec. 4, we obtain T X U . The formula 1 means that z T X . Therefore, z U and z D. Let us deduce from these properties the formula . Let u D and u z . Then, by Lemma 9, 1 Sec. 4, u z U implies u U . From the formula 1 , it follows that for u, there exist x T and y X such that u = x, y . By Lemma 9, Sec. 4, x, y U D. We have stated above that x, y = x, y in this case. Since x T and T = Z1 , it follows that x Z1 . Thus, from u z , the U formula (u U x Dy D(x Z1 y X u = x, y )) is deduced. Applying the theorem of U deduction and the rules of deduction, we deduce the formula . 1 5812


Let x D, and let x Z1 = T . Since T U , by Lemma 9, Sec. 4, it follows, that x U . From the formula 2 , we infer that for x, there exists y X such that x, y z . By the transitivity of D, the condition y X D, implies y D. Similarly, by Lemma 9, Sec. 4, y X U implies y U . But x, y = x, y in this case. Thus from x Z1 , the formula (x U x Z1 y D(y X x, y z )) U U is deduced. As above, from here, we deduce the formula . 2 Let x Z1 = T , y D, y X , y D, y X , x, y z , and let x, y z . As above, these U U conditions imply x, y z and x, y z . But then the formula 3 implies y = y . In turn, applying several times the theorem of deduction and the rules of deduction, we deduce the formula from the 3 formula . Thus, the formula is deduced. Since z T X , it follows that z Y = {z (Y )}. Consequently, from Z2 {z (Y )}, we infer that Z2 = z (Y ). Therefore, for the function z , the conditions Y D and Y Z1 = T imply Z2 = z (Y ) Y . All this means that from Axiom A10 (ZF) is deduced the existence of an ob ject z satisfying the formula , from which the formula Y D(Y Z1 Z2 Y ) is deduced. Therefore, in ZF, from the fixed conditions, the formula z D( ) is deduced. In turn, applying several times the theorem of deduction and the rule of generalization, we deduce as result the formula At 14. Since all the translations of the axioms of LTS turn out to be deducible formulas of the ZF+ISIC theory, it follows that the LTS is consistent. The absence of an axiom scheme like the axiom scheme of replacement in the ZF theory in the LTS apparently makes impossible an interpretation of the ZF+ISIC theory in the LTS. But this interpretation becomes possible if we strengthen the LTS by the axiom of an infinite class of universes IC U X (U X (U Lemma 1. The fol lowing assertions are (1) ICU ; (2) ITCU (an infinite transitive class (a) U Y (U ); (b) Y = ; (c) U V (U U V Y U (d) V Y W Y (V W ) (the ) X = V X W X (V W )).

equivalent in the LTS : of universes ) there exists a class Y such that : Y ) (the property of transitivity with respect to universes ); property of unboundedness ).

Proof. (1) (2). Denote by D the class the existence of which is postulated by Axiom ICU. It follows from the axiom of universality A6 that D for some universal class . By the axiom of transitivity A7, V D(V ). By Corollary 2 to Proposition 4, a or a = . It is clear that the second case contradicts ICU. Therefore, a . Consider the class E {U |U V D(U V )}. If U D, then, by ICU, V D(U V ). Therefore, D E . The class E is universally transitive. Actually, if U and U V E , then U V W D for some W . Using Axiom A7, we obtain U W D , U W , and U . Therefore U E . If V E , then V W D E for some W , by definition. Therefore, E has property (d). The deducibility (2) (1) is obvious. A similar lemma is valid for inaccessible cardinals in the ZF theory if we replace ICU by ISIC. Lemma 2. Let E be a nonempty class of universes with the transitivity property with respect to universes, i.e., E possesses properties (a)í(c) from Lemma 1. Then a E . Proof. Let V E . By Corollary 2 to Proposition 4, Sec. 5, V = a or a V . In the first case, a E . In the second case, a V E implies a E . Statement 4. If the LTS+ICU is consistent, then the ZF+ISIC theory is consistent. 5813


Proof. Consider the class C the existence of which is postulated by axiom ICU. According to the axiom of universality A6, there exists a universal class D such that C D. Consider the interpretation M (D, I ) of the ZF theory in the LTS described in the proof of Statement 1, Sec. 5. In the proof of Statement 1, Sec. 5, it was established that the interpretation M is a model of ZF in the LTS, and therefore, a model of ZF in the LTS+ICU. Let us verify the deducibility of the translation of Axiom ISIC under the interpretation M on an arbitrary infinite sequence s x0 ,...,xq ,... of elements of the class D. This translation has the form M IS IC [s] = X D(x D(x X Icn(x)D ) X = y D(y X z D(z X y z ))). In the proof of Statement 2, it was established that the formula Icn(x)D means that x is a D-inaccessible D-cardinal number in the LTS. In such that q () and = Vq() . By Theorem 3, Sec. 5, there exists the injective mapping q : U If C , then q () C D, by Axioms A7 and A8, implies q () D. Therefore, p q |C is an injective mapping from C into D. Since C D, it follows, by Lemma 5, Sec. 5, that p C D D and C D K . Since p() D, by the axiom of the full union A11, it K rng p = rngD p D. Hence p follows that K D. From C = , it follows that K = . If K , then D. By Proposition 3, Sec. 5, is a D-inaccessible D-cardinal. Consequently K consists of D-inaccessible D-cardinals. By Axiom ICU, for K and V C , there exists C such that . Consider the inaccessible cardinal p( ) K D. Since q is strictly monotone, it follows that . Consequently, the formula (K ) (x D(x K (x is a D-inaccessible D-cardinal)) K = y D(y K z D(z K y z )))) is deduced in the LTS+ICU. Therefore, the formula = X D (X ) is also deduced. Axiom ICU allows us to combine the finite sequences of universal classes continuing each other from Theorem 5, Sec. 5 into one infinite sequence. Prop osition 3. In the LTS, the fol lowing assertions are equivalent : (1) ICU ; (2) there exist a universal class X and an infinite strictly increasing X -sequence u (Un X of universal classes such that from n , V is a universal class, and U0 V Vn it fol V = Vk for some k n +1 (the property of incompressibility ); n (3) there exists a universal class X such that Uk X for any k n + 1 and any n n U (n)|k n + 1) u(n) (Uk U (n) are the increasing incompressible U (n)-sequences of classes continuing each other strictly from Theorem 5, Sec. 5.

|n )X lows that , where universal

Proof. (1) (2). Consider the class A the existence of which is postulated by Axiom ICU. By the axiom of universality, there exists a universal class X such that A X . By Theorem 4, Sec. 5, in the class A, there exists the smallest element . In the same way as in the proof of Theorem 5, Sec. 5, it is proved that for every n , there exists a unique X -sequence of universal classes u(n) (Uk A|k n +1)X such that U0 = , Uk Ul for every k l n +1, and if V is a universal class and U0 V Un , then V = Uk for some k n +1 (the property of incompressibility ). It follows from the property of uniqueness that u(n)|(m +1) = u(m) for all m n, i.e., these finite sequences continue each other. By this uniqueness, we can denote the sequence u(n) by n (Uk |k n +1). x Consider the X -class X A and the X -correspondence u {z X A|x (z = x, Ux X )}. n X A. By the axiom of transitivity, Since u n = {Un }X X for every n , it follows that u n A X implies U X . Therefore, u is an X -sequence (U X |n ). U n Un n n (2) (3). From the property of uniqueness of the U (n)-sequence u(n) and the class U (n) from Then orem 5, Sec. 5, it follows that u|n + 1 = u(n), i. e., Un+1 = U (n) and Uk = Uk for any n and any n k n + 1. Therefore, Uk X . 5814


x n (3) (1). Consider the X -class Y {y X |x (y = Ux )} = {Un X |n }X . Since the U (n)-sequences u(n) are strictly increasing and continue each other, it follows that the class Y satisfies Axiom ICU.

It follows from assumption (2) of this statement that the LTS+ICU resembles the axiomatics of da Costa (see [6] and [7]) with the denumerable set of constants U1 ,..., Un ,... for universes with axioms like the axiom X Un X Un+1 . However, the theory of da Costa uses the nonconstructive rule of deduction (precisely, the -rule of Carnap) and some properties of natural numbers. Corollary. In the LTS+ICU there exist a universal class X and an infinite strictly increasing incompressible X -sequence of universal classes u (Um X |m )X , and also for every n , there exist a unique universal class V and a unique finite strictly increasing incompressible V -sequence of universal classes v (n) (Vk V |k n +1)V such that V0 = X . From the property of uniqueness, it fol lows that v (n)|(l + 1) = v (l) for al l l n, i. e., these finite sequences continue each other. Proof. By Proposition 3, there exist the corresponding X and u (Um X |m )X . Further similarly to the proof of Theorem 5, Sec. 5 is deduced the existence of the corresponding V and v (n) (Vk V |k n +1)V . Roughly speaking, the LTS+ICU ensures the existence of + n different universal classes. It follows from this corollary and the remark made before Theorem 1 that to construct a model of the LTS+ICU in the ZF theory, it is necessary to have at least two infinite sequences u (m |m ) and v (n |n ) of inaccessible cardinals in ZF such that k < m < l < n for every k m and l n . But, as Proposition 1 shows, the existence of such infinite sequences is equivalent to Axiom ISIC2 . With the help of Proposition 1 we can prove the following statement. Statement 5. If the ZF+ISIC2 theory is consistent, then the LTS+ICU is also consistent. Proof. In the same way as in the proof of Statement 3, consider the sequences (m |m ) and (n |n ) from Proposition 1. Consider the sets A {m |m } and B {n |n }. Further, instead of Vm and Vn we will write Wm and Wn , respectively. Consider the ordinal numbers A = sup A and B = sup B and the sets D Wm |m V and E D Wn |n V . It is clear that = V0 W0 Wk Wm D V W0 Wl Wn E V for every 0 k m and 0 l n . Therefore, by Lemma 8, Sec. 4, we infer that Wk ,Wl E for all k, l . Choose the set E as the domain of interpretation of the LTS+ICU in the set ZF+ISIC2 theory. In E , consider the subsets R {x E |m (x = Wm )} and S {x E |n (x = Wn x = Wn )}. Define a correspondence J assigning to the predicate symbol in the LTS the two-placed relation C {z E ½ E |x, y E (z = (x, y ) x y )}, to the symbol in the LTS the one-placed relation S E , and to the constant symbols and a in LTS the elements and W0 of the domain E . Consider the interpretation N (E, J ) of the LTS in the ZF+ISIC2 set theory, which is similar to the interpretation M (D, I ), described in the proof of Statement 3. Let us prove that this interpretation is a model of the LTS+ICU. According to the proof of Statement 3, we need to only consider the translation of Axiom ICU and to prove its deducibility in ZF+ISIC2 . Let s x0 ,...,xq ,... be an arbitrary sequence of elements of the set E . The translation of Axiom ICU under the interpretation N on the sequence s has the form N IC U [s] X E (U E (U X U R) X = V E (V X W E (W X V W ))). Since m < 0 < 1 for every m , it follows that Wm W0 W1 . By Lemma 8, Sec. 4, R W1 and, therefore, R E . From W0 R, it follows that R = . If U E and U R, then U = Wm for some m . Since m < m +1 m1 , by Lemma 7, Sec. 4, we infer that U = Wm Wm+1 V R E . Consequently, for the set R in ZF+ISIC2 , the formula (R) (U E (U R U R) R = V 5815


E (V R W E (W R V W ))) is deduced. Therefore, the formula X E (X ) is also deduced. Thus, we have proved the following chain of interpretations: ZF + IC LT S ZF + IS IC LT S + IC U ZF + IS IC2 ZF + I, where T S denotes the interpretation of the theory T in the set S theory. Denoting by cons(T ) the consistency of the theory T , we obtain the inverse chain of relative consistency: cons(ZF + I ) cons(ZF + IS IC2 ) cons(LT S + IC U ) cons(ZF + IS IC ) cons(LT S ) cons(ZF + IC ). The similar chains remain valid, apparently, if we replace the ZF theory by the NBG theory. It follows from Proposition 2 that inside the ZF+I theory, which is the strongest of the mentioned ones, the chain of mutual interpretations can be continued further if we take as the next steps the LT S + IC U2 , ZF + IS IC3 theories, and so on. Since, according to Sec. 6.1, ZF + U ZF + I , it follows from Proposition 2 that the ZF + IS IC theory is weaker than the ZF + U theory. From Statement 3 of this section, it follows that the LTS is weaker than ZF + IS IC . Therefore, the LTS is weaker than the ZF + U theory. Thus, the LTS satisfies condition (1) formulated in the Introduction. It follows from Theorem 5, Sec. 5, that the LTS, as well as the theory ZF + U ( ) ZF + IS IC (see Sec. 6.1), has a countable totality of different universes and, therefore, satisfies all needs of category theory to such an extent as the theory ZF + U ( ) does. Therefore, the LTS satisfies condition (2). Finally, the axiom of universality A6 from the Sec. 2.1 asserts that in the LTS, there are no ob jects which are not elements of this countable totality of universes. For the same reasons, the LTS satisfies condition (3). It follows from here that the LTS is a more adequate foundation for category theory than the ZF + U and ZF + U ( ) theories. Moreover, the consistency of the ZF + U ( ) theory implies the consistency of the LTS. Moreover, the LTS is a more adequate foundation for category theory than the set theory of da Costa, because the existence of a countable totality of universes in the LTS is deduced but is not postulated beforehand as in the axiomatics of da Costa. This saves us from the necessity of attracting externally the natural numbers and their properties. Note also that in Sec. 8.2 we will show that in the LTS we cannot prove that the assembly sequence of n n finite U (n)-sequences u(n) (Uk U (n)|k n +1)U (n) of universal classes Uk constructed in Theorem 5, Sec. 5 can be continued as was done in the assertion (3) of Proposition 3. This means that in the LTS we have only a countable assembly of universes from Theorem 5, Sec. 5. 7. Pro of of Relative Consistency by the Metho d of Abstract Interpretation

The method of abstract interpretation going back to Gè odel (see [19], 10) is a direct generalization of the method of interpretation stated in Sec. 1.3. 7.1. Abstracts of a set theory. Let S be some set theory (see Sec. 1.3). We will consider that either S is a theory with the equality or in S the equality is introduced by the formula (A B ) (B A). In exactly the same way as in the ZF set theory, we introduced classes (see 4.1), and in the LTS, we introduced assemblies (see 2.1), and in an arbitrary set theory S , we introduce the abstracts C {x|(x)} and C(u) {x|(x, u)}. For the abstracts C {x|(x)} and D {x| (x)}, as in Sec. 2.1, we define the formulas C D and C = D. Define the formula C y as the notation for the formula z (z y z = C). As in the Sec. 5.2, for abstracts A and B and ob jects A and B of the S set theory, we introduce the abstracts P (A), A B, A B, {A}, {A, B }, A, B , A B, and A. Similarly, in S , we define a correspondence C with the domain of definition dom C and the range of values rng C, a function ( a mapping ) F, a correspondence C : A B, a function F : A B, a (multivalued ) col lection Ba B|a A with the union Ba B|a A and the intersection 5816


Ba B|a A , a simple col lection (ba B|a A) with the abstract of members {ba B|a A}, the (multivalued ) sequential pair A, A , triplet A, A , A , ...of abstracts A, A , A ,... , the simple Ai A|i I of a sequential pair (a, a ), triplet (a, a ,a ),...of objects a, a ,a ,... , the product col lection Ai A|i I , the product A ½ A , A ½ A ½ A , ...of the pair A, A , triplet A, A , A , ...of abstracts A, A , A ,... , an n-placed relation R An Map(n, A) on an abstract A, an n-placed operation O : An A, and so on. The abstract U {x|x = x} consisting of all ob jects of the theory S is said to be universal. Note that operating with abstracts, we always stay within the framework of formulas of the S set theory. 7.2. The abstract interpretation of a first-order theory in a set theory. A set theory S is said to be finitely-closed ( closed up to finite col lections ) if in the theory S , some formula on(x) defines natural numbers as the ob jects of this theory, and for every natural number n 1 every abstract F that is a mapping from the ob ject n into the universal abstract U is an ob ject of the S theory. In a finitely-closed S set theory, we define the abstract {x|on(x)} consisting of all natural numbers. Therefore, in such a theory, abstracts s : A are defined. They can be called abstract infinite sequences of elements of the abstract A. Suppose that in a S set theory, by means of this theory, we have selected some abstract D {x|(x)}. Let S be some fixed finitely-closed set theory with some selected abstract D. An abstract interpretation of a first-order theory T in the finitely-closed set theory S with the selected abstract D is a pair M consisting of the abstract D and some correspondence I assigning to every predicate letter Pin some n-placed relation I (Pin ) in D, every functional letter Fin some n-placed operation I (Fin ) in D, and every constant symbol ai some element I (ai ) of D. Let s be some abstract infinite sequence x0 ,...,xq ,... of elements of the abstract D {x|(x)}. Define the value of a term t of the theory T on the sequence s under the abstract interpretation M of the theory T in the S set theory (in the notation tM [s]) by induction in the following way: -- if t -- if t -- if t tM [ s] vi , then tM [s] xi ; ai , then tM [s] I (ai ); F (t0 ,...,tn-1 ), where F is an n-placed functional symbol and t0 ,...,tn-1 are terms, then I (F )(t0 M [s],...,tn-1 M [s]). follows that for the term t F (t0 ,...,tn-1 ), we have always an element of the abstract D, i. e., it is some sequence s under the abstract interpretation M of the notation M [s]) by induction in the following way:

Since I (F ) is an operation from Dn into D, it tM [s] D. Consequently, the value of a term is ob ject of the theory S . Define the translation of the formula on the theory T in the finitely-closed set theory S (in the -- if M -- if -- if -- if

(P (t0 ,...,tn-1 ), where P is a n-placed predicate symbol and t0 ,...,tn-1 are terms, then [s] ((t0 M [s],...,tn-1 M [s]) I (P )); (ì), then M [s] (ìM [s]); (1 2 ), then M [s] (M 1 [s] M 2 [s]); (vi ), then M [s] (x(x D M [x0 ,...,xi-1 ,x,xi+1 ,...,xq ,... ])).

On other formulas the translation is continued similarly to Sec. 1.3. This definition needs some explanation. For the formula (P (t0 ,...,tn-1 )), the symbol-string ((t0 M [s],...,tn-1 M [s]) I (P )) is a formula of the theory S . Actually, we have mentioned above that the values of the terms ti M [s] are ob jects of the theory S . Since the theory S is finitely-closed, it follows that the abstract v (t0 M [s],...,tn-1 M [s]) is an ob ject of the theory S . By definition, I (P ) is a subabstract of the abstract Dn . Therefore, the symbol-string (v I (P )) is, in fact, a formula of the theory S . It follows from the other items of this definition that as a result of the translation, we always obtain formulas of the theory S . Thus M [s] is a formula of the theory S . 5817


An abstract interpretation M is called an abstract model of the axiomatic theory (T, a ) in finitely-closed set theory (S, a ) with the selected abstract D if for every abstract sequence of D, the translation M [s] of every axiom of the theory T is a deducible formula (S, a ). All other definitions and assertions from Sec. 1.3 are transferred to the case of abstract under the corresponding insignificant changes. 8. Undeducibility of Some Axioms in LTS

the axiomatic s of elements in the theory interpretation

In this section, all proofs are given by the method of abstract interpretation described in the previous section. 8.1. The undeducibility of the axiom scheme of replacement. made the globalization of almost all main constructions used in naive set Now we need only to know if one can deduce the global axiom scheme ASR (the axiom scheme of replacement ). Let (x, y ) be a formula of Y as a free variable. Then xy y ((x, y ) (x, y ) y = y ) X Y In Secs. 5.2 and 5.4, we have theory. of replacement in the LTS: the LTS, and let not contain x X y ((x, y ) y Y ).

Statement 1. (1) If the LTS is consistent, then LT S + ìAS R is consistent. (2) If the LTS is consistent, then the axiom scheme ASR is not deducible in the LTS. Proof. (1) For n , consider the class U and the U -sequence u(n) from Theorem 5, Sec. 5. By their n uniqueness, we can denote them by U (n) and u(n) (Uk U (n)|k n +1)U (n) . Consider the assembly C {z |xy (x y U (x) z = x, y )}. It is clear that C is a correspondence from the class into the assembly V such that C n = Un for every n . Therefore, C can be written as the collection C U (n) V|n ]. Consider the assemblies D U (n)|n = {y |x (y U (x))} and R {y |x (y = U (x))}. By Theorem 5, m+1 n n+1 Sec. 5, U (m) = Um+1 = Um+1 Un+1 = U (n) D for any m n . Therefore, R D. Moreover, +1 U0 D implies D. By Corollaries 4 and 5 to Theorem 4, Sec. 5, the LTS is a finitely-closed set theory. Choose the assembly D in the capacity of the domain of abstract interpretation of the theory T LT S + ìAS R in the finitely-closed set theory S LT S . Define a correspondence I assigning to the predicate symbol in T the two-placed relation B {z |xy (x D y D z = (x, y ) x y )} on D, to the predicate symbol in T the one-placed relation R on D, and to the constants and a in T the elements and U0 of the domain D, respectively. Consider the abstract interpretation M (D,I ). Let s be an abstract sequence x0 ,...,xq ,... of elements of D. We will consider the translations M [s] of axioms and axiom schemes of the theory T on the sequence s under the interpretation M and will prove their deducibility in the S set theory. Instead of M [s] and M [s], we will write t and t for terms and formulas , respectively. The assembly D is transitive. Actually, if y D, then y U (m) for some m. By Axiom A7, y U (m) D. Moreover, if x y D, then x D. Actually, by Axiom A8, x y U (m), implies x U (m) D. We will often use these two properties in our proofs further. For simplifying the further presentation, we first consider the translations of some simple formulas. Let u and v be some classes in the LTS. The formula u v is translated into the formula (u v )t = ((ut ,v t ) B). By Corollary 5 to Theorem 4, Sec. 5, the assembly (ut ,v t ) is a class, i.e., there exists a class z such that z = (ut ,v t ). Therefore, similarly to the arguments from the proof of Statement 3, Sec. 6, we establish the first equivalence (u v )t ut v t . Further, similarly to the proof of Statement 3, Sec. 6, we establish the second equivalence (v w)t t wt . v This equivalence immeditely implies the third equivalence (v = w)t v t = wt . 5818


We will now write not the literal translations of axioms and axiom schemes but their equivalent variants which are obtained by using the proved equivalences (u v )t ut v t , (v w)t v t wt and (v = w)t v t = wt . We will denote these equivalent variants using the sign " " over them. At 1. y Dz D((y = z ) (X D(y X z X ))). This formula is directly deduced from the axiom of extensionality A1 in the LTS.

ASt 2. Let (x) be an X -predicative formula in the LTS such that the substitution (x y ) is admissible and does not contain Y as a free variable. Then X D(Y D(y D((y Y ) (y X (y ))))), [s ] in which by s we denote the corresponding change of the where denotes the formula M sequence s under the translation of the quantifier over-formulas X (... ), Y (... ), and y (... ) indicated above. Let X D. Let us verify that the formula is also X -predicative. Suppose that the subformula x(x X ... ) occurs in the formula . Then the subformula occurs in the formulas . By the proved equivalence, taking into account the external quantification by X , the formula is equivalent to the formula x(x D x X ... ). If x X , then it follows from the transitivity of D that x D. Consequently, the formula is equivalent to the formula x(x X ... ). Substituting the subformula in the formula by the equivalent formula , we obtain the formula , which is equivalent to the formula and contains the subformula x(x X ... ). Making this substitution with all subformulas of the form in the formula , we obtain the formula ½ , which is equivalent to the formula and contains only subformulas of the form . Now suppose that the formula contains the subformula x(x X ... ). Then the subformula occurs in the formula . Therefore, it also occurs in the formula ½ . As above, the formula is equivalent to the formula x(x D (x X ... )). Consider the formula . We deduce from it the formula (x D (x X ... ). If x X , then, by the transitivity of D, x X D implies x D. This means that and x X imply the subformula (x X ... of the formula and, therefore, the formula x(x X ... ). By the theorem of deduction in the LTS, we deduce the formula . Conversely, consider the formula . By LAS12, it implies the subformula (x X ... ). By LAS1, the formula is deduced. By the deduction theorem in the LTS, the formula is deduced. By the generalization rule, the formula x( ) is deduced. In virtue of LAS13, the formula is deduced. Thus, in the LTS, we deduce the equivalence of the formulas and . Substituting the subformula in the formula ½ by the equivalent formula , we obtain the formula ½ , which is equivalent to the formula ½ and contains the subformula x(x X ... ). Making this substitution with all subformulas of the form in the formula , we obtain the formula ½½ , which is equivalent to the formula and contains only subformulas of the form and . Consequently, the formula ½½ is X -predicative. Therefore, by AS2 from the LTS, X D implies the formula (Y (y (y Y (y X ½½ (y ))))). Consider the formula (y Y (y X ½½ (y )))). By LAS11, the formula implies the formula (y Y (y X ½½ (y ))). By LAS1, from , we infer the formula (y D ). Consequently, from X D and , we infer the formula (y D (y Y (y X (y )))). By the generalization rule, we infer the formula (y D(y Y (y X (y )))). Moreover, from , we infer the formula Y X . Since X D, by the second property of the totality D proved above, we obtain Y D. Therefore, from X D and , we infer the formula Y D . By LAS12 is implied the formula Y D. Thus, by the deduction theorem, from X D, we infer the formula . By the generalization rule, we infer the formula Y ( ). Then, by LAS14, from X D, we infer the formula . 5819


Since we have already deduced above the formula under the condition X D, by the implication rule, we infer the formula . By the theorem of deduction in the LTS, the formula (X D ) is deduced. Therefore, by the rule of generalization, the formula ASt 2 is deduced. / At 3. Z D((x D(x Z )) z = ). Fix the condition Z D. Consider the formula x(x D x Z ). If x Z , then, by the / property of transitivity, x D and then implies x Z . If x Z , then obviously implies x Z . / / / Therefore, under our condition, we infer that implies x Z . By the rule of generalization, implies / x(x Z ). By Axiom A3, implies Z = . By the theorem of deduction Z D implies the formula / Z = . Conversely, by A3, Z = , implies x(x Z ). Therefore, Z D and Z = imply the / formula (Z = ). Thus, the condition Z D implies the formula ( Z = ). By the theorem of deduction, we infer the formula Z D ( Z = ). Therefore, by the rule of generalization, we infer the formula At 3. At 4. U DV D((U = V (U D V R)). Let U = V . If U R, then U = Un for some n . Then V = Un implies V R. And vice versa. Therefore, U R V R. At 5. U0 R U D(U R U0 U )). Consider the formulas (x, y ) (x y = U (x)) and x(x, y ). Since 0 U (0) = U (0), by LAS12 in the LTS, we infer the formula x(x U (0) = U (x)), i. e., the formula (y U (0)). By definition, this means that U (0) R. If U R, then U = U (n) for some n . If n = 0, then U (0) = U . If n > 0, then, as was indicated at the beginning of the proof, U (0) U (n). By the axiom of transitivity A7, U (0) U (n) = U . By the theorem of deduction in the LTS, we infer the formula (U R U (0) U ). By LAS1, we infer the formula (U D ) and, by the rule of generalization, we infer the formula U D. Therefore, we infer the formula At 5. At 6. X DU D(U R X U ). From X D, it follows that X U (n) for some n . In the same way as in the deduction of At 5, we prove the deducibility of the formula U (n) R D. Consequently, from X D, we infer the formula (U (n) D U (n) R X U (n)). By LAS12, we infer the formula U D(U R X U ). By the theorem of deduction in the LTS, we infer the formula (X D ). By the rule of generalization, we infer At 6. At 7. U D(U R X D(x U x U )). This formula is deduced from the axiom of transitivity A7 in the LTS. At 8. U D(U R X DY D(X U Y X Y U )). This formula is deduced from the axiom of subset A8 in the LTS. At 9. U D(U R X D(X U PU (X ) U )), where the U -class Z PU (X ) is defined from the formula Z D(y D((y Z ) (y U y X ))). First, verify that if U R, X D, and X U , then Z = PU (X ) Y . Let y Z . Since Z D, by the proved-above transitivity, y D. But then y D and y Z imply y U y X , i.e., y Y . Conversely, let y Y , i.e., y U y X . Since X D, by the proved-above second property of the assembly D, we obtain y D. From U R, it follows that U is a universal class. Therefore, by the axiom of subset A8, y X U implies y U . But then y D, y U , and y X imply y Z , which proves the required equality. By Axiom A9, X U implies Z = Y U . From here, by logical means, we infer the formula At 9. At 10. U D(U R X DY D(X U Y U (X U Y ) U )), where the U -class Z (X U Y ) is defined from the formula z D(y D((y z ) (y U (y X y Y )))). 5820


In the same way as in the deduction of the formula At 9, we verify that the conditions U R, X D, Y D, X U , and Y U imply the equality Z = X U Y , where U is a universal class. By Axiom A10, Z = X U Y U . From here, we infer the formula At 10. At 11. U D(U R X DY Dz D((X U Y U (z (X U Y ) ) (x D(x X z x U ))) ((rngU z ) U ))), where: -- the U -- the U -- the Y U -class Z1 (X U Y (u Dv D(u X U -class Z2 Z2 (x) y Y x, y z ))), U U -class Z3 (rngU z ) (x D(x X x, y ) is defined from the formula Z1 D((y D((y Z1 ) (y v Y y = u, v ))))), U z x is defined from the formula Z2 D(y D((y Z2 ) (y is defined from the formula Z3 D(y D((y Z3 ) (y U y t z ))))). U

As above, we verify that the conditions U R, u D, v D, u U , and v U successively imply the equalities {u} = {u}U , {u, v } = {u, v }U , and u, v = u, v U , where U is a universal class. By U U U Lemma 2, Sec. 2, u, v U implies u, v = u, v U U . U From here, in turn, we infer that the conditions U R, X D, Y D, X U , Y U , x D, and x X imply the equalities Z1 = X U Y , Z2 = z x , and Z3 = rngU z . Let us have one more condition x D(x X z x U ). Since z is an U -correspondence from X into Y U , it follows that z is an U -correspondence from X into U . If x X D, then from the transitivity of D, we infer that x D. Therefore, the additional condition implies z x = z x U . Since X U , by the axiom of full union A11, it follows that Z3 = rngU z U . From here, by logical means, we infer the formula At 11. At 12. U D(U R X D(X U X = x D(x X (x U X ) = ))), where the U -class Z (x U X ) is defined from the formula Z D(y D((y Z ) (y U (y x y X )))). Let us verify that the conditions U R and X D imply the equality Z = x U X Y . Let y Z . Since X D, it follows that y D. But in this case, y D and y Z imply y U y x y X , i.e., y Y . Conversely, let y Y , i.e., y U y x y X . Since y X D, it follows that y D. Consequently, y Z , which proves the required equality. From U R, it follows that U is a universal class. By the axiom of regularity A12, for = X U , there exists x X such that Z = Y = . Since x X D, it follows that x D. From here, by logical means, we infer the formula At 12. At 13. X D(X U0 X x D(x X ((x U0 {x}U0 ) X ))), where: -- the U0 -class Z1 Z1 (x) (x U0 {x}U0 ) is defined from the formula Z1 D(y D((y Z1 ) (y U0 (y x y {x} 0 )))), U -- the U0 -class Z2 Z2 (x) {x} 0 is defined from the formula Z2 D(y D((y Z2 ) (y U U0 y = x))). From the conditions X D, X U0 = a, x D, and x X it follows that Z2 = {x}a, and, therefore, Z1 = x a {x}a. Consider the a-set from the axiom of infra-infinity A13. It is clear that a = U0 D. Since possesses the property U0 x (Z1 (x) ), it follows that in the LTS the formula At 13 is deduced. At 14. U D(U R X D(X U X = z D((z D(Y PU (X ) \ {}U ) z (Y ) Y )))), where: PU (X ) \ {}U U X ) Y

-- the U -class Z1 Z1 (X ) (PU (X ) \ {}U ) is defined from the formula Z1 D(y D((y / Z1 ) (y U (y PU (X ) y {} )))), U is defined from the formula Z U Y, Z z , -- the U -class Z2 Z2 (Y ) z (Y ) 2 2U 5821


-- denotes the formula M [s ] in which s denotes the corresponding change of the sequence s under the translation of the quantifier over-subformulas U (... ), X (... ), z (... ), and Y (... ), indicated above. Fix the conditions U U, U R, X D, and X U . We established above that under these conditions, PU (X ) = PU (X ) and {} = {}U . From here, by the transitivity of D, as above, we infer U Z1 = PU (X ) \ {}U T . From U R, it follows that U is a universal class. Consequently, by A9, PU (X ) U . Therefore, T U by A8. If Y D and Y Z1 , then Y T U implies Y U . As was established above, Z2 U and Y U imply Y, Z2 = Y, Z2 U . Then Y, Z2 U z implies Z2 z Y . From here and from the previous U conditions, we cannot yet infer that Z2 = z (Y ). Consider the formula (z T U X ). It is the conjunction of the three following formulas: 1 (z T U X ), 2 (domU z = T ), and 3 (x(x T y (y X y (y X ( x, y u z x, y U z y = y ))))). Therefore, = . Since 1 = (u(u z u U xy (x T y X u = x, y U ))), 1 2 3 it follows that (u D(u z u U x Dy D(x Z1 y X u = x, y ))). Similarly, 1 U 2 = (x(x T x U x T y (y X x, y U z ))) implies (x D(x Z1 x 2 U x Z1 y D(y X x, y z ))). U Finally, (x D(x Z1 y D(y X y D(y X ( x, y z x, y z 3 U U y = y ))))). By the properties of transitivity for x, y , and y in the formulas , , and , we have x, y , y U . 1 2 3 Therefore, by the proved above (see the proof of deducibility of At 11), in this formulas, we have the equalities Z1 = T , x, y = x, y U , and x, y = x, y U . It follows from here that the formulas U U , , and differ from the formulas 1 ,2 , and 3 , respectively, only by the bounded quantifier 1 2 3 prefixes ... D and ... D. For X , by the axiom of choice A14, there exists z such that (z PU (X ) \ {}U U X ) Y (Y PU (X ) \ {}U z (Y ) Y ). Therefore, in the LTS, we infer the formula = 1 2 3 and, consequently, the formulas 1 ,2 , and 3 . Let u D and u z . Then from the formula 1 , we infer that there exist x T and y X such that u = x, y U . Since x T U and y X U , by the transitivity property, it follows that x, y U D. This means that under the given conditions u D and u z , in the LTS we infer the formula (u U x Dy D(x T y X u = x, y U )). Applying the deduction theorem and the deduction rules two times, we infer the formula . 1 Let x D and x Z1 = T . Then from the formula 2 , we infer that for x, there exists y X such that x, y U z . From y X D, by the transitivity of D, it follows that y D. This means that under the given coditions x D and x T , in the LTS, we infer the formula (x U x T y D(y X x, y U z )). From here, as above, we infer the formula . 2 Let x D, x Z1 = T , y D, y X , y D, y X , x, y U z , and let x, y U z . Then from the formula 3 , we infer that y = y . In turn applying several times the deduction theorem and the deduction rule, we infer the formula . 3 Thus, the formula is deduced. Since z T U X , it follows that z Y = {z (Y )}U . Consequently, from Z2 U {z (Y )}U , we conclude that Z2 = z (Y ). Therefore, for the U -mapping z , the conditions Y D and Y Z1 = T imply Z2 = z (Y ) Y . Since T U and X U , by Lemma 3, Sec. 2, it follows that, T U X U . By Axiom A8, from z T U X , it follows that z U D. All this means that from axiom A14, we deduce the existence of an ob ject z satisfying the formula from which we infer the formula Y D(Y Z1 Z2 Y ). For the same reason, in the LTS, 5822


from the fixed conditions, we infer the formula z D . In turn, applying several times the deduction theorem and the generalization rule, as a result, we infer the formula At 14. Consider now the translation of the axiom scheme of replacement ASR. ASRt . Let (x, y ) be a formula of the theory T that does not contain Y as a free variable. Then x Dy Dy D( (x, y ) (x, y ) y = y ) X DY Dx D(x X y D( (c, y ) y Y )), where and denote the formulas M [s ] and M [s ], respectively, in which by s we denote the corresponding change of the sequence s under the translation of the quantifier over-formulas x(... ), y (... ), and y (... ) indicated above, and by s indicated above we denote the corresponding change of the sequence s under the translation of the quantifier over-formulas X (... ), Y (... ), x(... ), and y (... ). Denote the first part of this scheme by and the second part by . Then AS Rt = ( ). Therefore, the equivalence (ì( )) ( ì ) implies (ìAS R)t = (y Dy Dy D( (x, y ) (x, y ) y = y )) (X DY Dx D(x / X y D( (x, y ) y Y ))). Further, the first part of this scheme we will denote by , and the second part by . For the adduced below concrete formula the symbol-strings and will be formulas of the LTS. Consider the following formulas of the theory T : -- (x, y , z ) (x a y y (z x + 1 y y ) k x + 1(z (k ) ) z (0) = a k x +1(l x +1(k l z (k ) z (l))) V ((V z (0) V V y ) k x +1(V = z (k )))), -- (x, y ) z (x, y , z ), where x + 1 denotes the class x a {x}a. For the formula we have the following translations: x +1 y y ) k D(k (x +1) z (k )(k -- (x, y ) z D(x a y y R (z (x +1) l D(l (x +1) (k l z (k ) z (l) ))) V D((V R (z (0) V ) V y ) k D(k (x +1) (V = z (k ) ))), x +1 y y ) k D(k (x +1) z (k ) -- (x, y ) z D(x a y y R (z = a k D(k (x +1) l D(l (x +1) (k l z (k ) z (l) ))) V R) z (0) D((V R (z (0) V ) V y ) k D(k (x +1) (V = z (k ) )))),

where , , , and denote the terms M [s ] and M [s ] and the formulas M [s ] and M [s ] in which s and s denote the corresponding changes of the sequences s and s under the translation of the quantifier over-formula z D(... ). Let us verify that = and = . By the formula On(x) defined in Sec. 6.1, the class is assigned by the formula !z (On(z ) z = x(On(x) z = x a {x}a) y ((On(y ) y = x(On(x) y = x a {x}a)) z y )), which is deduced in the theory T . Therefore, by what was the three equivalences proved above, the value is defined from the formula !z D(OnD (z ) z = z a x D(OnD (x) x a z = (x a {x}a) y D((OnD (y ) y = y a x D(OnD (x) x a y = (x a {x}a) )) z y )), because a is translated into a. Since the assembly D is transitive, by a direct verification, using the definition of the formula On(z ) from 6.1, we can prove that for z D, the equivalence onD (z ) On(z ) holds. When we verfied the deducibility of the formula At 13, we established that the conditions x D and x a imply the equality (x a {x}a) = x a {x}a. Therefore, the formula is equivalent to the formula , which differs from the formula by only bounded quantifier prefixes ... D and ... D. But since the formula and the formula contain the subformulas z a, x a, and y a, which immediately imply the restrictions z D, x D, and y D, it follows that in the LTS, we infer the equivalence . From the equivalence , it follows that = . In just the same way, it is verified that = . 5823


We have verified above that under the conditions x , a, and a D, by the transitivity D, the equality (x + 1) = x a {x}a = x + 1 holds. We also verified that under the condition y R, the x +1 y y ) holds. Therefore, z (i) = z (i) for every i x +1. equivalence (z x +1 y y ) (z The same holds for the variant with the sign . Therefore, (x, y ) and (x, y ) are equivalent to the same formula (x, y ) z D(x a y y R (z x +1 y y ) k D(k x +1 z (k ) R) z (0) = a k D(k x +1 l D(l x +1 (k l z (k ) z (l)))) V D((V D (z (0) V ) V y ) k D(k x +1 V = z (k ))))). In the same way as in the proof of Theorem 4, Sec. 6, in the LTS, we infer the formula xy y z z ( (x, y , z ) (x, y ,z ) y = y z = z ), which means that y and z are uniquely defined by x. We also infer the formula xx y y z z (( (x, y , z ) (x ,y ,z ) x x ) k k +1(z (k ) = z (k )) (z (x +1) = y ))), which means that for m n, the sequence u(n) continues the sequence u(m) and U Now, let us deduce the formula
n m+1

= U (m).

xy z ( (x, y , z ) k ((x +1) \ 1)x y z (x x (x ,y ,z ) z (k ) = y )), which means that all members of the sequence u(n) starting from the first one are constructed from the previous classes U (m) for m n. Denote the formula k ((x +1) \ 1)x y z (x x (x ,y ,z ) z (k ) = y ) by (x, y , z ). We will infer this formula under the condition (x, y , z ). The formula (x, y , z ) postulates that x is a natural number, y is a universal class greater than a and there exists a finite y -sequence of universal classes u(x) (yk y |k x +1)y such that y0 = a, yk yl for all k l x +1, and if V is a universal class and y0 V y , then V = yk for some k x + 1. By Theorem 5, Sec. 5, for every x such a sequence exists and is unique, and, moreover, u(x)|m +1 = u(m) for all m x. The formula (x, y , z ) has the form k (k (x +1) \ 1 x y z (x x (x ,y ,z ) z (k ) = y ). Let us show that from our conditions and the condition k (x + 1) \ 1, the formula (x, y , z , k ) x y z (x x (x ,y ,z ) z (k ) = y ) is deduced. Consider x such that x + 1 = k . This is possible, because 1 k . By Theorem 5, Sec. 5, for the given x there exist y and z such that (x ,y ,z ). Since x k x, it follows that x x. It remains to show that z (k ) = y , i. e., y = yk in the sequence u(x). Since (x ,y ,z ), it follows that a = y0 y , i. e., y0 y . Since y , there are only three possibilities: (1) y y ; (2) y = y ; (3) y y . In the first case, y = z (l) for some l x < x; but this is impossible; in the second case, the sequences u(x) and u(x ) must coincide, but this is impossible, because x < x. As a result, only case (3) y y is possible. Thus, y0 y y , and, consequently, by the condition, y = ym for some m x + 1. Let us show that m = k . Actually, if m < k , then ym = z (m), but this is impossible, because z (m) y for all m < k . If m > k , then, taking V yk , we obtain the condition y0 V y , which implies V = yl for l < k , but this is also impossible. Therefore, y = yk , i.e., z (k ) = y . Thus, under the conditions (x, y , z ) and k (x +1) \ 1, we infer the formula (x, y , z , k ), and, therefore, by the deduction theorem, under the condition (x, y , z ), we infer the formula k (x + 1) \ 1 (x, y , z , k ); from here, by the generalization rule, the formula (x, y , z ) is deduced. Then, applying once more the deduction theorem and the generalization rule, we obtain the required formula. Consequently, z (k ) R for all k x + 1. Take in the capacity of value of the variable X the class . Since a = U (0) D, it follows that D. Take any Y D. Then Y U (x0 ) for some x0 . This means that in the LTS, the formula xy (!z ( (x, y , z ) Y y ) is deduced. Denote the unique values of the variables y and z corresponding to the value x0 by y0 and z0 . From all this, it follows that the formula (x0 ,y0 ,z0 ) Y y0 is deduced. By definition, y0 R D. From the previous arguments, it follows that z0 (k ) R for any k x0 +1. It is clear that k D and l D. If V D and V R, then V , and, therefore, the conditions z0 (0) V and V y0 imply k D(k x0 +1 V = z0 (k )). Thus, in the LTS, the following formula is deduced: 5824


(x0 ,y0 ,z0 ) (x0 a y0 y0 R (z0 x0 + 1 y0 y0 ) k D(k x0 + 1 z0 (k ) R) z0 (0) = a k D(k x0 +1 l D(l x0 +1 (k l z0 (k ) z0 (l)))) V D((V R z0 (0) V V y0 ) k D(k x0 +1 V = z0 (k ))))). Since z0 x0 + 1 y0 y0 , by Axiom A11, it follows that, P rngy0 z0 y0 . Therefore, z0 ((x0 + 1)0 P ) Q. Moreover, x0 + 1 a y0 implies x0 + 1 y0 . By Lemma 3, Sec. 2, Q y0 . y Consequently, by Axiom A8, z0 y0 D. Hence we obtain z0 D. Therefore, in the LTS, the formula (x0 ,y0 ) = z D (x0 ,y0 ,z0 ) is deduced. Moreover, the formula Y y0 was deduced. By the axiom of / regularity A12, the formula y0 Y is deduced. / For the same reason, we deduced the formula (x0 ,y0 ) y0 Y . Since x0 D, x0 , and y0 D, by logical means, we infer the formula x D(x y D( (x, y ) y Y ). Since D and Y D, then by logical means, we infer the formula . Now let x, y , y D, x , y , a y , y R, and let y R. Let us infer the formula (x, y ) (x, y ) y = y . Consider the condition, ²(x, y , y ) (x, y ) (x, y ). According to this condition for a natural number x, there exist universal classes y and y from R greater than a and finite sequences of universal classes u(x) (yk y |k x + 1)y and u (x) (yk y |k x +1)y such that y0 = y0 = a, yk yl and yk yl for any k l x +1, and if V and W are universal classes from R and y0 V y , y0 W y , then V = ym , W = yl for some m, l x + 1. Suppose that y = y . Since y and y are universal classes, it follows that in this case either y y or y y . Suppose, for example, that y y . Set W y . We obtain W R a W W y , W = yl for some l x +1. Thus y = yl for l x + 1. Similarly, for any k < x + 1 there exists l(k ) < x + 1 such that yk = yl(k) . Since k x +1(yk y ), it follows that k x +1(yl(k) yl ), i. e., l(k ) l for all k x +1. Moreover, if k, m x +1 and k = m, then yl(k) = yl(m) . Consequently, there exists an inclusion of the set x + 1 into the set l x + 1, but this is impossible. The case y y is verified in just the same way. Consequently, y = y . Applying the deduction theorem, we deduce the formula ²(x, y , y ) y = y . Therefore, the formula (x, y ) (x, y ) y = y is deduced. From here, by logical means, the formula is deduced. As a result, in the theory S , the formula is deduced, which is equal to the formula (ìAS R)t with a given concrete formula . Since all the translations of the axioms of the theory T turned out to be deducible formulas of the theory S , it follows that the theory T is consistent. (2) We will argue in the naive propositional logic with the symbol of implication . Denote by a and a the totalities of axioms of the theories T LT S + ìAS R and S LT S , respectively. AS R) and B cons(S ) (a AS R). Then Consider the propositions A cons(S ) ì(a ìA = cons(S ) ìì(a AS R). Using LAS10, we obtain ìA B . It is clear that B (a AS R) and a ìAS R. Therefore, the proposition B (a AS R) (a ìAS R), i.e., the expression B ìcons(T ) is valid. By the deduction rule, ìA ìcons(T ). According to item (1) of our statement, the proposition cons(S ) cons(T ) is valid. Therefore, B cons(T ) is valid. By the deduction rule, we have ìA cons(T ). Thus, the proposition (ìA cons(T )) (ìA ìcons(T )) is deduced. Applying the tautology (ìA C ) (ìA ìC ) A (see [21], chap. 1, ç 7), we infer the proposition A. Using a more complicated abstract interpretation, one can also prove that if the LTS is consistent, then the axiom scheme ASR is not deducible in the LTS+ICU. In Secs. 5.2 and 5.4, we have proved the closureness of the assembly V of all classes in the LTS with respect to all basic finite set-theoretical operations. Therefore, in the assembly V we can define such basic mathematical systems as groups, topological spaces, automata, and other on classes, and also define morphisms between them. For the same reason in V, we can consider abstract categories of all such mathematical systems and morphisms between them. 5825


From the undeducibility in the LTS of the global axiom scheme of replacement, it follows that the assembly V does not possess the fourth of the five properties of the EresmanníDedeckeríSonneríGrothendieck universe listed in the Introduction and necessary for developing in this universe valuable category theories. Therefore, the theory of abstract categories in the LTS will be essentially poorer than the theory of (local) categories in the LTS. In particular, these abstract categories of mathematical systems will not be closed with respect to such Ai |i I of the collection Ai |i I infinite operations as the sum Ai |i I and the product of ob jects Ai of these categories and consequently will be abstract categories without direct and inverse limits (see [5], ch. 2, ç 1; chap. 3, ç 2). On the contrary, in the ZF or NBG set theories with the axiom of universality abstract categories of mathematical systems from the point of view of naive category theory do not differ absolutely from local U -categories of mathematical systems. 8.2. The nondep endence of axiom ICU on the axioms of the LTS. In Sec. 6, we have compared the LTS with the ZF theory with some additional axioms. The fact that axiom IC postulating the existence of an inaccessible cardinal is independent of the axioms of the ZF theory is well-known (see [19], 13). Consequently, Axioms IS IC and IS IC2 postulating the existence of infinite sets of inaccessible cardinals are also independent of the axioms of the ZF theory. It remains only to clarify the nondependence of Axiom IC U postulating the existence of an infinite class of universal classes on the axioms of local theory of sets. Statement 2. (1) If the LTS is consistent, then LT S + IC U is consistent. (2) If the LTS is consistent, then Axiom ICU is not deducible in LTS. Proof. (1) By Lemma 1, Sec. 6, Axiom ICU is equivalent to Axiom ITCU. Therefore, we will consider the equivalent theory T LT S + ìIT C U . Consider the abstract interpretation M (D,I ) of the theory T in the finitely-closed set theory S LT S , described in the proof of Statement 1. In the proof of Statement 1, we have established that the interpretation M is an abstract model of the LTS in the S set theory. In virtue of Lemma 2, Sec. 6, in the conjunctive kernel of Axiom ITCU, we can insert one more formula a Y . Therefore, consider the formula IT C U Y (U (U Y U ) a Y U V (U U V V Y U Y ) V (V Y W (W Y V W ))). The translation of this formula on some abstract sequence s of elements of the assembly D under the interpretation M has the form of the formula M [s] = Y D(U D(U Y U R) a Y U DV D(U R U V V Y U Y ) V D(V Y W D(W Y V W ))). Suppose that the condition is fixed and consider a class E D the existence of which follows from n this condition. Consider the classes An {x U (n)|k n +1(x = Uk )}, consisting of all members of n the U (n)-sequences u(n) from Theorem 5, Sec. 6. Further, along with Un , we will write Un . Let us prove by the natural induction that An E for every n . Consider the assembly X {x|x 0 Ax E }. If n = 0, then U0 E implies A0 {x U (0)|k 1(x = Uk )} E . Therefore, 0 X. n Let n X, i. e., Uk E for every k n + 1. By the property of the class E , there exists V D such n+1 n n that V E and Un V . Moreover, Un Un = Un +1 Un+1 Un+1 . If Un+1 = V , then Un+1 E . Let Un+1 V . In the proof of Theorem 5, Sec. 6, we have established that Un+1 = U (n) R. Since V E , by the property of the class E , we conclude that Un+1 E . Finally, let V Un+1 . Then V D and V E implies V R. Consequently, V is a universal class. From V Un+1 U (n + 1), by the axiom of universality, we infer that V U (n + 1). Therefore, by the property of incompressibility from Theorem 5, n n Sec. 6, the condition U0 +1 = a V U (n + 1) implies the equality U = Uk +1 for some k n +2. From n+1 n n n V Un+1 , it follows that k < n + 1. Hence Un +1 = Un Un V = Uk +1 implies n < k < n + 1, but this is impossible. From the obtained contradiction, we infer that the third case V Un+1 is impossible. By Proposition 4, Sec. 6, and Theorem 4, Sec. 6, there is no other possibilities, except the considered three 5826


n n cases. In the first and the second cases, we obtain Un+1 E . Moreover, Uk +1 = Uk E for all k n +1. Therefore, An+1 E implies n +1 X. By the principle of natural induction in the LTS (Theorem 2, Sec. 5), X. Thus, from the formula , we deduced the formula x (Ux E ). Moreover, from , one can / infer E D. Consequently, E U (m) = Um+1 for some m . Therefore, Um+1 E . This means that from the formula ì is inferred. By the theorem of deduction, in the theory S , we deduce the formulas ( ) and ( ì). Applying LAS9 and the logical explicit axiom ( ) (( ì) ì ), we consecutively deduce the formulas ( ì) ì and ì . The last formula is equal to the formula M (ì)[s]. Therefore, M is an abstract model of T in S . (2) The proof is similar to the proof of assertion (2) from Statement 1.

Thus, ICU does not depend on axioms of the LTS, i. e., is actually a new axiom for the LTS. Corollary. If the LTS is consistent, then the assertion (3) from Proposition 3, Sec. 6, is not deducible in the LTS. It follows from here that in the LTS there is only a countable assembly of universes, constructed in Theorem 5, Sec. 5, and there are no means to continue it further on like what was done in assertion 3) from Proposition 3, Sec. 6. 8.3. Lo cally-minimal theory of sets. A local theory of sets with an additional axiom, which states that infinite class of universes does not exist, will be called a local ly-minimal theory of sets (LMTS), i.e. LM T S LT S + ìIC U . Statement 2 implies that LTS and LMTS are mutually consistent. In LMTS, the assembly U of all universal classes has the following complete description.
n Theorem 1. In LMTS, an assembly sequence (u(n)|n ) of finite U (n)-sequences u(n) (Uk U (n)|k n + 1)U (n) of universal classes from Theorem 5, Sec. 5, includes al l universal classes; more n strictly, U (U n (U = Un )). n n (U = Un )}. Suppose that U = U, i.e., there exists Proof. Consider an assembly U {U |U . a universal class X such that X U / n n Fix numbers n and k n + 1. Suppose that X = Uk . Then by Theorem 5, Sec. 5, X = Uk = k U , but this is not true. Therefore, X = U n for all n and k n + 1. By Theorem 4, Sec. 5, and Uk k n n n Proposition 4, Sec. 5, either X Uk or Uk X . Suppose that X Uk . By Corollary 2 to Proposition 4, n n n n Sec. 5, U0 = a X Uk . By Axiom A8, from LTS, we have U0 Uk . Since k n, we have n 1. n-1 n U n - U (n - 1). By the prop erty of incompressibility from Theorem 5, = a X Uk Thus, U0 n Sec. 5, X = Uln for some k n + 1. But we have proved above that this is impossible. This contradiction n implies that Uk X for all n and k n +1. Therefore, according to Proposition 3, Sec. 6, we deduce Axiom ICU, but this is impossible if LMTS is consistent. Consequently, our assumption is not true and U = U.

We have proved that LMTS satisfies the following two properties: (1) it has (xU (2) it has ZF + the property of universal comprehension, which is expressed as the universality axiom A6 (x U U )); a countable metasequence (assembly) of all universes. Neither the ZF + U theory nor the U ( ) theory (see Introduction) satisfy these two properties.

Moreover, Statement 1 implies that LMTS is strictly weaker than the ZF + U and ZF + U ( ) theories. Therefore, LMTS satisfies Conditions (1)í(3) given in the Introduction. Thus, this theory is more natural for category theory than the ZF + U and ZF + U ( ) theories. 5827


REFERENCES 1. P. V. Andreev, E. I. Bunina, V. K. Zakharov, and A. V. Mikhalev, "The foundation of category theory within the framework of the local theory of sets," In: International Algebraic Conference. Abstracts of Reports [in Russian], St. Petersburg (2002), pp. 10í11. 2. G. Blanc and A. Preller, "Lawvere's basic theory of the category of categories," J. Symbol. Logic, 40, 14í18 (1975). 3. G. Blanc and M. R. Donnadieu, "Axiomatisation de la cat‡ egorie des cat‡ egories," Cahiers de topologie et g‡ ‡ eometrie diff‡ entiel le, 17, 135í170 (1976). er 4. N. Bourbaki, Th‡ eorie des Ensembles, Hermann, Paris (1960). 5. I. Bucur and A. Deleanu, Introduction to the theory of categories and functors, Mir, Moscow (1972). 6. N. da Costa, "On two systems of set theory," Proc. Koninkl. Nederl. Akad. Wet., Ser. A, 68, No. 1, 95í98 (1965). 7. N. da Costa, "Two formal systems of set theory," Proc. Koninkl. Nederl. Akad. Wet., Ser. A, 70, No. 1, 45í51 (1967). 8. N. da Costa and A. de Caroli, "Remarques sur les universe d'EhresmanníDedecker," C.R. Acad. Sci. Paris, S‡ A., 265, 761í763 (1967). er. 9. P. Dedecker, "Introduction aux structures locales," Col l. G‡ eom. Diff. Glob. Bruxel les, 103í135 (1958). 10. C. Ehresmann, "Guttungen von lokalen strukturen," J.-Ber. Deutsch. Math. Verein, 60, No. 2, 49í77 (1957). 11. S. Eilenberg and S. MacLane, "General theory of natural equivalences," Trans. Amer. Math. Soc., 58, 231í294 (1945). 12. S. Feferman, "Set-theoretical foundations of category theory," Lect. Notes Math., 106, 201í247 (1969). 13. A. Fraenkel, "Zu den Grandlagen der CantoríZermeloschen Mengenlehre," Math. Ann., 86, 230í237 (1922). 14. P. Gabriel, "Des cat‡ egories ab‡ eliennes," Bul l. Soc. Math. France, 90, 323í448 (1962). 15. R. Topoi Goldblatt, The Categorial Analysis of Logic, NorthíHolland Publishing Company, AmsterdamíNew YorkíOxford (1979). 16. W. S. Hatcher, The Logical Foundations of Mathematics, Pergamon Press, Oxford (1982). 17. H. Herrlich and G. Strecker, Category Theory. Introduction, Heldermann Verlag, Berlin (1979). 18. J. Isbell, "Structure of categories," Bul l. Amer. Math. Soc., 72, 619í655 (1966). 19. T. J. Jech, Lectures in Set Theory with Particular Emphasis on the Method of Forcing, Springerí Verlag, BerliníHeidelbergíNew York (1971). 20. J. L. Kelley, General Topology, Van Nostrand Company, TorontoíNew YorkíLondon (1957). 21. A. N. Kolmogorov and A. G. Dragalin, Introduction in Mathematical Logic [in Russian], MGU, Moscow (1982). 22. A. N. Kolmogorov and A. G. Dragalin, Mathematical Logic. Additional Chapters, [in Russian], MGU, Moscow (1984). 23. K. Kuratowski and A. Mostowski, Set Theory, Polish Scientific Publishers, Warzawa (1967). 24. F. W. Lawvere, "The category of categories as a foundation for mathematics," In: Proceedings of the Conference on Categorical Algebra, SpringeríVerlag, Berlin (1966), pp. 1í20. 25. S. MacLane, Local ly Smal l Categories and the Foundations of Set Theory, Symposium, Warsaw (1959), pp. 25í43. 26. S. MacLane, "One universe as a foundation for category theory," Lect. Notes Math., 106, 192í200 (1969). 27. S. MacLane, Categories for Working Mathematician, SpringeríVerlag, Berlin (1971). 28. E. Mendelson Introduction to Mathematical Logic, Van Nostrand Company, TorontoíNew Yorkí London (1971). 29. J. Sonner, "The formal definition of categories," Math. Z., 80, 163í176 (1962). 5828


30. V. K. Zakharov and A. V. Mikhalev, "The local theory of classes and sets as a foundation for category theory," In: Mathematical Methods and Applications. Proceedings of the 9th Mathematical Lectures MGSU [in Russian], MGSU, Moscow (2002), pp. 91í94. 31. V. K. Zakharov and A. V. Mikhalev, "On the concept of a mathematical system," Fund. Prikl. Mat., 4, No. 3, 927í935 (1998). 32. V. K. Zakharov and A. V. Mikhalev, "Mathematical systems," In: Proceedings of the International Algebraic Conference, Walter De Gruyter Publishers, Berlin (2000), pp. 370í383. 33. E. Zermelo, "Untersuchungen uber die Grundlagen der Mengenlehre, I," Math. Ann., 65, 261í281 è (1908).

5829