# Doing reverse mathematics by regarding modal logic as weak first-order logic

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?

• In this translation, do you have a pair of modal operators $\square_x$ and $\lozenge_x$ for each variable $x$? Oct 13, 2022 at 14:16
• Alex, thanks for pointing out my naivety. Oct 13, 2022 at 14:22
• It was just a clarifying question - I didn't mean to suggest your question is naive! I think it's interesting. Oct 13, 2022 at 14:27
• I take no offence, Alex. I am grateful for your asking a question that helps to clarify my idea. Oct 13, 2022 at 15:59