Модальные предикатные логики дедекиндовых порядков

Известно, что модальные и суперинтуиционистские логики, определяемые классами нестрогих линейных порядков (как шкал Крипке), устроены относительно просто: они финитно аппроксимируемы, конечно аксиоматизируемы и даже coNP-полны. Если же мы будем рассматривать предикатные логики таких классов шкал, то даже вопрос описания — аксиоматического или алгоритмического — некоторых конкретных логик (например, определяемых всего одной «простой» шкалой Крипке) нередко оказывается весьма нетривиальным. Задача, лежащая в основе исследования, о результатах которого предполагается рассказать, состоит в том, чтобы найти конечную аксиоматику модальной предикатной логики, определяемой действительной прямой (как шкалой Крипке) при условии постоянства предметных областей миров (действительных чисел), или же доказать, что такая её аксиоматизация невозможна.
В процессе решения этой задачи удалось установить следующее: любая модальная предикатная логика, лежащая между логикой всех дедекиндовых порядков (как шкал Крипке) с условием постоянства предметных областей миров и логикой натурального ряда с постоянной счётной предметной областью, является Пи-1-1-трудной, причём даже в языке с двумя предметными переменными, одной унарной предикатной буквой и одной пропозициональной буквой. Отсюда, в частности, следует и решение задачи о конечной аксиоматизируемости логики действительной прямой с постоянными областями: эта логика не является не только конечно аксиоматизируемой, но и рекурсивно аксиоматизируемой. В докладе предполагается дать обзор известных результатов, а также объяснить идею доказательства Пи-1-1-трудности логик описанного класса (будет использована Сигма-1-1-полная проблема укладки домино). Также предполагается обсудить близкие задачи, в т.ч. такие, решение которых докладчику неизвестны.
Все необходимые определения будут даны в докладе.