16-17 октября. "Семантические аспекты интуиционистской логики" (Д. Рогозин)

[Alexander V. Smal]

Добрый вечер!

На ближайших выходных 16-17 октября Даниил Рогозин (ИППИ РАН,
Serokell) прочитает курс "Семантические аспекты интуиционистской
логики". Начало в субботу 16 октября в 12:00.
https://compsciclub.ru/courses/intuitionisticsemantics/2021-autumn/

Впервые мы попробуем провести курс в "гибридном" формате:
- Лекции будут транслироваться в zoom (ссылка будет опубликована в
новостях курса, её получат те, кто запишется на курс на сайте).
- Будет возможность очного участия с соблюдением противокодных мер. В
связи с этим количество очных участников ограничено. Если вы хотите
поучаствовать очно, то запишитесь, пожалуйста, в эту форму:
https://forms.gle/eza9P1DTwYdvV12w9

Аннотация

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

После чего принципы интуиционистких рассуждений были формализованы
Арендом Гейтингом, что положило начало одной из первых неклассических
логик, интуиционистской логики. В дальнейшем интуиционисткая логика
получила развитие в теории доказательств. Более того, интуиционисткая
логика оказалась довольно тесно связанной c типизированным
лямбда-исчислением. Таким образом, конструктивные логики также
повлияли на теорию языков программирования и системы проверки
доказательств.

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

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

Саша

--
Alexander V. Smal
St. Petersburg Department of Steklov Mathematical Institute
27 Fontanka, St. Petersburg, 191023, Russia