In quantified modal logic, the Barcan formula and the converse Barcan formula (more accurately, schemata rather than formulas) (i) syntactically state principles of interchange between quantifiers and modalities; (ii) semantically state a relation between domains of possible worlds. The formulas were introduced as axioms by Ruth Barcan Marcus, in the first extensions of modal propositional logic to include quantification.[1]
Related formulas include the Buridan formula.