Barcan Marcus Disimplicated: ∀x □Fx ⊃ □∀xFx

Speranza

Consider the Barcan formula:


∀x□Fx ⊃ □∀xFx

In the construction of any system -- call it the Barcan Marcus system -- we have

"+, *"

and

"-, *"

i.e. introduction and elimination rules for each operator. "Rule" is too strong a word for Geary, so perhaps "guidelines" may do.
In the case of the Barcan formula, formulated by Palma above, the same applies.
I was suggesting that
the introduction and elimination 'rules' (alla Gentzen) for this or that operator (Barcan Marcus's field: quantified modalities) may bring in unwanted implicatures, and that most metaphysical (or ontological, better?) puzzles that some logicians (alla Quine) have identified may get a proper implicature-based explanation. Or not.