Хорошо известно, что теорема о существовании модели для классической логики предикатов допускает естественную конструктивизацию: у любой разрешимой теории есть вычислимая модель. Настоящий мини-курс будет посвящён вопросам конструктивизации аналогичных теорем (в терминах моделей Крипке) для неклассических предикатных теорий. Сначала будет рассмотрено конструктивное построение модели Крипке в случае интуиционистской предикатной логики, где миры представляют собой перечислимые множества натуральных чисел, упорядоченные по теоретико-множественному включению. Поскольку соответствующее отношение достижимости, вообще говоря, не является разрешимым, в дальнейшем будет приведена более аккуратная конструкция, обеспечивающая разрешимость частичного порядка на мирах. Схожие идеи могут быть использованы для различных модальных предикатных логик, таких как $\mathsf{QK}$, $\mathsf{QS4}$ и $\mathsf{QS5}$. Материал мини-курса основан на серии статей Х. Исихары, А. Нероуда и Б. Хусаинова.

Лекторы
Баженов Николай Алексеевич, Институт математики им. С.Л. Соболева Сибирского отделения Российской академии наук
Калимуллин Искандер Шагитович, Казанский (Приволжский) федеральный университет