 Quine’s main arrows were pointed towards modal predicate logics, especially the construction of sentences that contain modal operators under the scope of quantifiers (“quantifying in”). In predicate provability logic, however, where quantifiers range over natural numbers, both de dicto and de re modalities have straightforward interpretations, contrary to the case of other modal logics (see the note on the  de dicto / de re distinction).  For example, formulas like