Субструктурными логиками называются логические системы, в которых не принимаются все или некоторые из структурных правил: ослабления, перестановки, сокращения. Применения таких логических систем разнообразны. С их помощью моделируются рассуждения об ограниченных ресурсах: если формула $A$ задаёт некоторый ресурс, то она не эквивалентна «$A \textit{ и } A$», т. е. не выполнено правило сокращения.

Некоммутативные (без правила перестановки) субструктурные логики применяются для описания синтаксиса естественных языков, где играет роль порядок слов. Логики без правила ослабления (если $A$, то $B \to A$ для любого $B$) называются релевантными: в них моделируются рассуждения, где существенно должны использоваться все посылки. Таким образом, исключаются верные классически, но странные для естественного языка рассуждения вроде «Если завтра пойдёт дождь, то $2+2=4$». В рамках курса планируется дать общий обзор субструктурных логик и рассказать несколько наиболее ярких результатов об этих необычных логических системах.

Программа

1. Секвенциальные исчисления для субструктурных логик: мультипликативно-аддитивное исчисление Ламбека и его расширения. Алгебраическая семантика: решётки с делениями.
2. PSPACE-полнота задачи выводимости для мультипликативно-аддитивного исчисления Ламбека.
3. Интерполяционная лемма Роорды для исчисления Ламбека. Теорема Пентуса о грамматиках Ламбека и контекстно-свободных грамматиках. Контрпример к теореме Пентуса для коммутативного случая.
4. Теорема Андреки — Микулаша о полноте исчисления Ламбека относительно моделей на алгебрах бинарных отношений.
5. Дистрибутивное мультипликативно-аддитивное исчисление Ламбека (по Козаку), его алгоритмическая разрешимость и свойство конечных моделей.
6. Линейная логика Жирара. Консервативность классической линейной логики над интуиционистской (при отсутствии константы «ноль»).
7. Алгоритмическая неразрешимость линейной логики и её некоммутативного мультипликативно-экспоненциального варианта.
8. Релевантные логические системы, результаты Уркхарта об их алгоритмической неразрешимости.
9. Неассоциативное исчисление Ламбека, тернарная семантика, полиномиальный алгоритм разрешения задачи выводимости.
10. Исчисление Ламбека с итерацией Клини («логика действий») и его инфинитарный вариант. Результаты об алгоритмической неразрешимости.

Задачи по курсу

Программа

Лекторы
Кузнецов Степан Львович
Пшеницын Тихон Григорьевич

Финансовая поддержка
Курс проводится при финансовой поддержке Минобрнауки России (грант на создание и развитие МЦМУ МИАН, соглашение № 075-15-2022-265).

Организации
Математический институт им. В.А. Стеклова Российской академии наук, г. Москва
Математический центр мирового уровня «Математический институт им. В.А. Стеклова Российской академии наук» (МЦМУ МИАН)