Аннотация:
Получен ответ на вопрос о том, разрешима ли элементарная теория порожденной константами 0 и 1 свободной алгебры, соответствующей известной полимодальной логике доказуемости $GLP$. Этот вопрос был сформулирован в 2006 году в обзорной статье Л. Д. Беклемишева и А. Виссера. Рассматриваемая алгебра играет важную роль в исследовании арифметических теорий с точки зрения их ординальных характеристик, поэтому изучение ее алгоритмических свойств представляет значительный интерес. Полученный результат говорит о том, что существует алгоритм для распознавания истинности любой заданной формулы языка первого порядка в алгебре с конечным числом модальностей. Для доказательства алгоритмической разрешимости логических теорий обычно применяется сведение исследуемой теории к одному из классов теорий, разрешимость которых уже известна. В данном случае вопрос об алгоритмической разрешимости не сводится очевидным образом ни к одному из известных классов теорий. Для доказательства развита оригинальная техника, опирающаяся на общее понятие “линейности” $GLP$-алгебр.
