The Barcan formula is: :\forall x \Box Fx \rightarrow \Box \forall x Fx. In
English, the schema reads: :If every x is necessarily F, then it is necessary that every x is F. It is equivalent to :\Diamond\exists xFx\to\exists x\Diamond Fx. In English: :If it is possible that there exists an x that is F, then there exists an x that is possibly F. The Barcan formula has generated some controversy because—in terms of
possible world semantics—it implies that all objects which exist in any possible world (accessible to the actual world) exist in the actual world, i.e. that domains cannot grow when one moves to accessible worlds. This thesis is sometimes known as
actualism—i.e. that there are no
merely possible individuals. There is some debate as to the informal interpretation of the Barcan formula and its converse. An informal argument against the plausibility of the Barcan formula would be the interpretation of the predicate
Fx as "
x is a machine that can tap all the energy locked in the waves of the Atlantic Ocean in a practical and efficient way". In its equivalent form above, the
antecedent \Diamond\exists xFx seems plausible since it is at least theoretically possible that such a machine could exist. However, it is not obvious that this implies that there is something that is possibly a machine which could tap the energy of the Atlantic. == Converse Barcan formula ==