Set theory as modal logic

A logical systemBM⁺ is proposed, which, is a prepositional calculus enlarged with prepositional quantifiers and with two modal signs, and These modalities are submitted to a finite number of axioms. is the usual sign of necessity, corresponds to transmutation of a property (to be white) into the abstract property (to be the whiteness). An imbedding of the usual theory of classesM intoBM⁺ is constructed, such that a formulaA is provable inM if and only if(A) is provable inBM⁺. There is also an inverse imbedding with an analogous property.