Язык: введение

Краткое содержание

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

Цели обучения

Описать последовательность содержания раздела и объяснить, что каждый урок даёт следующему.
Поместить раздел в маршрут курса (язык, вывод, семантика и метатеория) и объяснить, почему синтаксис изучается раньше трёх остальных частей.
Объяснить на примере, почему запись со связкой между её аргументами и без скобок неоднозначна и почему язык кружков и дисков не таков.
Распознать то немногое, что предполагает раздел, и организовать его изучение, взяв за отправную точку входную самопроверку.

Входная проверка

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

Содержание раздела

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

Что такое математическая логика. Урок очерчивает предмет дисциплины: не истинность отдельных высказываний, а правильность, то отношение между посылками и заключением, которое гарантирует, что истинность первых переходит на второе. Он отличает правильность от истинности, показывает, почему естественный язык, неоднозначный и способный говорить о себе самом, недостаточен для её изучения, и устанавливает различение языка-объекта и метаязыка. Он разбирает, с явными допущениями, парадоксы лжеца, Берри, брадобрея и Рассела и завершается картой курса.
Язык логики высказываний. Урок излагает необходимое о множествах и цепочках символов, подсчитывает цепочки, которые можно записать двумя символами, и строит базовый язык: бесконечно много переменных, записанных кружками и дисками, единственное правило образования и условие замыкания, из которого выводится принцип для доказательства свойств всех формул. Он даёт разрешающую процедуру, позволяющую решить, является ли цепочка формулой, и строит над базовым языком метаязык, которым мы будем пользоваться в дальнейшем: метапеременные, стрелку Пирса, записанную со скобками, и официальные сокращения остальных связок.
Индукция по натуральным числам и по формулам. Урок излагает индукцию по натуральным числам, простую и сильную, и переносит её на формулы. С её помощью он доказывает лемму о весе, а из неё теорему об однозначности разбора, которую сформулировал предыдущий урок: каждая составная формула разлагается единственным образом. Однозначность разбора, наконец, оправдывает определения по рекурсии на формулах (длина, подформулы, глубина) и подстановку вместо одной подформулы другой.
Формализация естественного языка. Урок наводит мост между русским языком и формальным: словарь формализации, прочтение каждой связки, выведенное из прочтения исходной связки, тонкости «но», «только если» и «если только не», область действия связок, материальная импликация и то, чего логика высказываний выразить не может. Он завершается формализацией полных рассуждений как множества посылок и заключения, которые следующие разделы подвергнут выводу и семантике.

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

Место раздела в курсе

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

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

Почему язык кружков и дисков

Язык курса имеет алфавит всего из двух символов, кружка $\sigO$ и диска $\sigI$ , и единственное правило образования: если $\varphi$ и $\psi$ формулы, то и $\sigI\varphi\psi$ формула. $n$ -я переменная есть цепочка из $n$ кружков, за которыми следует диск, $v_{n} = \sigO^{n}\sigI$ . На первый взгляд выбор странен, потому что записанные так формулы трудно читать. У него, однако, есть четыре точные причины.

Первая состоит в том, что двух символов достаточно, чтобы записать бесконечно много переменных, не выходя за пределы конечного алфавита, так что всякая формула есть, буквально, конечная цепочка символов из множества двух элементов, а вопросы о языке суть вопросы о цепочках, которые можно подсчитывать и сравнивать. Вторая в том, что единственное правило оставляет в каждом доказательстве индукцией единственный случай: то, что доказано для переменных и для $\sigI\varphi\psi$ , доказано для всех формул, без отдельного случая для каждой связки. Третья в том, что правило ставит связку перед двумя её аргументами, как в записи, которую предложил Ян Лукасевич в 1920-х годах, и поэтому не нуждается в скобках: однозначность разбора устанавливается доказательством в одну страницу, которое приписывает каждой переменной вес $+1$ , а каждому диску-связке вес $-1$ . Четвёртая в том, что единственная связка, стрелка Пирса, «ни $\varphi$ , ни $\psi$ », достаточна для выражения всех остальных, как заметил Чарльз Сандерс Пирс около 1880 года и опубликовал Генри Шеффер в 1913 году и как докажет раздел семантики; так что экономность языка не жертвует ничем из того, что может сказать логика высказываний.

Однако ценой этой экономности оказывается удобочитаемость, и раздел платит её в метаязыке: никто не будет ежедневно писать цепочки кружков и дисков, а будет писать их имена, $(\varphi \downarrow \psi)$ , $\neg\varphi$ , $(\varphi \rightarrow \psi)$ , определённые один раз и в любой момент развёртываемые до цепочки, которую они обозначают. Следовательно, курс работает сразу на двух уровнях: минимальный базовый язык, о котором доказывают, и удобная запись, которой пишут; и различение языка-объекта и метаязыка, которое вводит первый урок, позволяет их не смешивать.

