A two-sorted theory of classes and sets, admitting sets of propositional formulas

The crisis arisen in the naive set theory in the beginning of the 20th century brought to the origin of such strict axiomatic theories as the theory of sets in Zermelo–Fraenkel's axiomatics (ZF) and the theory of classes and sets in Neumann\ddf Bernays–Gödel's axiomatics (NBG). However, in the same time as the naive set theory admitted considering sets of arbitrary objects, such a natural notion as a set of propositional formulas became inadmissible in ZF and NBG. In connection with this circumstance some methods of associated admission were developed, the most known of which is the method of Gödel's enumeration. This paper is devoted to a solution of the full rights admission problem. An axiomatics of the two-sorted theory of classes and sets is exposed in it, which allows to consider sets of propositional formulas equally with sets of object elements.