 Here the \(\mathtt{\Box}\) and \(\mathtt{\Diamond}\) are the box and diamond forms of the universal modality. The result of prefixing the ordinary propositional symbol \(\mathtt{p}\) by the \(\mathtt{Q}\) operator, converts \(\mathtt{p}\) to a nominal. To be more precise, taking the propositional quantifier \(\mathtt{\forall q}\) to range over all sets of worlds, \(\mathtt{Qp}\) says that \(\mathtt{p}\) denotes a singleton set, that is, \(\mathtt{p}\) is a standard nominal. But there is another approach to interpreting propositional quantifiers, called the general (or Henkin) approach, where propositional quantifiers range over a preselected set of subsets of worlds. Interpreted these two different ways, the \(\mathtt{Q}\) operator gives rise to two different ‘species’ of nominals, and it turns out that these two species behave differently with respect to the rule of universal instantiation. This is investigated in the paper Blackburn, Braüner, and Kofod (2020), which gives a tableau system for a hybrid logic with Henkin-style propositional quantifiers, containing both species of nominals. The paper moreover describes how this formally-defined ‘species division’ corresponds rather well with two intuitions about nominals that can be detected in Prior’s writings. 