 The idea of quantified modal systems occurred to Ruth Barcan too. In “A Functional Calculus of First Order Based on Strict Implication” (1946a) she added quantification to Lewis’s propositional system S2; Carnap (1946) added it to S5. Though some specific semantic points about quantified modal logic will be considered, this entry is not focused on the development of quantified modal logic, but rather on the emergence of the model theoretic formal semantics for modal logic, propositional or quantified. For a more extensive treatment of quantified modal logic, consult the SEP entry on  modal logic.