Учебный план курса «Математическая логика I»

Цель

Все курсы математики требуют доказывать, и все курсы философии требуют рассуждать; однако ни один из них не делает своим предметом само рассуждение, и все считают само собой понятным, что значит, что заключение следует из посылок. Этот курс делает этот вопрос своей темой. Его цель состоит в том, чтобы построить для простейшего языка логики первую полную математическую теорию, предметом которой является рассуждение, со всеми четырьмя её частями на виду: язык, формулы которого распознаются и читаются однозначно; исчисление, порождающее выводы без обращения к значению знаков; значение, приписывающее каждой формуле её истинностное значение при каждой оценке её переменных; и доказательство того, что исчисление и значение совпадают.

Если это так, то курс есть не собрание правил обращения с символами, а теория с центральным результатом, теоремой о полноте, которую подготавливает всё предшествующее. Для множества формул $\Gamma$ и формулы $\varphi$ выводимость $\Gamma \vdash \varphi$ означает, что существует конечная последовательность формул, построенная по аксиомам и правилам и оканчивающаяся на $\varphi$; семантическое следование $\Gamma \models \varphi$ означает, что всякая оценка, делающая истинными формулы из $\Gamma$, делает истинной и $\varphi$. Оба отношения рождаются из противоположных идей, одно синтаксическое и экзистенциальное, другое семантическое и универсальное; тем не менее курс доказывает, что $\Gamma \vdash \varphi \Leftrightarrow \Gamma \models \varphi$. Отсюда следует, что на всякий вопрос о том, что следует из данных посылок, можно отвечать с той стороны, с которой это окажется легче: предъявляя вывод, просматривая таблицу или, как учит последний содержательный урок, опровергая методом резолюций.

Для кого курс и предварительные знания

Курс обращён к тем, кто начинает изучать математику, информатику или философию, и к тем, кто на любом этапе своего образования хочет точно знать, что такое доказательство и почему ему можно доверять: к студентам, которые приступают к университетской математике и спотыкаются о доказательства, к студентам-информатикам, которым нужна логика схем, программ и задач выполнимости, и к студентам-философам, которые хотят перейти от логики рассуждений к её теории.

Это курс уровня 1, без предварительных требований и самодостаточный. Он не предполагает, что студент изучал логику, знает теорию множеств или когда-либо доказывал теорему. То, что он использует из множеств (принадлежность, включение, объединение, множества формул), из функций (оценка есть функция из переменных в $\{0, 1\}$), из цепочек знаков и из индукции, он излагает там, где это нужно: множества и цепочки в уроке раздела 1 о языке, а индукцию в следующем уроке, прежде чем ею пользоваться. Он предполагает лишь две вещи: внимательное чтение, потому что в формальном языке добавленный или пропущенный знак меняет цепочку, и элементарную арифметику натуральных чисел, которые в этом курсе, как и на всём сайте, начинаются с $1$.

Куда ведёт курс

Из сказанного следует место курса на сайте. У него нет предварительных требований, и он входит в цели трёх учебных программ, «Математика», «Информатика» и «Философия», потому что во всех трёх рассуждение есть одновременно инструмент и предмет. У него три дополнительных курса, которые можно проходить раньше, параллельно или позже, в любом порядке. Курс «Логика Аристотеля» изучает логику терминов и силлогизм, правильность которого зависит от таких слов, как «все» и «некоторый», остающихся за пределами этого курса, и показывает, из какой традиции пришли к исчислению. Курс «Алгебра и геометрия I» возводит дедуктивное здание из аксиом Пеано и применяет на практике, к числам, аксиоматический метод и индукцию, которые этот курс изучает как предмет; его план рекомендует изучить этот курс раньше или параллельно. Наконец, курс «Программирование на C++ I» переносит в практику то, что здесь является теорией: решить, правильно ли построена цепочка, просмотреть таблицу истинности, вычислить нормальную форму или найти опровержение суть процедуры, которые можно записать в виде программ.

