Fixed Points of Formulas with Double Modalities

In the paper definability of fixed points in modal logics is studied. The following theorem is proved: the least fixed point of the operator $F_\varphi$ in finite transitive model is defined by some iteration of the positive formula $\varphi(p,x_1,\ldots,x_n)$ with double modalities.