Наименьшие неподвижные точки в логике Гёделя–Леба

Показано, что существует формула, определяющая наименьшую неподвижную точку модальной пропозициональной позитивной схемы в любой иррефлексивной частично упорядоченной модели Крипке с обрывом возрастающих цепей. Отсюда следует теорема о наименьшей неподвижной точке для логики Гёделя–Леба.