Интуиционизм возник в начале XX века как направление в основаниях математики, и основателем этого направления является Л. Э. Я. Брауэр. Когда в канторовской теории множеств были Расселом обнаружены парадоксы, возник кризис оснований математики, который математики и логики пытались решить в рамках программы Гильберта, которая предполагала доказательство непротиворечивости математики финитными методами, что являлось в те дни центральной проблемой в математической логике. Брауэр, предлагая альтернативный путь, полагал, что мы не можем рассуждать о конечных и бесконечных объектах одним и тем же образом. Более того, интуиционизм Брауэра отклонял абстракцию актуальной бесконечности и теоремы чистого существования, а основным критерием истинности математического знания Брауэр называл интуицию. Отсюда и название “интуиционизм”. После чего принципы интуиционистких рассуждений были формализованы Арендом Гейтингом, что положило начало один из первых неклассических логик, интуиционистской логики.

В дальнейшем интуиционисткая логика получила развитие в теории доказательств. Более того, интуиционисткая логика оказалась довольно тесно связанной c типизированным лямбда-исчислением, и, таким образом, конструктивные логики стали тесно связанными с теорией языков программирования и системами проверки доказательств.

В этом курсе мы базово изучим семантические аспекты интуиционистской логики. Мы изучим семантику Крипке, которая позволяет нам рассматривать интуиционистские логики как логики частичных порядков. Помимо самого исчисления Гейтинга мы в общих чертах рассмотрим расширения интуиционисткой логики, которые называются суперинтуиционисткими.

Логические исчисления также связаны с алгебраическими структурами. Например, классическая логика является логикой булевых алгебр. Интуиционистские логики можно аналогичным образом изучать методами универсальной алгебры. Мы изучим топологическую двойственность для алгебр Гейтинга и покажем, что любое непротиворечивое расширение интуиционистской логики является полным относительно усиленных шкал Крипке, которые называются обобщенными дескриптивными шкалами (general descriptive frames).