# What is the Barcan Formula?

can someone please help explain this Barcan formula to me? (In English translation and maybe with an example?)

(◊ ∃x Fx) ↔ (∃x ◊ Fx)

And if there is only one possible state of the world, would it hold true??

Would love some clarification on this. Thanks!

• Do you mean to use a double arrow? (see en.wikipedia.org/wiki/Barcan_formula ) – virmaior Jun 12 '19 at 4:52
• @virmaior Yes, I do mean to use a double arrow. Why, does that change the meaning? I've seen what wikipedia has to say on it but I'm still confused as to what it means – user39914 Jun 12 '19 at 4:55
• Where are you getting the version with a double arrow? This isn't my area of expertise in philosophy, but the double arrow would have a significantly different meaning than a single direction arrow. – virmaior Jun 12 '19 at 5:10
• If there is only one possible world then all modal operators can be dropped without changing the meaning (possible=necessary=actual). With ◊ dropped this formula is a trivial tautology, hence it holds. – Conifold Jun 12 '19 at 17:48

(◊ ∃x Fx) ↔ (∃x ◊ Fx) can be seen as a conjunction of

(◊ ∃x Fx) → (∃x ◊ Fx) (the Barcan formula in the narrower sense)

and

(∃x ◊ Fx) → (◊ ∃x Fx) (the converse Barcan formula).

The forward direction, (◊ ∃x Fx) → (∃x ◊ Fx), says that no new objects come into existence when going from one possible world to another: If there is an accessible world where there exists an x s.t. Fx, then this x already exists in the current world (and Fx is possible at our world since we know it is true in the other world), so the object x that exists in that other world is not new. This property is called anti-monotonicity.

The converse direction, (∃x ◊ Fx) → (◊ ∃x Fx), says that no object ceases to exist when going from one possible world to another: If an x exists in the current world (and there is some accessible world where F is true of x), then there is an accessible world such that x exists in this world (and F is true of x in that world). This property is called monotonicity.

Together, (◊ ∃x Fx) ↔ (∃x ◊ Fx) expresses that the same set of objects exist in all possible worlds. It is hence an axiomatization of models with a constant domain, i.e. models where each world has the same set of individuals, whereas the combined Barcan formula is not valid in models with variying domains, where each world comes with a possibly different domain of objects.
If the model contains only one possible world, then the Barcan formula is trivially valid, since then we're talking about only one domain of objects anyway.