  We show that first-order logic can be translated into a very simple and weak
logic, and thus set theory can be formalized in this weak logic. This weak
logical system is equivalent to the equational theory of Boolean algebras with
three commuting complemented closure operators, i.e., that of diagonal-free
3-dimensional cylindric algebras (Df_3's). Equivalently, set theory can be
formulated in propositional logic with 3 commuting S5 modalities (i.e., in the
multi-modal logic [S5,S5,S5]). There are many consequences, e.g., free finitely
generated Df_3's are not atomic and [S5,S5,S5] has G\"odel's incompleteness
property. The results reported here are strong improvements of the main result
of the book: Tarski, A. and Givant, S. R., Formalizing Set Theory without
variables, AMS, 1987.
