  Carnap’s work was primarily semantic, and resulted in a logic that did not correspond to any of the formal systems that had been studied up to this point. Axiomatically presented propositional modal logics were well-established, so it was important to see how (or if) they could be extended to include quantifiers and equality. At issue were decisions about what sorts of things quantifiers range over, and substitutivity of equals for equals. Quine’s modal objections needed to be addressed. Ruth Barcan Marcus began a line of development in (Marcus 1946) by formally extending the propositional system S2 of C. I. Lewis to include quantification, and developing it axiomatically in the style of Principia Mathematica. It was clear that other standard modal logics besides S2 could have been used, and S4 was explicitly discussed. The Barcan formula, in the form  \(\Diamond (\exists \alpha )\)A \(\supset (\exists \alpha )\Diamond\)A, made its first appearance in (Marcus  1946),[1]  though a full understanding of its significance would have to wait for the development of a possible-world semantics. Especially significant for the present article, her system was further extended in (Marcus 1947) to allow for abstraction and identity. Two versions of identity were considered, depending on whether things had the same properties (abstracts) or necessarily had them. In the S2 system the two versions were shown to be equivalent, and in the S4 system, necessarily equivalent. In a later paper (Marcus 1953) the fundamental role of the deduction theorem was fully explored as well. 