Modal group theory

I introduce modal group theory, where one investigates the class of all groups using embeddability as a modal operator. By employing HNN extensions, I demonstrate that the modal language of groups is more expressive than the first-order language of groups. Furthermore, I establish that the theory of true arithmetic, viewed as sets of Gödel numbers, is computably isomorphic to the modal theory of finitely presented groups. Finally, I resolve an open question posed by Sören Berger, Alexander Block, and Benedikt Löwe by proving that the propositional modal validities of groups constitute precisely the modal logic S4.2.