In this paper, we study the \(\Box \exists \) -bundled fragment of first-order modal logic, in which quantifiers are only allowed to occur within “bundled operators” of the form \(\Box \exists x\) . We characterize the expressivity of the fragment via the notion of \(\Box \exists \) -bisimulation, and offer complete axiomatizations of the fragment over 15 classes of constant-domain augmented frames in the modal cube, ranging from K to S5. In the axiomatizations, when characterizing certain frame properties, axioms involving the \(\Box \exists \) -operator, which do not appear in propositional modal logic, are also used. Hence, we also show that these \(\Box \exists \) -axioms are necessary for the completeness of the axiomatizations in question. Finally, we show under what frame conditions can we partly or completely eliminate the part of the axiomatization which characterizes the constant-domain property.
