In quantified modal logic, the Barcan formula and the converse Barcan formula state possible relationships between quantifiers and modalities.

The Barcan formula states:

In English, the statement reads, "'For all x, it is necessary that A', implies, 'It is necessary that for all x, A'". The formula tells us that if everything is quantifiable in all other worlds then it would have to be necessary that everything is quantifiable in our world as well.

The Barcan formula is most often used when adding quantifiers to David Lewis's modal logic S5, and was first proposed by Ruth Barcan Marcus.

The converse Barcan formula states:

The Barcan formula has generated some controversy because some philosophers believe the formula violates the structure of the Kripke System. It implies that all objects which exist in this world (which the first is quantified over) must also exist in the sucessor states to this world (which the second is quantified over), so one interpretation is that no new objects can ever be created.

Related formulas include the Buridian formula, and the converse Buridian formula.