*Congress of Logic, Methodology and Philosophy of Science, Helsinki*

It is well known that the most straightforward way of adding rules for the quantifiers to
any adequate sequent calculus for the modal logic **S5** allows for the derivation of the
Barcan formula—$\diamondsuit\exists x\varphi \to \exists x \diamondsuit\varphi$. This
result is philosophically undesirable as, contra the Barcan Formula, common-sense metaphysics would have it that things can possibly exist without actually existing. In this talk I give an
account of what is suspicious about such derivations by making use of a modal object
language with primitive scope indicators. Using this modal object language we see derivations of
the Barcan formula as requiring a certain kind of scope elision between “possibly, $a$ is $F$” (written in this
language as “$\diamondsuit\ a\ Fa$“) and “concerning $a$, possibly it is $F$” (written as “$a\
\diamondsuit Fa$“), where we are only able to infer “$\exists x \diamondsuit Fx$” from the second
of these
formulas.