Let me add another instance, this time involving both set theory and modal logic at the same time. This application involves modal logic fundamentally, but seems very little related to computer science, and rather seems much closer to philosophical issues concerning the nature of mathematical existence.
The idea is to consider a model of set theory in the context of all its forcing extensions, and their forcing extensions, and so on, as a kind of multiverse. This generic multiverse is very naturally viewed as a Kripke model, where each model of set theory accesses exactly its forcing extensions, and it turns out that although the fundamental concepts seem at first to be second order, they are actually first order expressible in set theory. Thus, one defines that $\varphi$ is possible, written $\diamond\varphi$, if $\varphi$ holds in some forcing extension, and necessary, written $\square\varphi$, if $\varphi$ holds in all forcing extensions. The general question was, What are the modal validities of this forcing interpretation of modal logic?
It is easy to see that all the S4 and even the S4.2 axioms of modal logic are provably legitimate under the forcing interpretation. But what exactly are the provable validities?
Theorem.(Hamkins & Loewe, TAMS, 260, 2008) If ZFC is consistent, then the ZFC-provably valid principles of forcing are exactly the modal assertions of S4.2.
The proof makes essential use of an increased understanding of a complete set of Kripke frames for S4.2, using bisumulation at its core, as well as some detailed forcing combinatorics. Benedikt and I proved via bisimulation that the class of finite pre-Boolean algebras is complete for S4.2. Apart from this, the key ideas were the concepts of buttons and switches in set theory. Namely, a statement $\varphi$ is a switch if you can force $\varphi$ or $\neg\varphi$ over any model of set theory, and a button if you can force $\varphi$ in such a way that it remains true in all further extensions. (Once you push a button, you cannot unpush it.) For example, the Continuum Hypothesis is a switch, and the assertion "$\aleph_1^L$ is countable" is a button. By considering larger independent families of buttons and switches, we were able to simulate any Kripke model on a finite pre-Boolean algebra frame within set theory via forcing extensions, and thereby deduce the theorem.
A related question was whether the set theoretic universe could ever be completed with respect to what is possibly necessary. The Maximality Principle is the scheme expressing that every possibly necessary statement is already true: $\diamond\square\varphi\implies\varphi$. Under MP, if one could force any statement $\varphi$ in such a way that $\varphi$ was true in all subsequent forcing extensions, then $\varphi$ should already be true. I proved (also observed independently by Vanaana and Stavi) that this is equiconsistent with ZFC.