Однако курс оставляет открытым вопрос о выразительности: его язык не может сказать «все» или «некоторый», и формализация рассуждений на русском языке теряет, начиная с раздела 1, кванторы. Следовательно, его предусмотренное продолжение есть курс «Математическая логика II», посвящённый логике предикатов, который пройдёт тот же путь с кванторами и переменными, пробегающими объекты: он сохранит корректность, полноту и компактность, с методами, которые этот курс предвосхищает, но в нём следование перестанет быть разрешимым.

Общие учебные цели

Следующие цели описывают, что должен уметь тот, кто завершит курс. Каждая сформулирована как наблюдаемое действие, так что её можно проверить конкретным заданием; каждый содержательный урок, в свою очередь, называет свои собственные цели, которые служат одной или нескольким общим, а заключительный урок показывает, в каких разделах и уроках прорабатывается каждая. Семь целей пронумерованы, чтобы на них можно было ссылаться.

1. Цель 1. Отличать язык-объект от метаязыка и решать по правилам образования, является ли цепочка формулой.
2. Цель 2. Формализовать высказывания и рассуждения естественного языка, указывая, что формализация сохраняет и что теряет.
3. Цель 3. Строить выводы в системе курса (аксиомы Лукасевича, modus ponens и замена двойного отрицания), сочетая аксиомы, исходные правила и производные правила.
4. Цель 4. Доказывать метатеоремы индукцией по натуральным числам, по сложности формул и по длине выводов.
5. Цель 5. Решать вопросы общезначимости, выполнимости, семантического следования и семантической эквивалентности с помощью таблиц истинности и эквивалентностей.
6. Цель 6. Приводить формулы к нормальным формам и выражать с их помощью функции истинности и схемы.
7. Цель 7. Объяснять и применять корректность, полноту и компактность и устанавливать невыполнимость методом резолюций.

Цели 3 и 7 имеют каждая свой раздел, вывод и метатеорию; цели 5 и 6 делят между собой раздел семантики, первая его первую половину, вторая вторую. Цель 2 имеет собственный урок, урок о формализации, и затем упражняется всякий раз, когда задача ставится словами. Цели 1 и 4, напротив, сквозные: различие между тем, что говорится внутри языка, и тем, что говорится о нём, проходит через все четыре раздела, а индукция есть форма всех важных доказательств курса, от однозначности разбора формул до корректности системы и леммы Кальмара. Отсюда следует, что их достижение нельзя приписать одному уроку и что их стоит развивать на протяжении всего курса.

Система курса и её решения

Курс логики высказываний можно построить многими способами, и обычные учебники различаются языком, исходными связками и дедуктивной системой. Этот курс принимает три решения, которые стоит знать с самого начала, потому что они объясняют то, что на первый взгляд может показаться странным.

Язык кружков и дисков

Язык курса имеет алфавит всего из двух знаков, кружка $\sigO$ и диска $\sigI$. $n$-я переменная есть цепочка из $n$ кружков, за которыми следует диск, $v_{n} = \sigO^{n}\sigI$, так что $v_{1} = \sigO\sigI$ и $v_{2} = \sigO\sigO\sigI$; и есть единственное правило образования: если $\varphi$ и $\psi$ формулы, то формулой является и $\sigI\varphi\psi$, которая сокращается как $(\varphi \downarrow \psi)$ и читается «ни $\varphi$, ни $\psi$». Следовательно, совместное отрицание $\downarrow$ есть единственная исходная связка, а все остальные суть сокращения, определяемые один раз: $\neg\varphi$ есть $(\varphi \downarrow \varphi)$, дизъюнкция $(\varphi \vee \psi)$ есть $\neg(\varphi \downarrow \psi)$, и через них определяются конъюнкция, импликация, эквиваленция и строгая дизъюнкция. Любой другой способ их записи есть теорема, которая доказывается, а не определение.

