Двусортная теория классов и множеств, допускающая множества высказывательных формул

Кризис, возникший в наивной теории множеств в начале 20 века, привёл к возникновению таких строгих аксиоматических теорий, как теория множеств Цермело–Френкеля (ZF) и теория классов и множеств Неймана–Бернайса–Гёделя (NBG). Однако в то время как наивная теория множеств допускала рассмотрение множеств любых объектов, такое естественное понятие, как множество высказывательных формул, оказалось недопустимым в ZF и NBG. В связи с этим были развиты методы ассоциированного допущения, наиболее известным из которых является метод нумераций Гёделя. Данная статья посвящена решению задачи полноправного допущения. В ней излагается аксиоматика двусортной теории классов и множеств, позволяющей рассматривать множества высказывательных формул наравне с множествами объектных элементов.