Об интерпретации нормальных модальных логик и аддитивных формулах в S4, S5, Grz, K и GL

Пусть $L$ — модальная логика, $A(p)$ — формула с единственной переменной $p$. Рассмотрим перевод формул $f_A$, коммутирующий с булевыми связками и отображающий формулу вида $\Diamond B$ в $A(f_A(B))$. Обозначим через $L_A$ множество формул, перевод которых выводим в $L$. Несложно проверить, что $L_A$ является логикой (вообще говоря, не нормальной). Будем говорить, что формула $A$ задаёт интерпретацию $L_A$ в $L$.
Несложно заметить, что логика $L_A$ нормальна тогда и только тогда, когда
$$L \vdash A(p \lor q) \leftrightarrow A(p) \lor A(q) \text{ и } L \vdash A(\bot)\leftrightarrow \bot.$$
Такие формулы $A$ назовём аддитивными. Оказывается, что неэквивалентных аддитивных формул немного. В S5 их всего три, в S4 и Grz — пять. В K и GL аддитивных формул бесконечно много, но все они устроены относительно просто.
Мы обсудим основные методы, которыми были получены перечисленные результаты и возможные их обобщения.