Программа учебного курса
Логические исчисления
Специальная программа в рамках стандарта магистерской программы ___ «___» по направлению подготовки магистров ___ «___»
Организационно-методический раздел.1.1. Цели и задачи курса
Цели курса
- знакомство с важнейшими видами неклассических логик
- изучение различных видов семантики для неклассических логик: оценочная семантика, семантика Крипке, алгебраическая семантика
- изучение методов доказательства полноты и разрешимости неклассических логик
- знакомство с важнейшими конструктивными свойствами логик: дизъюнктивным свойством, свойством конструктивного отрицания, свойством финитной аппроксимируемости, интерполяционным свойством
- знакомство с новыми видами логических исчислений: табличные исчисления, естественный вывод, дескриптивные логики, пропозициональная динамическая логика, линейная логика
Задачи курса
- Познакомить студентов с аппаратом логических исчислений, как с одним из инструментов для формализации информации
- создать базис для дальнейшего самостоятельного изучения и исследования компьютерных языков, основанных на логических исчислениях
- научить студентов применять самостоятельно основные методы доказательства полноты и разрешимости логик, а также методы сравнения выразительности логик
1.2. Требования к уровню усвоения содержания курса
По окончании изучения данной учебной дисциплины студент должен
Иметь представление
- о причинах введения в рассмотрение различных видов неклассических логик
- об областях применения неклассических логик и примерах их использования в информатике
- об основных видах семантики неклассических логик
- об алгебраических методах исследования неклассических логик
Знать
- Аксиоматику и семантическую характеризацию различных конструктивных, модальных и релевантных логик
- основные методы доказательства теорем полноты
- методы доказательства разрешимости неклассических логик
Уметь
- строить выводы в различных дедуктивных системах
- доказывать теоремы полноты для различных видов логик и различных типов семантик
- обнаруживать и обосновывать сходства и различия выразительности логик
1.3. Формы контроля
Итоговый контроль. Для контроля усвоения дисциплины учебным планом предусмотрен экзамен, включающий в себя теоретические вопросы.
Текущий контроль. Не предусмотрен.
2. Содержание дисциплины.
2.1. Новизна и актуальность курса.
Курс включает в себя знакомство с важнейшими типами неклассических логик и логических семантик с учетом современного состояния исследований в области неклассических логик. Неклассические логики находят многочисленные применения в методах верификации программ и протоколов, в инженерии знаний и лингвистике, что обуславливает актуальность данного курса для студентов, планирующих работать в области теоретической и прикладной информатики.
2.2. Тематический план курса (распределение часов).
Наименование разделов и тем | К о л и ч е с т в о ч а с о в | ||||
Лекции | Семинары | Лаборатор-ные работы | Самостоятельная работа | Всего часов | |
Раздел 1 Обзор курса и элементы традиционной логики | 4 | 2 | 6 | ||
Раздел 2. Первые примеры неклассических логик. Метод канонических моделей | 6 | 4 | 10 | ||
Раздел 3. Конструктивные логики. Семантика Крипке. | 8 | 6 | 14 | ||
Раздел 4. Методы доказательства разрешимости. | 6 | 4 | 10 | ||
Раздел 5. Нормальные модальные логики | 8 | 6 | 14 | ||
Раздел 6. Многозначные логики | 4 | 2 | 6 | ||
Раздел 7. Алгебраическая семантика для позитивной, интуиционистской, минимальной логик и их расширений | 10 | 8 | 18 | ||
Раздел 8. Алгебраическая семантика для нормальных модальных логик | 4 | 2 | 6 | ||
Раздел 9. Типизированное λ-исчисление | 4 | 2 | 6 | ||
Раздел 10. Неклассические логики в современной информатике | 6 | 6 | 12 | ||
Итого по курсу: | 60 | 42 | 102 |
2.3. Содержание отдельных разделов и тем.
Раздел 1. Обзор курса и элементы традиционной логики (4 часа).
Обзор направлений современных исследований в области неклассических логик. Примеры практического применения логик. Описание тем курса и их сопоставление с предметом математической логики.
Краткий исторический экскурс в традиционную логику. Синтаксические категории языка: имена, предложения и функторы. Структура простого категорического предложения. Простые категорические силлогизмы: фигуры и модусы. Правила простого категорического силлогизма. Формализация силлогистики средствами современной логики.
Раздел 2. Первые примеры неклассических логик. Метод канонических моделей (6 часов).
Пропозициональный язык: термы, формулы, подстановки. Дедуктивные системы и отношения следования. Важнейшие свойства следования, задаваемые дедуктивной системой. Теории. Теорема дедукции в общем виде. Дедуктивная система классической логики. Доказательство теоремы полноты методом канонических моделей: лемма о расширении, свойства полных теорий, лемма о канонической модели. Позитивная классическая логика: понятие простой теории, оценочная семантика, теорема полноты. Логика CLuN: пример не истинностно-функциональной семантики, теорема полноты.
Логика как множество формул. Решетки логик. Понятия фрагмента и консервативного расширения логики. Дальнейшие примеры логик с оценочной семантикой: логика классической опровержимости, максимальная негативная логика. Понятия точного вложения и дефинициальной эквивалентности логик. Примеры задания одной логики в различных языках. Следствия из результатов сопоставления логик: сведение проблем разрешимости, сравнительная выразительность.
Раздел 3. Конструктивные логики. Семантика Крипке (8 часов).
Позитивная логика. Шкалы Крипке, выполнимость формул в шкалах. Леммы о монотонности и о порожденной подмодели. Полнота и сильная полнота логики относительно класса шкал. Полнота по Крипке. Каноническая модель для расширения позитивной логики. Теоремы о корректности и полноте для позитивной логики. Дизъюнктивное свойство позитивной логики: семантическое и синтаксическое доказательства.
Интуиционистская и минимальная логики: способы задания в различных языках; семантика Крипке, корректность и полнота, дизъюнктивное свойство. Примеры расширений интуиционистской и минимальной логик.
Исторический экскурс: интуиционизм и конструктивизм; формализация интуиционистской логики Колмогоровым и Гейтингом; задачная семантика Колмогорова и семантика реализуемости по Клини. Дизъюнктивное свойство и свойство конструктивного отрицания. Построение программ по доказательствам, концепция proofs as programs.
Логики Нельсона с сильным отрицанием N3 и N4. Семантика Крипке для N3 и N4. Монотонность верифициремости и фальсифицируемости. Лемма о порожденной подмодели. Теоремы о корректности и сильной полноте для логик N3 и N4. Дизъюнктивное свойство и свойство конструктивного отрицания для N3 и N4. Формы правила замены для логик Нельсона.
Раздел 4. Методы доказательства разрешимости (6 часов).
Метод фильтрации. Полнота позитивной, интуционистской и минимальной логик относительно классов конечных шкал. Финитная аппроксимируемость и разрешимость. Отсутствие свойства сильной полноты относительно классов конечных шкал.
Точное вложение логики N4 в позитивную логику и N3 в интуиционистскую логику. Разрешимость N3 и N4.
Табличные алгоритмы, доказательство полноты и корректности вывода относительно табличного алгоритма. Метод семантических таблиц. Табличные исчисления для классической и интуиционистской логики. Исчисление Дыкхова-Воробьева для интуиционистской логики.
Проблемы домино: общая, ограниченная и периодическая. Примеры сведения проблем домино к проблемам разрешимости логик. Доказательство нижней границы вычислительной сложности проблемы разрешимости на примере.
Раздел 5. Нормальные модальные логики (8 часов).
Семантика Крипке для модальных логик. Модальная степень формулы и лемма о порожденной подмодели. Минимальная нормальная модальная логика K. Решетка номальных расширений логики K. Каноническая модель для расширений логики K. Теоремы о корректности и полноте для K. Нормальные модальные логики T, D, K4, S4, S5: аксиоматика и семантическая характеризация. Алгебраические свойства бинарных отношений, выразимые и невыразимые в модальных логиках; сопоставление с логикой первого порядка.
Трансляция интуиционистской логики в S4.
Логика доказуемости. Аксиома Геделя-Леба. Теорема полноты. Отсутствие компактности семантики.
Методы доказательства разрешимости. Фильтрация для модальных логик. Табличные алгоритмы. Вычислительная сложность проблемы разрешимости в модальных логиках. Вложение модальных логик в логику первого порядка. Гардидный фрагмент.
Раздел 6. Многозначные логики (4 часа).
Логические матрицы и проблема независимости систем аксиом. Трехзначные логики Лукасевича, Клини, Геделя-Сметанича. Четырехзначная логика Белнапа и отношение первопорядкового следования FDE. Релевантность отношения следования. Система естественного вывода для FDE.
Понятие нормальной логической матрицы. Теорема о существовании характеристической нормальной матрицы.
Раздел 7. Алгебраическая семантика для позитивной, интуиционистской, минимальной логик и их расширений (10 часов)
Импликативные решетки: определение и основные свойства. Задание импликативных решеток тождествами. Конгруэнции и фильтры. Подпрямо неразложимые импликативные решетки. Дуальный изоморфизм решетки подмногообразий многообразия импликативных решеток и решетки расширений позитивной логики. Аксиоматики пересечения двух логик. Дистрибутивость решетки расширений позитивной логики.
Алгебры Гейтинга и j-алгебры. Топологические представления алгебр Гейтинга и модальных алгебр. Дуальный изоморфизм решетки подмногообразий многообразия алгебр Гейтинга (j-алгебр) и решетки расширений интуиционистской (минимальной) логики. Полное описание решетки расширений логики Даммета.
Формулы Янкова. Леммы Янкова и Вроньского. Сильно независимые последовательности формул. Лестница Ригера-Нишимуры. Континуальность решетки суперинтуционистских логик.
Раздел 8. Алгебраическая семантика нормальных модальных логик (4 часа).
Модальные алгебры. Конгруэнции и открытые фильтры. Подпрямо неразложимые алгебры. Топологическое представление модальных алгебр. Многообразия модальных алгебр и нормальные модальные логики.
Раздел 9. Типизированное λ-исчисление (4 часа)
λ-исчисление как универсальная модель вычислений; λ-куб; варианты применения.
Раздел 10. Неклассические логики в современной информатике (6 часов)
Синтаксис и семантика дескриптивной логики ALC, пропозициональной динамической логики, темпоральной логики и линейной логики. Сравнение с модальными логиками, изученными ранее в курсе. Табличные исчисления для данных логик и вычислительная сложность проблемы разрешимости.
2.4. Образцы вопросов для подготовки к экзамену.
Раздел 1.
1) Каковы основные периоды развития логики?
2) Напишите повествовательное предложение, состоящее не менее чем из шести слов, и определите синтаксические категории его составных частей.
3) Опишите основные логические связи между предложениями, входящими в логический квадрат?
4) Какова каноническая форма простого категорического силлогизма?
5) Опишите, чем определяются фигуры и модусы простого категорического силлогизма?
6) Перечислите важнейшие правила простого категорического силлогизма?
7) Как аксиоматизировать силлогистику, используя средства пропозициональной логики?
Раздел 2.
1) Что такое пропозициональный язык?
2) Дать определение дедуктивной системы и отношения следования, заданного дедуктивной системой?
3) Определите транзитивность, монотонность, компактность и подстановочность отношения следования. Для каких дедуктивных систем выполнены эти свойства?
4) Какие свойства дедуктивной системы позволяют доказать теорему дедукции?
5) Определите дедуктивную систему позитивной классической логики.
6) Дайте определение простой теории и докажите лемму о расширении для позитивной классической логики.
7) Какими свойствами обладают простые теории позитивной классической логики?
8) Докажите теорему полноты для позитивной классической логики.
9) Что такое истинностно-функциональная семантика? Приведите пример логики, семантика которой не является истинностно-функциональной.
10) Как определяются решеточные операции на классе расширений данной логики?
11) Что такое консервативное расширение?
12) Докажите, что классическая логика, логика классической опровержимости и максимальная негативная логика являются консервативными расширениями позитивной классической логики.
13) Определите понятия точного вложения одной логики в другую и дефинициальной эквивалентности двух логик.
14) Дайте определения логики классической опровержимости в двух различных языках и докажите, что получившиеся логики дефинициально эквивалентны.
Раздел 3.
1) Перечислите аксиомы позитивной логики.
2) Что такое шкала Крипке, модель над шкалой, как определяется выполнимость формул в мирах модели?
3) Докажите лемму о монотонности.
4) Что такое порожденная подмодель? Докажите лемму о порожденной подмодели.
5) Как определяются логика шкалы и логика класса шкал? Докажите, что это будут расширения позитивной логики.
6) Что такое полнота и сильная полнота логики относительно класса шкал? Какие логики полны по Крипке?
7) Как определяется каноническая модель расширения позитивной логики.
8) Докажите лемму о канонической модели для расширения позитивной логики.
9) Докажите теорему сильной полноты для позитивной логики.
10) Что такое дизъюнктивное свойство? Докажите, что позитивная логика обладает дизъюнктивным свойством.
11) Что такое слэш Клини? Приведите синтаксическое доказательство дизъюнктивного свойства позитивной логики.
12) Что такое интуиционистская логика?
13) Как определяется выполнимость формул интуиционистской логики на шкалах Крипке.
14) Докажите теорему о сильной полноте для интуиционистской логики.
15) Что такое j-шкала? Как определяется выполнимость формул на j-шкалах?
16) Окажите теорему о сильной полноте для минимальной логики.
17) Обладают ли интуиционистская и минимальная логики дизъюнктивным свойством.
18) Что такое свойство конструктивного отрицания? Обладает ли интуиционистская логика свойством сильного отрицания?
19) Определите логику Нельсона N4 и семантику Крипке для этой логики.
20) Будет ли отношение фальсифицируемости формул монотонным?
21) Что такое каноническая модель для расширения логики N4?
22) Докажите теорему сильной полноты для логики N4.
23) Что такое N3-модели? Их важнейшее свойство?
24) Докажите, что логика N3 сильно полна относительно класса N3-моделей.
25) Замкнута ли логика N4 относительно правила замены?
26) Какие слабые варианты правила замены верны для логик N3 и N4?
Раздел 4.
1) Как определяется фильтрация модели по множеству формул?
2) Каким условиям должно удовлетворять множество формул, по которому происходит фильтрация?
3) Докажите лемму о фильтрованной модели.
4) Докажите, что интуиционистская и позитивная логики полны относительно класса всех конечных шкал.
5) Докажите, что минимальная логика полна относительно класса всех j-шкал.
6) Докажите разрешимость позитивной, интуиционистской и минимальной логик.
7) Докажите, что позитивная и интуиционистская логики не сильно полны относительно класса всех конечных шкал.
8) Докажите, что минимальная логика не сильно полна относительно класса все конечных j-шкал.
9) Докажите, что логика N4 точно вкладывается в позитивную логику.
10) Докажите, что логика N3 точно вкладывается в интуиционистскую логику.
11) Докажите разрешимость логик N3 и N4.
12) Какова главная идея метода семантических таблиц?
13) Определите табличное исчисление для классической логики. Докажите его полноту
14) Определите табличное исчисление для интуиционистской логики и докажите его полноту.
15) Приведите пример бесконечной таблицы для интуиционистского табличного исчисления.
16) Определите исчисление Дыкхова-Воробьева для интуиционистской логики.
17) Оцените сложность таблицы для формулы длинны n.
18) Докажите полноту исчисления Дыкхова-Воробьева.
Раздел 5.
1) Определите семантику Крипке для модального языка. Как определяется выполнимость модальных формул.
2) Определите модальную степень формулы, сформулируйте и докажите лемму о порожденной подмодели.
3) Задайте исчисление для минимальной нормальной модальной логики K.
4) Как определяется каноническая модель для нормального расширения логики K.
5) Докажите, что логика K полна относительно класса всех шкал.
6) Определите нормальные модальные логики T, D, K4, S4, S5.
7) Какими классами шкал характеризуются логики T, D, K4? Докажите соответствующие теоремы полноты.
8) Какими классами шкал характеризуются логики S4, S5? Докажите соответствующие теоремы полноты.
9) Докажите, что интуиционистская логика точно вкладывается в логику S4.
10) Определите логику доказуемости.
11) Сформулируйте теорему о вложении логики доказуемости в арифметику Пеано.
12) Какой класс шкал задает логику доказуемости? Докажите соответствующую теорему полноты.
13) Докажите, что семантика логики доказуемости не удовлетворяет свойству компактности.
Раздел 6.
1) Что такое логическая матрица? Как по логической матрице задать множетсво тавтологий и отношение следования.
2) Приведите примеры использования логических матриц для доказательства независимости систем аксиом.
3) Определите трех-значную логику Лукасевича. Ее особенности?
4) Определите логики Клини и Геделя-Сметанича.
5) Какова мотивация для четырехзначной логики Белнапа?
6) Задайте отношение первопорядкового следования FDE по четырех-значной матрице Белнапа. В чем состоит свойство релевантности следования?
7) Задайте систему естественного вывода для FDE и докажите теорему полноты.
8) Докажите теорему о существовании нормальной характеристической матрицы.
Раздел 7.
1) Определите импликативные решетки. Докажите простейшие свойства операции относительного псевдодополнения.
2) Докажите, что импликативные решетки образуют многообразие.
3) Какими тождествами можно задать многообразие импликативных решеток?
4) Докажите эквивалентность понятий решеточного и импликативного фильтров на импликативных решетках.
5) Установите взаимно однозначное соответствие между фильтрами и конгруэнциями импликативной решетки.
6) Какие импликативные решетки подпрямо неразложимы.
7) Покажите, что решетка подмногообразий многообразия импликативных решеток дуально изоморфна решетке расширений позитивной логики.
8) Как по двум аксиоматизируемым расширениям позитивной логики построить аксиоматику их пересечения.
9) Докажите, что решетка расширений позитивной логики дистрибутивна.
10) Определите алгебры Гейтинга и j-алгебры. Докажите их простейшие свойства.
11) Докажите, что произвольная импликативная решетка вкладывается в решетку плотных открытых подмножеств компактного T0-пространства.
12) Докажите, что произвольная алгебра Гейтинга вкладывается в решетку открытых подмножеств компактного T0-пространства.
13) Докажите, что решетки подмногообразий многообразия алгебр Гейтинга ( j-алгебр) и решетки расширений интуиционистской (минимальной) логики дуально изоморфны.
14) Опишите решетку расширений логики Даммета.
15) Постройте формулу ЯНокова по заданной подпрямо неразложимой алгебре Гейтинга.
16) Докажите лемму Янкова.
17) Докажите лемму Вроньского.
18) Что такое сильно независимая последовательность логик? Как по сильно независимой последовательности логик построить континуальное семейство логик?
19) Опишите свободную 1-порожденную алгебру Гейтинга.
20) Докажите, что существует континуум суперинтуиционистских логик.
Раздел 8.
1) Определите модальные алгебры и докажите их простейшие свойства.
2) Что такое открытый фильтр? Установите взаимно однозначное соответствие между открытыми фильтрами и конгруэнциями модальной алгебры.
3) Опишите подпрямо неразложимые модальные алгебры.
4) Установите дуальный изоморфизм между многообразиями модальных алгебр и нормальными модальными логиками.
3. Список основной и дополнительной литературы
, Многозначные логики, Логика и компьютер, вып.4, М:Наука, 1997. , Релевантная логика, М: ИФ РАН, 2000. Символическая логика, Изд-во Санкт-Петербургского университета, Санкт-Петербург, 2005. Е. Расева, Р. Сикорский, Математика метаматематики, М. Наука, 1972. H. Rasiowa, An algebraic approach to non-classical logic, North-Holland, Amsterdam, 1974.