What is the Barcan Formula?

In 1946, Barcan introduced an axiom schema in modal predicate logic which is now referred to as the Barcan Formula (p. 2).

Barcan Formula

Axiom Schema 1. Let \(F\) be a predicate and let \(x\) be a variable. The Barcan Formula states that if it is possible that there exists an \(x\) that is an \(F\), then there exists an \(x\) that is possibly an \(F\).

\[ \Diamond \exists x Fx \rightarrow \exists x \Diamond Fx \]

For example, if it is possible that there exists a man who is mortal, then there exists a man who is possibly mortal.

The formula above is equivalent to the formula below. The formula below states that if all \(x\) are necessarily \(F\), then it is necessray that all \(x\) are \(F\).

\[ \forall x \square Fx \rightarrow \square \forall x Fx \]

For example, if all men are necessarily mortal, then it is necessary that all men are mortal.

Converse Barcan Formula

Axiom Schema 2. The Converse Barcan Formula states that if there exists an \(x\) that is possibly an \(F\), then it is possible that there exists an \(x\) that is an \(F\).

\[ \exists x \Diamond Fx \rightarrow \Diamond \exists x Fx \]

For example, if there exists a man who is possibly mortal, then it is possible that there exists a man who is mortal.

The formula above is equivalent to the formula below. The formula below states that if it is necessary that all \(x\) are \(F\), then all \(x\) are necessarily \(F\).

\[ \square \forall x Fx \rightarrow \forall x \square Fx \]

If it is necessary that all men are mortal, then all men are necessarily mortal.

References

Barcan, R. (1946). A Functional calculus of first order based on strict implication. Journal of Symbolic Logic, 11(1), 1-16. doi:10.2307/2269159