Что считается известным

Раздел начинается почти с нуля. Он не предполагает ни изучения логики, ни знания теории множеств, ни опыта доказательства теорем: то, что он использует из теории множеств, излагает второй урок, а то, что использует из индукции, третий. Он предполагает лишь две вещи. Первая: внимательное чтение; в формальном языке добавленный или пропущенный символ меняет цепочку, а порядок слов в определении важен не меньше, чем сами слова. Вторая: элементарная арифметика натуральных чисел, которые в этом курсе суть $1, 2, 3, \ldots$ , то есть умение складывать и умножать, вычислять степени числа $2$ , отличать чётные числа от нечётных и распознавать простое число.

Тот, кто хочет дополнительной опоры для индукции, может обратиться к урокам об аксиомах Пеано и о суммах и индукции из курса «Алгебра и геометрия I»; это не обязательно, потому что третий урок этого раздела излагает индукцию начиная с её формулировки.

Задача, которую решает раздел

Логика изучает правильность, а правильность зависит от формы рассуждений. Но чтобы говорить о форме строго, нужно, чтобы у каждого выражения была только одна форма, а естественный язык этого не гарантирует: «дважды три плюс четыре» может быть $10$ или $14$ , смотря по тому, как группировать. Отсюда две задачи, которые и составляют задачи раздела. Первая состоит в том, чтобы построить язык, в котором у каждого выражения только одно прочтение. Вторая в том, чтобы это доказать: формул бесконечно много, и никакая проверка случай за случаем, сколь бы долгой она ни была, не устанавливает, что у каждой из них только одно прочтение. Следующий пример показывает обе задачи на одном выражении.

ПримерОдно выражение, две цепочки

Выражение $v_{1} \downarrow v_{2} \downarrow v_{3}$ , записанное со связкой между её аргументами и без скобок, не указывает, какая из двух связок главная. В языке кружков и дисков, напротив, каждая группировка есть отдельная цепочка, и сама цепочка говорит, как она группируется.

Доказательство

$((v_{1} \downarrow v_{2}) \downarrow v_{3}) = \resaltar{\sigI\sigI} v_{1} v_{2} v_{3}$
Первое прочтение: первая связка соединяет $v_{1}$ с $v_{2}$ , а вторая главная. В базовом языке оба диска стоят впереди.
$(v_{1} \downarrow (v_{2} \downarrow v_{3})) = \sigI v_{1} \resaltar{\sigI} v_{2} v_{3}$
Второе прочтение: вторая связка соединяет $v_{2}$ с $v_{3}$ , а первая главная. Второй диск стоит между $v_{1}$ и $v_{2}$ .
$\sigI\resaltar{\sigI}\sigO\sigI\sigO\sigO\sigI\sigO\sigO\sigO\sigI \neq \sigI\resaltar{\sigO}\sigI\sigI\sigO\sigO\sigI\sigO\sigO\sigO\sigI$
Записанные кружками и дисками, две цепочки различаются уже вторым символом: это разные формулы.
$\sigI \; \resaltar{\sigI \; v_{1} \; v_{2}} \; v_{3}: \quad -1, \quad 0, \quad +1$
Чтобы разобрать первую цепочку, достаточно считать: после начального диска каждый диск-связка вычитает $1$ , а каждая переменная прибавляет $1$ , и первая компонента кончается там, где сумма впервые достигает $+1$ .
$\sigI \, \resaltar{(\sigI v_{1} v_{2})} \, \resaltar{v_{3}}$
Откуда первая компонента есть $\sigI v_{1} v_{2}$ , а вторая $v_{3}$ : цепочка разбирается согласно первому прочтению, и никак иначе. То, что этот подсчёт работает для всех формул, а не только для этой, и есть теорема об однозначности разбора, которую третий урок доказывает индукцией.

Итак, ответ раздела на эти две задачи состоит из двух частей. Для первой: язык, единственное правило которого ставит связку впереди, так что скобки не нужны, и метаязык, каждое сокращение которого обозначает единственную цепочку. Для второй: принцип доказательства, индукция по сложности формул, которая переходит от конечного числа проверок (переменные и правило) ко всем формулам, так же как индукция по натуральным числам переходит от $1$ и от шага от $k$ к $k + 1$ ко всем числам. С обеими частями форма рассуждения становится точным объектом, и вопрос о его правильности можно строго поставить в следующих разделах.

Как изучать раздел

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

Куда он ведёт

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

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