Consider a unary operation f on the set of sentences of a model-theoretic language L, and a set T of sentences of L. Properties of f in T can be studied using propositional modal language: variables are evaluated as sentences of L, and f interprets the modal operator. The modal theory of f in T is defined as the set of those modal formulas which are in T under every valuation.

An example of this approach is Solovay's theorem providing a complete modal axiomatization of formal provability in Peano arithmetic. Another example is the theorem of Hamkins and Loewe axiomatizing the modal logic of forcing, where the modal operator expresses satisfiability in forcing extensions. Both these logics have good semantic and algorithmic properties: in particular, they have the finite model property, are finitely axiomatizable, and hence decidable.

This raises the question of modal theories of other model-theoretic relations R (e.g., the submodel relation or the homomorphic image relation). These theories can be defined in the case when satisfiability in R-images is expressible in L. In this talk we will discuss general properties of such modal systems, and then provide a complete axiomatization for the case of the submodel relation. This talk is based on a joint work with D.I. Saveliev.