#матлог #учёба #миникурсы

На следующей неделе Степан Львович Кузнецов и Станислав Олегович Сперанский (Математический институт им. В.А. Стеклова РАН) в рамках своего визита в Новосибирский государственный университет прочтут мини-курсы.

Лекции пройдут очно в НГУ, возможно также подключение через Zoom. Для получения ссылки зарегистрируйтесь на странице мини-курсов https://sites.google.com/view/mca-logic

Расписание лекций.
ВНИМАНИЕ! Время везде указано новосибирское, т.е. +4 часа от московского, GMT+7.

В рамках мини-курса С.Л. Кузнецова "Лямбда-исчисление" запланировано три лекции:
(1) 18 ноября (понедельник), 16:20-17:55, ауд. 4140 НГУ,
(2) 19 ноября (вторник), 18:10-19:45, ауд. 4268 НГУ,
(3) 20 ноября (среда), 16:20-17:55, ауд. 4267 НГУ.

В рамках мини-курса С.О. Сперанского "Подход Крипке к формальной теории истины" запланировано три лекции:
(1) 18 ноября (понедельник), 18:10-19:45, ауд. 4140 НГУ,
(2) 19 ноября (вторник), 16:20-17:55, ауд. 4268 НГУ,
(3) 20 ноября (среда), 18:10-19:45, ауд. 4267 НГУ.

---
Аннотация курса С.Л. Кузнецова "Лямбда-исчисление":

Лямбда-исчисление — это логическая система для формализации вычислений посредством операций применения функций и функциональной абстракции. Лямбда-исчисление является основой семейства современных языков программирования, называемых функциональными языками. В рамках мини-курса будет дано введение в лямбда-исчисление, в двух его видах — бестиповом и типизованном. На первой лекции будет рассказано о лямбда-исчислении без типов (в котором любое лямбда-выражение может быть применено, как функция к любому другому), о его основных свойствах и о представлении в нём произвольных вычислимых функций. На второй лекции будут рассмотрены несколько вариантов типизованного лямбда-исчисления (здесь применение ограничено дисциплиной типов), описаны их вычислительные возможности и установлена связь между типизованным лямбда-термами и конструктивными доказательствами (соответствие Карри-Говарда). На третьей лекции будет рассказано о семантике лямбда-исчисления: теоретико-множественных моделях в типизованном случае и моделях Ершова-Скотта в бестиповом.

---
Аннотация курса С.О. Сперанского "Подход Крипке к формальной теории истины":

Пусть L — первопорядковый язык арифметики Пеано, а L' — какое-нибудь его расширение. Из леммы о диагонализации легко следует теорема Тарского о неопределимости истины: если L'-структура M обогащает стандартную модель арифметики, то множество всех (гёделевых номеров) L'-предложений, истинных в M, не определимо в самой M. Стало быть, если L' получается из L добавлением особого одноместного предикатного символа T, и мы хотим интерпретировать T как истинностный предикат для всего L', то T должен принимать как минимум три значения: «истинно», «ложно» и «неопределено», где последнее, в частности, соответствует парадоксу лжеца и ему подобным утверждениям.

Наиболее известный трёхзначный подход к формальной теории истины был предложен Солом Крипке. Здесь роль допустимых (трёхзначных) интерпретаций истинностного предиката T играют наименьшие неподвижные точки специальных монотонных операторов. Основой этих операторов являются различные схемы означиваний, которые соответствуют тем или иным трёхзначным логикам, таким как, например, сильная или слабая логика Клини. Получающиеся в результате наименьшие неподвижные точки могут быть представлены как пределы трансфинитных последовательностей аппроксимирующих интерпретаций.

Цель данного мини-курса — познакомить слушателей с теорией истины по Крипке и её вычислительными аспектами.

🔗 МЦА


➰ ВК