Конструктивные модели для неклассических предикатных логик. Лекция 1

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