Неподвижные точки формул с двойными модальностями

В статье изучается определимость неподвижных точек в модальных логиках. Доказана следующая теорема: наименьшая неподвижная точка оператора $F_\varphi$ в конечной транзитивной модели определяется некоторой итерацией позитивной формулы $\varphi(p,x_1,\ldots,x_n)$ с двойными модальностями.