Алгоритмическая сложность неклассических логик унарного предиката

Планируется обсудить алгоритмическую сложность неклассических предикатных логик при ограничениях на средства языка. В 1962г. С.Крипке предложил простой способ, позволяющий моделировать в модальном языке бинарную предикатную букву с помощью двух унарных. Будет показано, как можно моделировать бинарную букву с помощью одной унарной в модальном языке и с помощью двух унарных в интуиционистском языке. Это сразу даёт неразрешимость многих логик в языке с одной-двумя унарными буквами и тремя переменными, поскольку классическая логика бинарного предиката неразрешима при трёх переменных в языке. Кроме того, будет показано, как можно промоделировать все унарные буквы с помощью одной унарной (как в модальном, так и в интуиционистском языке). С учётом известных результатов о неразрешимости многих неклассических логик в языке с двумя переменными (Д.Габбай, В.Шехтман (1993), Р.Кончаков, А.Куруш, М.Захарьящев (2005)), это даёт возможность доказать неразрешимость многих модальных и суперинтуиционистских предикатных логик в языке с одной унарной предикатной буквой и двумя переменными. Предлагаемое моделирование позволяет получить неперечислимость и даже неарифметичность соответствующих фрагментов некоторых логик, определяемых семантически. Мы подробно разберём доказательство неперечислимости модальных предикатных логик естественных классов конечных (по числу миров) шкал Крипке и доказательство неперечислимости позитивного фрагмента интуиционистской предикатной логики конечных шкал Крипке, когда языки этих логик содержат одну унарную предикатную букву и три предметные переменные.