Full Idea
The Barcan Formula ∀x□Fx→□∀xFx is often regarded as a defect of Simple Quantified Modal Logic, though this most clearly seen in its equivalent form ◊∃xFx→∃x◊Fx.
Gist of Idea
The Barcan Formula ∀x□Fx→□∀xFx may be a defect in modal logic
Source
Theodore Sider (Logic for Philosophy [2010], 9.5.2)
Book Reference
Sider,Theodore: 'Logic for Philosophy' [OUP 2010], p.238
A Reaction
[See Idea 13719 for an explanation why it might be a defect] I translate the first one as 'if xs must be F, then they are always F', and the second one as 'for x to be possibly F, there must exist an x which is possibly F'. Modality needs existence.
Related Idea
Idea 13719 Barcan Formula problem: there might have been a ghost, despite nothing existing which could be a ghost [Sider]