Беклемишев Поступило 22.09.2016 г. Рассматривается естественное обобщение свойства редукции для полимодальных алгебр доказуемости на произвольные GLP-алгебры. <...> В частности, это свойство установлено для свободных GLP-алгебр и для некоторых топологических GLP-алгебр (GLP-пространств). <...> DOI: 10.7868/S0869565217040041 Понятие GLP-алгебры возникло при исследовании модальных логик, описывающих поведение схем рефлексии и родственного им понятия омега-непротиворечивости в формальной арифметике (см. <...> ). С точки зрения модальной логики GLP-алгебры представляют собой модели полимодальной логики доказуемости , введенной Г.К. Джапаридзе [9]. <...> Центральными примерами -алгебр являются так называемые алгебры рефлексии (названные в [2, 3] градуированными алгебрами доказуемости) для формальных арифметических теорий . <...> GLP GLP T Формулой -рефлексии для перечислимой арифметической теории (содержащей элементарную арифметику RT Σ0 n n() T EA =∆ +0 exp ) называется I предложение , выражающее на языке формальной арифметики тот факт, что всякое доказуемое в арифметическое предложение кванT торной сложности истинно. <...> Каждая такая формула порождает корректным образом опредеΣ0 n ленную операцию 〈〉 → ϕ жения : RT +ϕ n() 〈〉ϕ+ϕ .nRn T :[ ] [ ( T ({ : + , 〈〉 <ω}) T nn )] Алгебра Линденбаума–Тарского, обогащенная всеми такими операциями, называется алгеброй рефлексии теории и обозначается = =. <...> }T Интересные применения этих алгебр связаны с изучением формальной арифметики Пеано и, в Математический институт им. <...> В.А. Стеклова Российской Академии наук, Москва E-mail: bekl@mi.ras.ru гебре Линденбаума–Тарского теории , сопоставляющую классу эквивалентности любого предложения класс эквивалентности предлоn TT +T :++ на булевой алT частности, с описанием следствий этой теории Π0 n кванторной сложности и ее доказуемо тотальных рекурсивных функций в терминах итерированных схем рефлексии. <...> Тождество (iii), называемое тождеством Лёба, формализует обобщение второй теоремы Гёделя о неполноте для теории . <...>