У этого выбора есть цена, читаемость, которую курс платит в метаязыке: никто не пишет изо дня в день цепочки кружков и дисков, а пишет их сокращённые имена, которые в любой момент можно развернуть до обозначаемой ими цепочки. Однако эта цена окупается многократно. Двух знаков хватает на бесконечно много переменных, так что всякая формула есть конечная цепочка над алфавитом из двух элементов. Связка пишется перед своими аргументами, и поэтому скобки не нужны: однозначность разбора доказывается рассуждением о весе, которое приписывает $+1$ каждой переменной и $-1$ каждому диску-связке. А поскольку всякая составная формула есть совместное отрицание, каждое доказательство индукцией по сложности имеет единственный составной случай, что сокращает все доказательства следующих разделов. То, что одной связки хватает, чтобы выразить любую другую, не предполагается: раздел семантики это доказывает.

Второе исходное правило

Дедуктивная система исходит из системы Яна Лукасевича: три схемы аксиом, записанные через отрицание и импликацию, и modus ponens как единственное правило. Эти схемы были сформулированы для языков, исходными связками которых являются отрицание и импликация; в языке кружков и дисков формула вроде $(v_{1} \downarrow v_{2})$ не есть ни то, ни другое, и для аксиом она непрозрачна. Первый урок раздела о выводе доказывает с помощью разметки, которую имеют все аксиомы, которую сохраняет modus ponens и которой нет у этой формулы, что система Лукасевича не выводит $((v_{1} \downarrow v_{2}) \rightarrow \neg v_{1})$.

Если это так, то систему нужно пополнить, и естественным средством кажется доказать двойное отрицание, $\varphi \dashv\vdash \neg\neg\varphi$, которое второй урок выводит из трёх схем. Разметка показывает, что этого недостаточно: теоремы двойного отрицания её сохраняют, и всё же даже с ними нельзя заменить $v_{1}$ на $\neg\neg v_{1}$ внутри совместного отрицания. Поэтому, доказав двойное отрицание, второй урок добавляет второе исходное правило, замену двойного отрицания: из формулы $\chi$ выводится формула, получающаяся заменой в ней одного вхождения подформулы $\theta$ на $\neg\neg\theta$ или одного вхождения $\neg\neg\theta$ на $\theta$. Итак, система курса состоит из трёх схем Лукасевича, modus ponens и этого правила.

Другие системы для совместного отрицания достигают того же с помощью схем аксиом, сделанных специально для него. Курс предпочитает правило по двум причинам: оно ещё проще, чем modus ponens, потому что берёт одну строку и меняет одно вхождение, и в нём нет ничего искусственного, потому что оно выражает то, что уже говорит двойное отрицание, а именно что $\theta$ и $\neg\neg\theta$ взаимозаменяемы, распространённое на любое место формулы. Кроме того, оно корректно, потому что сохраняет истинностное значение каждой строки, и сохраняет теорему о дедукции, добавляя один случай в её доказательство. То, что с ним хватает средств, чтобы вывести всё, что должно выводиться, есть теорема о полноте последнего раздела.

Компактность раньше сильной полноты

Полнота допускает три степени: слабая говорит, что всякая тавтология есть теорема; полнота для конечных множеств говорит, что всякое следствие конечного множества посылок выводится из него; сильная говорит, что то же верно для любого множества, в том числе бесконечного. Метод курса, лемма Кальмара, работает с конечным числом переменных формулы и с конечными посылками, и поэтому достигает первых двух степеней, но не третьей. Чтобы дойти до неё, достаточно, чтобы при $\Gamma \models \varphi$ некоторая конечная часть $\Gamma_{0}$ множества $\Gamma$ уже удовлетворяла $\Gamma_{0} \models \varphi$; однако именно это и утверждает теорема компактности.

Многие учебники сначала доказывают сильную полноту другим методом и выводят из неё компактность. В этом же курсе сильная полнота есть то, что ищется, и получать из неё компактность было бы порочным кругом. Откуда порядок меняется на обратный: урок о компактности доказывает её внутри семантики, не упоминая никакого вывода, фиксируя одно за другим значения $v_{1}, v_{2}, \ldots$, и лишь затем, в три строки, получает сильную полноту, то есть $\Gamma \models \varphi \Rightarrow \Gamma \vdash \varphi$ для всякого множества $\Gamma$.

