С 11 января по 1 февраля 2023 г. в рамках семинара по социальной эпистемологии и искусственному интеллекту доктор физико-математических наук С.П. Одинцов (Институт математики им. С.Л. Соболева СО РАН) прочитает лекционный курс "Конструктивные семантики и IF-логика".
Лекции будут проходить по средам в 15.00 в конференц-зале. Первая лекция: 11 января.
Аннотация курса: Курс содержит краткий экскурс в историю конструктивных логик, включающий в себя объяснение задачной семантики Колмогорова и семантик реализуемости по Клини и по Нельсону. После этого мы рассмотрим теоретико-игровую семантику логики первого порядка (FOL), выясним, чем отличаются игры с полной информацией от игр с неполной информацией. Определим синтаксис IF-логики Хинтикки (Independence friendly logic, IF-FOL) и покажем как семантика IF-FOL получается из теоретико-игровой семантики FOL при помощи ограничения на полноту информации. Установим эквивалентность выразительных возможностей IF-FOL и экзистенциального фрагмента логики второго порядка и, как следствие, рефлексивность IF-FOL, т.е. возможность определить средствами IF-FOL истинность IF-FOL-формул. Далее, мы установим связь между реализациями по Нельсону и эффективными стратегиями в играх для FOL, установив тем самым, что реализуемость по Нельсону - это конструктивная версия теоретико-игровой семантики для FOL. Введем так называемую трамп-семантику для IF-FOL (семантика, задаваемая при помощи множеств означиваний, предложена Ходжесом). Определим трамп-реализуемость и покажем, что она является конструктивной версией теоретико-игровой семантики для IF-FOL. Наконец, установим результат о консервативности трамп-реализуемости над реализуемостью по Нельсону.