In quantified modal logic, the Barcan formula and the converse Barcan formula state possible relationships between quantifiers and modalities. Modal logic, or (less commonly) intensional logic is the branch of logic that deals with sentences that are qualified by modalities such as can, could, might, may, must, possibly, and necessarily, and others. ...

The Barcan formula states:

.

In English, the statement reads, "'For all x, it is necessary that x is A', implies, 'It is necessary that for all x, x is A'". The formula tells us that for all x in the actual world, if x is such that it is A in every possible world, then in every possible world, all x in those worlds are such that they are A. The Barcan formula has generated some controversy because it implies that all objects which exist in this world must also exist in every possible world accessible to this one. So one interpretation is that no new objects can ever be created--they can only cease to exist. In other words, the domain of any accessible possible world is a subset of the domain of the actual world. This condition on domains is known as anti-monotonicity. (Anti-monotonicity and the Barcan formula are not equivalent in all modal systems.) The English language is a West Germanic language that originates in England. ...

The Barcan formula is most often used when adding quantifiers to Clarence Irving Lewis's modal logic S5, and was first proposed by Ruth Barcan Marcus. Clarence Irving Lewis ( April 12, 1883 - February 3, 1964) was a pragmatist philosopher. ... Modal logic, or (less commonly) intensional logic is the branch of logic that deals with sentences that are qualified by modalities such as can, could, might, may, must, possibly, and necessarily, and others. ... Ruth Barcan Marcus (born 1921) is the philosopher and logician after whom the Barcan formula is named. ...

The converse Barcan formula states

.

It implies the converse condition of the Barcan formula regarding the existence of objects in the actual world and all accessible possible worlds--i.e. that nothing in this world can cease to exist. The corresponding condition on domains is called 'monotonicity' and it states that the domain of this world is a subset of the domain of any accessible possible world.

It has been proved that if a frame is based on a symmetric accessibility relation then adding either one of the Barcan or converse Barcan formulas implies the other. In this case the corresponding condition on domains is an equivalence relation.

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