Содержание

Курс состоит из шести разделов: этого знакомства, четырёх содержательных разделов и завершения. Каждый содержательный раздел открывается вводным уроком, который представляет его уроки, его место в курсе, то, что он считает известным, и задачу, которую он решает, и который начинается с входной проверки; закрывается он уроком итогов, который восстанавливает дедуктивную цепочку раздела, связывает её с остальным курсом, повторяет в итоговой проверке навыки входной и предлагает шесть задач повышенной трудности, более трудных, чем задачи уроков.

Раздел 0. Знакомство с курсом

Он состоит из этого урока, который устанавливает цель, общие цели, решения, содержание, трудоёмкость и устройство курса.

Раздел 1. Язык

Его цель состоит в том, чтобы построить язык, который изучает курс, доказать, что каждая формула читается единственным образом, и связать его с рассуждениями на русском языке.

1. Язык: введение.
2. Что такое математическая логика: правильность в сравнении с истинностью, контрпример, парадоксы и различие между языком-объектом и метаязыком.
3. Язык логики высказываний: множества и цепочки, язык кружков и дисков, его правило образования и его сокращения.
4. Индукция по натуральным числам и по формулам: простая, сильная и структурная индукция, лемма о весе, однозначность разбора и определения по рекурсии.
5. Формализация естественного языка: словарь, перевод высказываний и рассуждений и то, что теряет материальная импликация.
6. Язык: итоги и задачи повышенной трудности.

Раздел 2. Вывод

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

1. Вывод: введение.
2. Формальные дедуктивные системы: система Лукасевича, вывод из посылок, теорема о дедукции и разметка, показывающая её предел.
3. Четыре приёма вывода: гипотетический силлогизм, перестановка посылок, двойное отрицание, контрапозиция и замена двойного отрицания.
4. Симметрии связок: основная лемма о совместном отрицании, замена эквивалентных, альтернативные формы связок и их пять симметрий.
5. Приёмы классической логики: правила каждой связки, закон исключённого третьего, разбор случаев и доведение до абсурда, с посылками.
6. Законы де Моргана и дистрибутивности: их доказательства в обе стороны и замена эквивалентных внутри других формул.
7. Вывод: итоги и задачи повышенной трудности.

Раздел 3. Семантика

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

1. Семантика: введение.
2. Семантика логики высказываний: оценки и их продолжение по рекурсии, лемма о совпадении, таблицы истинности, общезначимость и выполнимость.
3. Семантическое следование и эквивалентность: следование из множеств, семантическая теорема о дедукции, замена и равномерная подстановка.
4. Обобщённые законы де Моргана и дистрибутивности: конъюнкции и дизъюнкции $n$ членов и их законы, по индукции.
5. Функциональная полнота: у всякой функции истинности есть формула, одного совместного отрицания достаточно, и полные системы связок.
6. Нормальные формы: литералы, дизъюнкты, дизъюнктивная и конъюнктивная формы, их двойственность и их существование.
7. Алгоритм нормальных форм и его применения: корректный и завершающийся алгоритм, а также проектирование и упрощение схем из переключателей.
8. Семантика: итоги и задачи повышенной трудности.

Раздел 4. Метатеория

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

1. Метатеория: введение.
2. Корректность и полнота: корректность индукцией по строкам, непротиворечивость, лемма Кальмара, слабая полнота и полнота для конечных множеств.
3. Теорема компактности: её семантическое доказательство, её эквивалентные формы, вытекающая из неё сильная полнота и её комбинаторные применения.
4. Метод резолюций: клаузальная форма, правило резолюции, его корректность и полнота опровержения и его цена.
5. Метатеория: итоги и задачи повышенной трудности.

Раздел 5. Завершение курса

