Аксиомы NBG

[arseniiv]

Пусть дана теория NBG с двумя наборами переменных — для классов и для множеств. Первые пусть будут $a_1, a_3, a_5, \ldots$, а вторые — $b_2, b_4, b_6, \ldots$. Теперь попробую построить теорию с одним набором переменных-классов, а вы подскажите, так или не так.

В аксиомах каждую формулу вида $\forall b_i . \phi$ заменим на $\forall a_i .(\exists a . a_i \in a) \to \phi$, каждую формулу вида $\exists b_i . \phi$ заменим на $\exists a_i .(\exists a . a_i \in a) \wedge \phi$. Т. к. свободных переменных в собственных аксиомах NBG вроде бы нет, этих преобразований должно хватить. Что надо поправить; чего не хватает? (А может, это и вовсе ахинея? Я просто не совсем пойму, каким способом оставить только классы, ведь есть же схема аксиом выделения, где кванторами предиката, которому должны удовлетворять элементы класса, переменные-классы связаны быть не могут.)

-- Вс дек 09, 2012 18:56:01 --

(Ах да, $a$ — это какое-нибудь $a_k$, не встречающееся в $\phi$. Ну, дело-то не в этом.)

[Xaositect]

Да, с выделением надо что-то делать, если там разрешить классы, получается более сильная теория.

У Мендельсона в учебнике NBG вводится с одним сортом переменных и определяется $Set(x) \mathop{\leftrightarrow}\limits^{\mathrm{def}} \exists z (x\in z)$.
Там, насколько я помню, нет схем аксиом. Схему выделения в NBG можно свести к конечному числу аксиом из-за соответствия между предикатами и классами.
Делается это примерно так: даются отдельные аксиомы для существования пересечения, дополнения и проекции классов, технические аксиомы о существовании классов-отношений с переставленными элементами в кортежах и существование классов-отношений $M_{\in} = \{(x, y)| x \in y\}$ и $M_{=} = \{(x, x)\}$. Заменив в $\phi$ кванторы всеобщности на существование и дизъюнкции на конъюнкции, можно индукцией по сложности формулы построить класс $\{x|\phi(x)\}$ из базовых классов-отношений с помощью указанных операций.

[arseniiv]

А со схемой выделения никак? Мой способ не сработает?

[Xaositect]

Ну можно поставить ограничение, что в формуле $\varphi$ все кванторы должны быть вида $\forall a (Set(a) \to \dots)$ и $\exists a (Set(a) \wedge \dots)$. Но это скорее всего неудобно и, по-моему, некрасиво.