In quantified modal logic, the Barcan formula is the formula
∀x. □P(x)→□ ∀x.P(x) \forall x.\, \Box P(x) \to \Box\, \forall x. P(x) ∀x.□P(x)→□∀x.P(x)
It is named after Ruth Barcan Marcus (1921-2012).