Он состоит из урока Итоговый обзор курса «Математическая логика I», который напоминает семь общих целей, показывает на рисунке, в каких разделах и уроках прорабатывается каждая, сводит по целям первую попытку итоговых проверок и указывает, куда продолжается обучение.

Трудоёмкость и кредиты

Трудоёмкость курса измеряется не часами лекций, которых в асинхронном курсе нет, а всей работой того, кто его изучает: чтением, прослеживанием доказательств и выводов, решением задач и повторением. Оценка следует одному и тому же методу во всех курсах сайта: она учитывает время чтения текста каждого урока из расчёта сто слов в минуту, считая каждую формулу одним словом, двадцать минут на решённую задачу, тридцать пять на предложенную задачу, сорок пять на задачу повышенной трудности и двенадцать на входную или итоговую проверку, и добавляет запас в одну десятую на повторение.

Результаты

Уроки курса содержат в совокупности $90$ решённых задач, $90$ предложенных задач и $24$ задачи повышенной трудности, а также восемь проверок разделов. Оценочная трудоёмкость по разделам, округлённая до часа, такова:

• Раздел 0, знакомство с курсом: меньше $1$ часа.
• Раздел 1, язык: $30$ часов.
• Раздел 2, вывод: $36$ часов.
• Раздел 3, семантика: $43$ часа.
• Раздел 4, метатеория: $25$ часов.
• Раздел 5, завершение курса: меньше $1$ часа.

Всего получается около $137$ часов работы. Эту цифру следует читать как то, чем она является: оценку для того, кто изучает все доказательства и решает все задачи, включая задачи повышенной трудности. Тот, кто уже изучал логику или ограничивается предложенными задачами, не берясь за задачи повышенной трудности, потратит заметно меньше; тому, кто никогда не доказывал теорем, может понадобиться больше, особенно в разделах вывода и семантики, которые к тому же самые объёмные.

Однако эта цифра номинальная: именно она определяет кредиты курса, и она предполагает чтение в постоянном темпе и три четверти часа на задачу повышенной трудности. Пока она не измерена на реальных студентах, её стоит сопровождать реалистичным диапазоном. Если бы чтение шло вдвое медленнее предполагаемого темпа, как бывает, когда каждый вывод переписывается на бумаге карандашом, а каждая цепочка кружков и дисков разбирается вручную, и каждая задача повышенной трудности требовала семидесяти пяти минут вместо сорока пяти, тот же метод дал бы около $174$ часов. Следовательно, ожидаемая трудоёмкость лежит между примерно $137$ и примерно $174$ часами. Верхняя граница есть осторожная оценка сверху, а не измерение; диапазон будет уточнён, когда станет известно время, которое тратят изучающие курс, а до тех пор кредиты рассчитываются по номинальной цифре.

Рекомендуемый темп

Чтобы назвать темпы, этот план использует тот же критерий, что и другие планы сайта: полная занятость соответствует учебному году в $60$ кредитов, около $1650$ часов, распределённых примерно на сорок недель, то есть около $40$ часов в неделю, а неполная занятость составляет половину, около $20$ часов в неделю. Отсюда следует рекомендуемый темп в один семестр из шестнадцати недель, с примерно $8$ или $9$ часами занятий в неделю, немногим больше пятой части полной занятости; с учётом реалистичного диапазона от $9$ до $11$ часов в неделю. Этот семестр можно разделить с курсом «Алгебра и геометрия I», доказательства которого лучше читаются, когда вывод уже знакомый предмет.

Интенсивный темп, около $20$ часов в неделю, то есть при неполной занятости, позволяет пройти курс за семь недель. Более свободный темп, около $4$ или $5$ часов в неделю, растягивает его на два семестра, которые делятся почти пополам: разделы 0–2, язык и вывод, занимают около $67$ часов, а разделы 3–5, семантика, метатеория и завершение, около $69$.

Эквивалент в переводимых кредитах

