На главную страницу НМУ
Михаил Александрович Раскин
Верное и доказанное
ВИДЕО
Курс планируется посвятить основным понятиям математической логики, рассматриваемой как
способ описать способы рассуждения в математике.
Я собираюсь обратить внимание слушателей не только на то, что является правильным
доказательством (это можно осознать и на примерах, таким примером является любой другой
курс НМУ), но и на то, что может оказаться неправильным, каким способом определить эту
неправильность и каких доказательств быть не может.
Кроме того, будут показано также и примеры того, что можно было бы строить математику на
другом понятии доказательства и тоже получить область изучения быть может, иногда менее
интересную и применимую, но это уже внешние понятия.
Предварительных знаний не требуется, но я надеюсь иногда ссылаться на примеры из алгебры
и математического анализа, которые проходятся на первом курсе.
Я планирую, что в качестве основного учебника, по которому будут излагаться
доказательства теорем, будет использоваться учебник Верещагина и Шеня.
Экзамен
[Экзаменационное задание 1 .pdf|Экзаменационное задание 2 .pdf]
Лекции (Lecture notes. pdf)
[Лекция 2 .pdf|Лекция 3 .pdf|Лекция 4 .pdf|Лекция 5 .pdf|Лекция 6 .pdf]
[Лекция 7 .pdf|Лекция 8 .pdf|Лекция 9 .pdf|Лекция 10 .pdf|Лекция 11 .pdf]
[Лекция 12 .pdf|Лекция 13 .pdf]
Листки (Exercise sheets. pdf)
[Листок 1 .pdf]
План программы курса
- Введение.
Математика как изучение полностью формальных фактов.
Способы установления формального факта. Понятие доказательства. Варианты требований к
доказательству.
Логика как наука о формальных доказательствах формальных фактов.
- Стандартные системы записи и доказательства формальных фактов.
Силлогизмы. Исчисление высказываний.
Исчисление предикатов первого порядка.
Модальные логики.
Исчисления Ламбека.
Стандартные выводы.
Генценовские исчисления.
Исчисление резолюций.
- Примеры нестандартных подходов.
Паранепротиворечивые логики.
Ультрафинитизм.
- Базовые факты про стандартные системы.
Модели. Корректность исчислений высказываний и предикатов (1-го порядка).
Полнота исчисления высказываний и исчисления предикатов.
Устранение сечений.
- Стандартные аксиоматические системы.
PA (Арифметика Пано).
ZFC (Теория множеств Цермело-Френкеля).
Алгебраические структуры.
- Ограничения доказуемого.
Понятие независимости утверждения от аксиом. Примеры в простых аксиоматиках.
Континуум-гипотеза.
Вычислимость и доказуемость.
Неподвижная точка и вычислительные модели в широком смысле слова.
Проблема остановки. Существование программы, про которую ничего нельзя доказать.
Теорема Гёделя о неполноте. Расширения с помощью утверждения из теоремы Гёделя.
Нестандартные модели арифметики и теории множеств.
- Новая правда. Доказательства, которые не может прочитать человек.
Проблемы, которые могут быть с необозримым доказательством, и от которых мы обоснованно
отмахиваемся, если доказательство читаем.
Виды проблем с надёжностью компьютерного доказательства.
Что же доказано в теореме о четырёх красках.
Существующие технические средства.
Литература:
-
учебник Шеня и Верещагина: Н./~ZК./~ZВерещагин,
А./~ZШень. Лекции по математической логике и теории алгоритмов.
- конспект Пентуса: М.
Р. Пентус. Спецкурс "Исчисление Ламбека"
- статья Ламбека: J
oachim Lambek. The mathematics of sentence structure
- Конспект Верещагина по методу вынуждения в теории множеств: Н.К. Верещагин. Метод
вынуждения (конспект лекций)
- учебник Шеня и Верещагина по теории множеств: Н.К.Верещагин,
А.Шень. Начала теории множеств.
- Статья про теорему 4 красок: Georges Gonthier. Formal Proof
The Four-Color Theorem