 The discussion of the Barcan Formula and its Converse has accompanied the development of quantified modal logic, as these formulas are linked both to the technical questions of how to combine Classical Quantification Theory with Modal Logic and how to define validity for quantified modal systems, as well as to the philosophical questions surrounding the variability of domains and the interpretations of the quantifiers. Proof theoretically, the most straightforward combination of classical quantification theory and modal logic makes both the Barcan Formula and its Converse theorems. Model theoretically, intra-model domain variability is a welcome generalization. We do not discuss here the technical solutions open to logicians who wish to build systems sound for variable domains, that is, systems that, like Kripke’s, do not allow proofs of the Barcan and its Converse (Deutsch 1994 and Linsky and Zalta 1994 contain useful overviews of the various technical options; see also the SEP entry on the possibilism-actualism debate).