Reverse mathematics seeks to find subsystems of second-order logic that are equivalent to certain mathematics theorems, say over $\mathsf{RCA}_0$.
Modal logic can be regarded as a weak version of first-order logic -- with the modal necessity operator $\square$ as replacing the universal quantifier $\forall$ in first-order logic, and the possibility operator $\diamond$ as replacing the existential quantifier $\exists$. (I learned this interpretation from van Benthem's book: Modal Logic for Open Minds, p.3.) Via this replacement, a mathematics theorem written in the language of first-order logic can be converted to a sentence in modal logic. We can then ask:
Is there an axiom system in modal logic, that when regarded as a subsystem of first-order logic, is equivalent to a given mathematics theorem, say over $\mathsf{K}$? (Here $\mathsf{K}$ is a weak system of modal logic, in analogy to $\mathsf{RCA_0}$ for reverse mathematics.) Has there been work to do reverse mathematics over modal logic, in this sense?
