Спецкурс «Полнота исчисления Ламбека»

Объявление

Знаете ли вы, что языки можно перемножать и даже делить друг на друга, и такие действия над языками интересны языковедам? Свойства этих операций описываются системой правил, называемой исчислением Ламбека, и об этом по средам с 18:30 до 20:05 в ауд. 16-04 (кроме дней, по которым собирается большой семинар кафедры) к. ф.-м. н. С. Л. Кузнецов читает спецкурс (½ г.) «Полнота исчисления Ламбека», на котором рассказывается об исчислении Ламбека и излагается доказательство весьма естественной и при этом глубоко нетривиальной теоремы М. Р. Пентуса о полноте исчисления Ламбека относительно интерпретации на формальных языках, а также связанных с ней результатов.

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

Задачи

Краткое содержание прошедших лекций

20.02.2013

Формальные языки над алфавитом Σ. Операции над формальными языками: умножение, левое деление, правое деление.
Исчисление Ламбека в гильбертовской форме (L_H) [4] [1, § 2].
Интерпретация типов исчисления Ламбека формальными языками. Формулировка теоремы о полноте. [2, теорема 6.5] [1, теорема 5.11]

27.02.2013

Исчисление Ламбека в генценовской форме (L). [4] [1, § 3.1]
Формулировка теоремы об устранимости сечения. [4] [1, § 3.2]
Обратимость однопосылочных правил L. [1, лемма 3.26]
Эквивалентность исчислений L и L_H. [4] [1, теорема 3.29]
Свойство подформульности и элементарные фрагменты L. [1, § 4.3]
Теорема Бушковского об L-полноте исчисления L(\,/). [3, теорема 1] [1, теорема 5.8]

06.03.2013

Разрешимость задачи выводимости секвенций в исчислении Ламбека.
Непригодность конструкции из доказательства Бушковского для доказательства L-полноты исчисления L.
Квазимодели. Tp(m)-квазимодели.
Консервативное расширение квазимодели. Предел консервативной последовательности квазимоделей.
Понятие свидетеля того факта, что u ∉ w(A\B), в Tp(m)-квазимодели. Засвидетельствованные классы Tp(m)-квазимоделей.

13.03.2013

Подсказки к некоторым задачам.
Теорема о расширении Tp(m)-квазимодели до модели в засвидетельствованном классе.

20.03.2013

Неполнота исчисления Ламбека относительно класса L-моделей, в которых интерпретации всех переменных суть конечные языки (решение задачи № 7).
Исчисление Ламбека, допускающее пустые левые части секвенций (L*).
Мультипликативная циклическая линейная логика (MCLL). Интерпретация L* в MCLL.
Сети доказательства для MCLL.

27.03.2013

Доказательство критерия выводимости в MCLL в терминах сетей доказательства.
Вариант MCLL' мультипликативной циклической линейной логики, соответствующий исчислению L. Сети доказательства для MCLL'.

03.04.2013

Интерпретация типов исчисления Ламбека на конечных линейных порядках.
Tp(m)-R-квазимодели, их построение на основе сетей доказательства.

08.05.2013

Завершение доказательства теоремы о полноте.

Список литературы