Мы обсудим «модальную логику Гёделя–Лёба», которая получается из K посредством добавления «формулы Лёба» и традиционно обозначается через GL. В частности, речь пойдёт о связи GL cо знаменитыми теоремами Гёделя о неполноте и теоремой Лёба. Далее, мы покажем, что формуле Лёба соответствует класс всех нётеровых строгих порядков, который не аксиоматизируем в логике первого порядка. Кроме того, будет доказано, что не существует класса шкал, относительно которого GL сильно полна.