Системы переводимых кредитов измеряют курс всей работой, которой он требует от того, кто его проходит, а не часами аудиторных занятий, чтобы обучение, пройденное в одном учреждении, могло быть признано в другом. Европейская система перевода и накопления кредитов, принятая европейскими университетами вслед за Болонской декларацией, отводит $60$ кредитов на учебный год при полной занятости и устанавливает каждый кредит в пределах от $25$ до $30$ часов работы. Чилийская система переводимых кредитов, принятая чилийскими университетами по аналогичной схеме, также отводит $60$ кредитов на учебный год и устанавливает каждый кредит в пределах от $24$ до $31$ часа работы.

Однако если разделить $137$ оценочных часов на границы каждого интервала, курс соответствует примерно $5$ европейским кредитам (от 4,6 до 5,5) и от $4$ до $6$ чилийским переводимым кредитам (от 4,4 до 5,7). Если взять за ориентир среднее значение обоих интервалов, 27,5 часа на кредит, то в обеих системах получается одно и то же число, 4,98, которое округляется до 5. Для европейских кредитов число $C$ кредитов ограничено так:

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

Устройство курса

Форма обучения

Курс асинхронный, сетевой и проходится в собственном темпе: у него нет дат, занятий в прямом эфире и сроков, и каждый студент продвигается с той скоростью, какую позволяют его подготовка и его время. Он предлагается на четырнадцати языках сайта, с одной и той же логикой во всех: формулы, выводы и шаги доказательств одинаковы в каждой версии, и переводится только текст. Уроки указывают, какие другие уроки стоит изучить раньше, так что рекомендуемый порядок задан явно.

Устройство урока

Все содержательные уроки построены одинаково. Они начинаются с краткого содержания и списка собственных учебных целей, сформулированных как наблюдаемые действия. Далее следует теория, с определениями, точно сформулированными результатами и их доказательствами, и примеры. Доказательства подаются как проигрыватели шагов: каждый шаг записывает строку, подсвечивает то, что меняется, и, когда опирается на предыдущий результат, возвращается к нему. Выводы системы записываются с пронумерованными строками и обоснованием каждой строки справа (аксиома, посылка, modus ponens с используемыми строками или производное правило), и по мере продвижения подсвечиваются цитируемые строки. Завершают урок пять решённых задач с пошаговым решением и пять предложенных задач, каждая со свёрнутой подсказкой и затем окончательным ответом; предложенные задачи на доказательство добавляют, в свёрнутом виде после ответа, развёрнутое решение, которое стоит открывать только после того, как написано собственное.

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

Проверка

Курс не ставит оценок: его проверка формирующая и опирается на самопроверку. Предложенные задачи позволяют проверить достижение целей каждого урока, а задачи повышенной трудности достижение целей каждого раздела. К этому добавляются проверки разделов: входная, в начале введения, измеряет исходный уровень одиннадцатью–пятнадцатью вопросами, потому что к вопросам раздела добавляет несколько вопросов о том, что раздел считает известным; итоговая, в уроке итогов и перед задачами повышенной трудности, измеряет достигнутое двенадцатью вопросами и сравнивается с входной. Обе проверяются прямо в браузере, с объяснением к каждому ответу и ссылкой на урок, который стоит повторить; их результаты хранятся только в браузере того, кто на них отвечает, а итоговый обзор сводит первую попытку каждой итоговой проверки в профиль по общим целям.

Как изучать этот курс

Курс задуман для изучения по порядку. Каждый раздел предполагает предыдущие: вывод записывается на языке первого, семантика придаёт значение его формулам, а метатеория сравнивает второй с третьим; пропуск урока рано или поздно заставит к нему вернуться.

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

Наконец, стоит всегда различать, к какому уровню относится каждое утверждение: говорит ли оно что-то внутри языка, как формула, или что-то о нём, как $\Gamma \vdash \varphi$ или $\Gamma \models \varphi$. Это различие, первое среди целей курса, позволяет также понять его центральный результат, который можно сформулировать только в метаязыке.