ch02.tex

\documentclass[../main.tex]{subfiles}
\begin{document}

\Chapter{Содержание и форма в математике}

ЭТА ДВУХГОЛОСНАЯ ИНВЕНЦИЯ оказалась для моих героев вдохновляющей идеей. Так же, как Льюис Кэрролл позволил себе вольное обращение с Ахиллом и Черепахой Зенона, я позволил себе некоторые вольности с Ахиллом и Черепахой Льюиса Кэрролла. У Кэрролла одни и те же события повторяются снова и снова, каждый раз на более высоком уровне; это замечательная аналогия Баховского Естественно Растущего Канона. Если лишить диалог Кэрролла его блестящего остроумия, в нем останется глубокая философская проблема: \emph{подчиняются ли слова и мысли каким-либо формальным правилам?} Это и есть основной вопрос, на который пытается ответить моя книга.

В этой и следующей главах мы рассмотрим несколько новых формальных систем; это поможет нам лучше понять саму идею \emph{формальной системы}. Когда вы дочитаете эти две главы до конца, у вас должно сложиться неплохое представление о мощности формальных систем и о том, почему они представляют интерес для математиков и логиков.


\subsection{Система «pr»}

В этой главе мы будем рассматривать \emph{систему}~\textbf{pr}. Ни математики, ни физики ею не заинтересуются; признаться, она \--- всего лишь мое собственное изобретение. Система~\textbf{pr} интересна лишь постольку, поскольку она хорошо иллюстрирует многие идеи, играющие в этой книге важную роль. В этой системе три символа:
\begin{center}
    \large%
    \textbf{p}\quad\textbf{r}\quad\textbf{--}
\end{center}

--- буквы \textbf{p} и~\textbf{r} и~тире.

Система~\textbf{pr} имеет бесконечное множество аксиом. Поскольку мы не можем записать их все, мы должны придумать какой-нибудь метод их описания. На самом деле, нам нужно не просто описание этих аксиом; нам нужен способ, позволяющий узнать, является ли данная последовательность символов аксиомой. Простое описание аксиом охарактеризовало бы их полностью, но недостаточно сильно; именно в этом была проблема с описанием теорем системы~\textbf{MIU}. Мы не собираемся возиться в течении неопределенного \--- возможно, бесконечного \--- времени, чтобы определить, является ли некая строчка символов аксиомой. Нам необходимо такое определение аксиом, которое предоставит в наше распоряжение надежный алгоритм разрешения, устанавливающий аксиоматичность любой строчки, состоящей из символов \textbf{p},~\textbf{r} и~тире.

\begin{mybox}{ОПРЕДЕЛЕНИЕ}
    \textbf{$x$p-r$x$-} является аксиомой, когда $x$ состоит только из тире.
\end{mybox}

Обратите внимание, что каждый из этих двух $x$-ов замещает одинаковое число тире. Например, \textbf{-{}-p-r-{}-{}-} является аксиомой. Само выражение \textbf{$x$p-r$x$-}, разумеется, не аксиома, так как $x$ не принадлежит системе~\textbf{pr}; оно, скорее, походит на форму, в которой отливаются все аксиомы данной системы. Такая «форма» называется схемой аксиом.

Система~\textbf{pr} имеет только одно правило вывода:

\begin{mybox}{ПРАВИЛО}
    Пусть $x$, $y$ и $z$ \--- строчки, состоящие только из тире.
    % TODO: why comment?
    % Пусть \textit{x}\textbf{p}\textit{y}\textbf{r}\textit{z} является теоремой.
    Пусть \textbf{$x$p$y$r$z$} является теоремой.
    Тогда \textbf{$x$p$y$-$z$-} также будет теоремой.
\end{mybox}

\noindent
Пусть, например, $x$~будет «\textbf{-{}-}», $y$ \--- «\textbf{-{}-{}-}» и $z$ \--- «\textbf{-}».
Правило говорит нам:

\begin{block}
    Если \textbf{-{}-p-{}-{}-r-} является теоремой, то \textbf{-{}-p-{}-{}-{}-r-{}-} также будет теоремой.
\end{block}

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

Очень полезное упражнение \--- попытаться найти разрешающий алгоритм для теорем системы~\textbf{pr}. Это нетрудно \--- после нескольких попыток вы, скорее всего, найдете решение. Попробуйте!


\subsection{Разрешающий алгоритм}

Надеюсь, что вы уже попытались найти решение. Во-первых, хотя это и кажется очевидным, я хотел бы заметить, что каждая теорема системы~\textbf{pr} имеет три отдельных группы тире, и что разделяющими элементами являются \textbf{p}~и~\textbf{r}, именно в таком порядке. (Это можно доказать, основываясь на аргументах «наследственности», так же, как мы смогли доказать, что теоремы системы~\textbf{MIU} всегда должны начинаться с~\textbf{М}.) Это означает, что уже сама форма такой строчки как \textbf{-{}-p-{}-p-{}-p-{}-r-{}-{}-{}-{}-{}-{}-{}-} исключает её из числа теорем.

Читатель может подумать, что, подчеркивая фразу «уже сама форма», автор поступает довольно глупо: что ещё может быть в такой строчке, кроме формы? Что, кроме её формы, может играть какую-либо роль в определении особенностей данной строчки? Совершенно ясно, что ничего больше! Однако имейте в виду, читатель, что по мере того, как мы будем углубляться в обсуждение формальных систем, понятие «формы» будет становиться всё сложнее и абстрактнее и нам придется всё чаще задумываться о значении самого этого слова. Во всяком случае, мы будем называть \emph{«правильно составленной строчкой»} любую строчку следующей структуры: группа тире, одно~\textbf{p}, вторая группа тире, одно~\textbf{r}, завершающая группа тире.

Вернемся к алгоритму разрешения. Для того, чтобы данная строчка считалась теоремой, первые две группы тире в сумме должны давать третью группу тире. Так, например, \textbf{-{}-p-{}-r-{}-{}-{}-} является теоремой, так как 2~плюс~2 равняется~4, в то время как \textbf{-{}-p-{}-r-} теоремой не является, так как 2~плюс~2 не равняется~1. Чтобы понять, почему этот критерий верен, взгляните сначала на схему аксиом. Очевидно, она производит только такие аксиомы, которые удовлетворяют критерию сложения. Теперь обратитесь к правилу вывода. Если первая строчка удовлетворяет критерию сложения, то же условие необходимо будет выполняться и во второй строчке. И,~наоборот, если первая строчка не удовлетворяет критерию сложения, не будет удовлетворять ему и вторая строчка. Это правило превращает критерий сложения в наследственное качество теорем; каждая теорема передает его своим «отпрыскам». Это показывает, почему критерий сложения верен.

Кстати, в системе~\textbf{pr} есть некое свойство, позволяющее нам с уверенностью сказать, что данная система имеет разрешающий алгоритм, ещё до того, как мы нашли критерий сложения. Это свойство заключается в том, что система~\textbf{pr} не усложнена встречными \emph{укорачивающими} и \emph{удлиняющими} правилами;~в ней имеются лишь удлиняющие правила. Любая формальная система, которая говорит нам, как получать более длинные теоремы из более коротких, но никогда не говорит нам обратного, должна иметь алгоритм разрешения для своих теорем. Представьте себе, что вам дана какая-либо строчка. Прежде всего, проверьте, является ли эта строчка аксиомой (я~предполагаю, что у нас имеется алгоритм разрешения для аксиом, иначе наше предприятие было бы безнадежным). Если это аксиома, то, следовательно, по определению она является теоремой, и проверка на этом заканчивается. Предположим теперь, что наша строчка \--- не аксиома. В~таком случае, чтобы быть теоремой, она должна была быть получена из более короткой строчки путем применения одного из правил. Перебирая правила одно за другим, вы всегда можете установить, какие из них были использованы для получения данной строчки, а также какие более короткие строчки предшествуют ей на «генеалогическом древе». Таким образом, проблема сводится к определению того, какие из новых, более коротких строчек являются теоремами. Каждая из них, в свою очередь, может быть подвергнута такой же проверке. В~худшем случае, нам придется проверить огромное количество всё более коротких строчек. Продолжая продвигаться таким образом назад, вы медленно, но верно приближаетесь к источнику всех теорем: схеме аксиом. Строчки не могут укорачиваться бесконечно; в один прекрасный момент вы либо установите, что одна из новых коротеньких строчек является аксиомой, либо застрянете на строчках, которые, не являясь аксиомами, тем не менее, не поддаются дальнейшему сокращению. Таким образом, системы, имеющие лишь удлиняющие правила, не особенно интересны; по-настоящему любопытны лишь системы, где взаимодействуют удлиняющие и укорачивающие правила.


\subsection{Снизу вверх \emph{vs.} сверху вниз}

Метод, описанный выше, можно назвать нисходящим алгоритмом разрешения; сравним его с восходящим алгоритмом, описание которого я сейчас приведу. Он весьма напоминает метод, используемый джинном для производства теорем в системе \textbf{MIU}; однако он несколько осложнен присутствием схемы аксиом. Мы возьмем что-то вроде корзины, куда будем бросать теоремы по мере их рождения.
\begin{itemize}[label={}, noitemsep, topsep=6pt]
    \item (1а) Бросьте в корзину самую простую (\textbf{-p-r-{}-}) из возможных теорем.
    \item (1б) Приложите правило вывода к предмету в корзине и положите в корзину результат.
    \item (3а) Положите в корзину следующую по простоте аксиому.
    \item (3б) Приложите правило в каждому имеющемуся в корзине предмету и бросьте в корзину результаты.
    \item (3а) Положите третью по простоте аксиому в корзину.
    \item (3б) Приложите правило к каждому имеющемуся в корзине предмету и бросьте в корзину результаты.
\end{itemize}

И~т.\,д. и~т.\,п.

Ясно, что, действуя таким образом, вы не можете пропустить не одной теоремы системы \textbf{pr}. С течением времени корзина будет наполняться всё более длинными теоремами; это \--- следствие отсутствия сокращающих правил. Таким образом, если вы желаете проверить, является ли данная строчка (например, \textbf{-{}-p-{}-{}-r-{}-{}-{}-{}-} ) теоремой, вам придется следуя шаг за шагом, бросать в корзину всё новые теоремы и сравнивать их с данной строчкой. Если таковая обнаружится, значит, это \--- теорема. Если же в какой-то момент вы заметите, что все, что попадает в корзину, длиннее искомой строчки, можете прекратить поиски \--- это не теорема. Такой разрешающий алгоритм называется восходящим, так как он исходит из основы, фундамента системы \--- аксиом. Предыдущий алгоритм разрешения, наоборот, спускался сверху, приближаясь к фундаменту системы.


\subsection{Изоморфизмы порождают смысл}

Теперь мы подошли к центральному вопросу данной главы \--- и книги в целом. Возможно, у вас уже мелькнула мысль, что теоремы~\textbf{pr} напоминают сложение. Строчка \textbf{-{}-p-{}-{}-r-{}-{}-{}-{}-} является теоремой, потому что 2~плюс~3 равняется~5. Может быть, вы даже подумали, что теорема \textbf{-{}-p-{}-{}-r-{}-{}-{}-{}-} не что иное как записанное необычной нотацией утверждение, означающее, что 2~плюс~3 равняется~5. На самом деле я нарочно выбрал буквы \textbf{p}~и~\textbf{r}, чтобы напомнить вам о словах «плюс» и «равняется». Так что же, строчка~\textbf{-{}-p-{}-{}-r-{}-{}-{}-{}-} на самом деле означает 2~плюс~3 равняется~5?

Что заставляет нас думать подобным образом? Мне кажется, что в этом виноват замеченный нами изоморфизм между системой~\textbf{pr} и сложением. Во введении термин «изоморфизм» был определен как трансформация, сохраняющая информацию. Теперь мы можем далее углубиться в это понятие и рассмотреть его в иной перспективе. Слово «изоморфизм» приложимо к тем случаям, когда две сложные структуры могут быть отображены одна в другой таким образом, что каждой части одной структуры соответствует какая-то часть другой структуры («соответствие» здесь означает, что эти части выполняют в своих структурах сходные функции). Такое использование слова «изоморфизм» восходит к более точному математическому понятию.

Обнаружить изоморфизм между двумя известными ему структурами \--- большая радость для математика. Часто это открытие изумительно и неожиданно, как гром с ясного неба. Осознание изоморфизма между двумя хорошо известными структурами \--- большой шаг вперед по дороге познания, и я считаю, что именно это порождает значения в человеческом мозгу. Для полноты картины заметим, что поскольку изоморфизмы бывают самых различных типов, иногда не совсем ясно, когда же мы в действительности имеем дело с изоморфизмом. Таким образом, слову «изоморфизм», как и вообще всем словам, присуща некая расплывчатость, что является одновременно и достоинством, и недостатком.

В данном случае, у нас имеется великолепный прототип для понятия «изоморфизм». Во первых, у нас есть «низший уровень» нашего изоморфизма \--- соответствие между частями двух структур:
% TODO: fix
\begin{center}
\setlength{\tabcolsep}{4pt}
\begin{tabular}{r c l}
    \textbf{p} & $\Longleftrightarrow$ & плюс \\
    \textbf{r} & $\Longleftrightarrow$ & равняется \\
    \textbf{-} & $\Longleftrightarrow$ & один \\
    \textbf{-{}-} & $\Longleftrightarrow$ & два \\
    \textbf{-{}-{}-} & $\Longleftrightarrow$ & три \\
    & \clap{и~т.\,д.} \\
\end{tabular}
\end{center}
Подобное соответствие между словами и символами называется интерпретацией.

Во-вторых, на более высоком уровне, у нас имеется соответствие между истинными утверждениями и теоремами. Заметим, однако, что это соответствие высшего уровня не может быть осознано, пока мы не выберем интерпретации для символов. Исходя из этого, правильнее будет говорить о соответствии между истинными суждениями и интерпретированными теоремами. В любом случае, мы установили соответствие между двумя порядками \--- нечто типичное для изоморфизма. Когда вы имеете дело с формальной системой, о которой ничего не знаете и в которой желаете найти скрытое значение, ваша задача \--- интерпретировать символы таким образом, чтобы установить соответствие между истинными высказываниями и теоремами. Возможно, что сначала вам придется искать наугад, прежде чем вы найдете набор слов, подходящий для ассоциации с символами системы. Эта процедура весьма напоминает попытки расшифровать секретный код или прочитать надпись на незнакомом языке, как, например, критский линейный~В: единственный возможный путь состоит в использовании метода проб и ошибок, а также «разумных» догадок. Когда вы найдете правильный, «значащий» вариант, внезапно всё приобретает смысл, и работа начинает идти во много раз быстрее. Очень скоро всё встает на свои места. Счастливое волнение, испытываемое при этом исследователем, хорошо описано Джоном Чадвиком в его книге «Расшифровка линейного языка~В» (John Chadwick, \textit{The Decipherment of Linear~B}).

Однако мало кому приходится расшифровывать формальные системы, найденные в раскопках древних цивилизаций. Больше всего с формальными системами имеют дело математики (а в последнее время также лингвисты, философы и некоторые другие ученые); они придерживаются определенной интерпретации в формальных системах, которые они изучают и используют. Эти специалисты пытаются создать такую формальную систему, теоремы которой изоморфно отражали бы какие-либо фрагменты действительности. В этом случае выбор символов так же важен, как выбор типографских правил вывода. Задумав систему~\textbf{pr}, я очутился как раз в таком положении. Читателю, вероятно, уже понятно, почему я выбрал именно такие символы. Теоремы системы~\textbf{pr} не~случайно изоморфны сложению; это получилось потому, что я искал способ представить сложение типографским путем.


\subsection{Интерпретации значащие и незначащие}

Вы можете выбрать интерпретации, отличные от моей. При этом не~обязательно, чтобы каждая теорема оказывалась истинной. Однако какой смысл в такой интерпретации, при которой, скажем, все теоремы оказывались бы ложными? Еще более бессмысленной выглядит интерпретация, при которой теоремы вообще никоим образом не соотносятся с критериями истинности или ложности. Нам придется поэтому различать два типа интерпретации формальных систем. Во-первых, мы можем говорить о \emph{незначащей} интерпретации, которая не~устанавливает никакой изоморфной связи между теоремами системы и реальностью. Подобных интерпретаций сколько угодно, годится любой случайный выбор. Возьмем, например, такую интерпретацию:
\begin{center}
    \setlength{\tabcolsep}{4pt}
    \begin{tabular}{r c l}
        \textbf{p} & $\Longleftrightarrow$ & лошадь \\
        \textbf{r} & $\Longleftrightarrow$ & счастливая \\
        \textbf{-} & $\Longleftrightarrow$ & яблоко \\
    \end{tabular}
\end{center}

Теперь строчка \textbf{-p-r-{}-} приобретает новую интерпретацию «Яблоко лошадь яблоко счастливая яблоко яблоко». Это поэтическое выражение, пожалуй, может понравиться лошадям и даже показаться им наилучшей интерпретацией строчек данной системы. Однако в такой интерпретации весьма мало «осмысленности», теоремы системы звучат ничуть не истинней и не лучше, чем не-теоремы. Утверждение «счастливая счастливая счастливая яблоко лошадь» (соответственно, \textbf{rrr-p}) доставит нашей лошадке точно такое же удовольствие, как и любая интерпретированная теорема.

Другой тип интерпретации может быть назван \emph{значащим}. В такой интерпретации, теоремы и истины совпадают \--- то есть, между теоремами и фрагментами реального мира существует изоморфизм. По этой причине мы будем различать \emph{интерпретацию} и \emph{значение}. Интерпретацией~\textbf{p} могло бы быть любое слово, но «плюс» кажется мне единственным \emph{значащим} вариантом. Короче, наиболее вероятно что значение~«\textbf{p}» \--- «плюс», хотя этот символ может иметь миллион различных интерпретаций.


\subsection{Активные и пассивные значения}

Возможно, что прочитавшие внимательно эту главу найдут самым важным в ней следующий факт: система~\textbf{pr}, по всей видимости, заставляет нас признать, что \emph{поначалу абстрактные символы неизбежно приобретают некое значение, по крайней мере, если мы находим какой-либо изоморфизм}. Однако между значением в формальных системах и значением в языке есть важное различие. Различие это заключается в том, что, выучив значение какого-либо слова, мы составляем затем новые предложения, основанные на этом значении. В определенном смысле значение становится \emph{активным}, так как оно порождает новые правила создания предложений. Это означает, что наше владение языком не является законченным продуктом, правил производства предложений становится всё больше по мере того, как мы выучиваем новые значения. С другой стороны, в формальных системах теоремы предопределены правилами вывода. Мы можем выбирать «значения», основанные на изоморфизме (если таковой удается найти) между теоремами и истинными утверждениями. Однако это ещё не разрешает нам по своему усмотрению прибавлять новые теоремы к уже имеющимся в системе. Именно об этом предупреждало нас в первой главе правило формальности.

В системе~\textbf{MIU}, разумеется, у нас не возникает искушения выйти за пределы четырех правил, так как мы не собираемся искать в ней никаких интерпретаций. Однако здесь, в нашей новой системе, мы можем соблазниться новоприобретенным «значением» каждого символа и решить, что строчка
\begin{center}
    \textbf{-{}-p-{}-p-{}-p-{}-r-{}-{}-{}-{}-{}-{}-{}-}
\end{center}
является теоремой. По крайней мере, у нас может появиться такое \emph{желание}; однако это не меняет того факта, что эта строчка \--- не теорема. Было бы грубой ошибкой думать, что она «должна» быть теоремой, только лишь потому, что 2~плюс 2 плюс 2 плюс~2 равняется~8. Более того, было бы неверно приписывать этой строчке вообще какое бы то ни было значение, поскольку она не является правильно построенной, в то время как наша интерпретация полностью выводится из наблюдения над правильно построенными строчками.

В формальной системе значение должно оставаться \emph{пассивным}; мы можем прочитывать каждую строчку в зависимости от значения символов, её составляющих, но нам не позволено создавать новые теоремы,основываясь назначениях, которые мы придаем этим символам. Интерпретированные формальные системы находятся на границе между системами без значения и системами со значением. Мы можем считать, что их строчки что-то выражают, но это является не более как следствием формальных особенностей данной системы.


\subsection{Double-entendre!}

А теперь я хочу рассеять ваши иллюзии по поводу того, что мы нашли единственно правильное значение для символов системы~\textbf{pr}. Рассмотрим следующее соотношение:
\begin{center}
    \setlength{\tabcolsep}{4pt}
    \begin{tabular}{r c l}
        \textbf{p} & $\Longleftrightarrow$ & равняется \\
        \textbf{r} & $\Longleftrightarrow$ & отнятое от \\
        \textbf{-} & $\Longleftrightarrow$ & один \\
        \textbf{-{}-} & $\Longleftrightarrow$ & два \\
        & \clap{и~т.\,д.} \\
    \end{tabular}
\end{center}

Теперь \textbf{-{}-p-{}-{}-r-{}-{}-{}-{}-} приобретает новое значение: «2~равняется 3 отнятым от~5». Разумеется, это истинное утверждение; более того, в новой интерпретации все теоремы системы будут истинны. Новая интерпретация ровно настолько же осмыслена, насколько и прежняя. Ясно, что глупо спрашивать, какое из двух значений является истинным \emph{на самом деле}. Любая интерпретация истинна, если только она аккуратно отражает определенный изоморфизм с действительностью. Когда какие-либо аспекты действительности (в данном случае, сложение и вычитание) изоморфны между собой, одна и та же система может быть изоморфна обоим этим аспектам и в результате иметь два пассивных значения. Тот факт, что одни и те же символы могут иметь различные значения, чрезвычайно важен. В нашем примере это могло показаться вам тривиальным, или любопытным, или вообще неинтересным; однако когда мы вернемся к этой теме в более сложном контексте, читатель увидит, какое богатство идей она заключает.

Подведем итоги тому, что мы сказали о системе~\textbf{pr}. В каждой из двух значащих интерпретаций, любая правильно построенная строчка соответствует какому-либо грамматическому высказыванию. Некоторые из этих высказываний окажутся истинными, некоторые \--- ложными. В~любой формальной системе \emph{правильно построенными строчками} являются те, которые, будучи проинтерпретированы символ за символом, порождают грамматические высказывания. (Безусловно, это зависит от самой интерпретации, но обычно мы уже имеем в виду какую-то одну из них.) Среди правильно построенных строчек некоторые являются теоремами. Теоремы определяются схемой аксиом и правилом вывода. Моей целью, когда я придумывал систему~\textbf{pr}, являлась имитация сложения: каждая теорема, интерпретированная определенным образом, выражает истинный пример сложения; наоборот, каждое уравнение сложения двух целых положительных чисел может быть записано в форме строчки, оказывающейся теоремой. Эта цель была достигнута. Таким образом, заметьте, что все ошибочные примеры сложения, такие, как, например, 2~плюс~3 равняется~6, соответствуют правильно построенным строчкам, которые, однако, не~являются теоремами.


\subsection{Формальные системы и действительность}

Это был наш первый пример того, как формальная система может быть основана на фрагменте действительности и точно отображать его в том смысле, что теоремы этой системы изоморфны истинным утверждениям данной части действительности. Однако надо иметь в виду, что действительность и формальные системы не зависят друг от друга. Никто не обязан знать об изоморфизме между ними. Каждая из этих систем существует сама по себе: 1~плюс~1 равняется~2, независимо от того, знаем ли мы, что \textbf{-p-r-{}-} является теоремой; с другой стороны, \textbf{-p-r-{}-} является теоремой, независимо от того, соотносим ли мы её с примером сложения.

Читатель может спросить, помогает ли создание этой (или любой другой) формальной системы узнать что-либо новое об области её интерпретации. Выучили ли мы какие-нибудь новые примеры сложения путем производства \textbf{pr}-теорем? Разумеется, нет; однако мы узнали что-то новое о самом процессе сложения, а именно, что оно легко может быть имитировано с помощью типографского правила, управляющего абстрактными символами. Это пока не~удивительно, так как сложение \--- весьма простое понятие. Всем известно, что суть сложения может быть «уловлена» скажем, при наблюдении за вращающимися шестеренками кассового аппарата.

Ясно, что мы затронули лишь самые начатки формальных систем; естественно, возникает вопрос, какие именно фрагменты действительности могут быть отражены при помощи набора бессмысленных символов, управляемых формальными законами? Может ли вся реальность быть превращена в формальную систему? В очень широком смысле кажется, что на этот вопрос можно ответить положительно. Мы можем предположить, например, что вся действительность \--- это не более чем весьма сложная формальная система. Её символы находятся не на бумаге, а в трехмерном вакууме (пространстве); это элементарные частицы, из которых устроена вселенная. (Мы предполагаем здесь, что материя не делится до бесконечности, и что, таким образом, выражение «элементарные частицы» имеет смысл.) «Типографские правила» такой формальной системы \--- законы физики, которые, учитывая положение и скорость всех частиц в данный момент, говорят нам, какие изменения произойдут, и каковы будут новая скорость и положение частиц в «следующий» момент. Таким образом, теоремами этой огромной формальной системы являются все возможные конфигурации частиц во все времена истории вселенной. Единственной аксиомой здесь является (или являлось) первоначальное положение всех частиц в «начале времен». Однако это концепция столь грандиозна, что представляет лишь сугубо теоретический интерес; к тому же, достижения квантовой механики (и других областей физики) вносят некие сомнения даже и в чисто теоретическую ценность этой идеи. Проблема сводится к вопросу, функционирует ли вселенная по законам детерминизма; этот вопрос пока остается открытым.


\subsection{Математика и манипуляция символами}

Вместо того, чтобы иметь дело с такой огромной картиной, возьмем в качестве нашей «действительности» математику. Тут мы сталкиваемся с серьезным вопросом: можем ли мы быть уверены в точности нашей формальной системы, моделирующей какую-либо область математики, в особенности, если мы ещё не изучили данную часть математики вдоль и поперек? Предположим, что цель формальных систем \--- дать нам новые знания по данной дисциплине. Каким образом мы узнаем, что интерпретация каждой теоремы истинна? Для этого пришлось бы доказать, что между формальной системой и данной частью математики существует полный изоморфизм. С другой стороны, подобное доказательство возможно только в том случае, если нам с самого начала уже известны все истинные утверждения данной дисциплины!

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

В таком же положении мы оказываемся, когда пытаемся при помощи типографских символов формальной системы описать фрагмент действительности, представленный натуральными числами (то-есть, неотрицательными целыми числами: 0,~1,~2,\ldots). Попробуем понять отношение между тем, что мы называем «истиной» в теории чисел, и тем, к чему мы можем придти путем манипуляции символами.

Для начала посмотрим, какие основания у нас существуют для того, чтобы называть одни утверждения теории чисел истинными, а другие \--- ложными? Сколько будет 12 умножить на~12? Любой знает, что~144. Однако многие ли из тех, кто уверенно дает этот ответ, когда-либо рисовали прямоугольник размером 12 $\times$ 12 и подсчитывали составляющие его квадратики? Большинство людей считают, что эта процедура совсем не нужна. Вместо нее в доказательство своей правоты они предлагают несколько значков на бумаге, вроде тех, что показаны ниже:
\[
    % `xlop` package
    \opmul{12}{12}
\]
Это и будет «доказательством». Почти все верят, что если посчитать квадратики, получится 144; мало кто когда-либо усомнился в этом результате. Конфликт между двумя точками зрения становится ещё заметнее, когда мы рассматриваем такую проблему, как нахождение произведения \num{987654321} $\times$ \num{123456789}. Прежде всего, практически невозможно построить прямоугольник нужного размера; но хуже всего то, что, даже если бы нам и удалось таковой построить и армии людей потратили бы столетия на подсчет квадратиков, всё равно конечному результату поверил бы разве что особенно доверчивый человек. Слишком велика вероятность того, что кто-нибудь обязательно что-то напутал. Возможно ли, в таком случае, узнать ответ? Да, если вы доверяете символическому процессу манипуляции числами при помощи некоторых простых законов. Этот процесс объясняют детям как способ нахождения верного ответа; при этом мало кто из них видит, какой смысл скрывается за этим арифметическим трюком. Правила, маневрирующие цифрами при умножении, основаны на нескольких основных свойствах сложения и умножения, которые считаются верными для всех чисел.


\subsection{Основные законы арифметики}

Свойства, которые я имею в виду, можно пояснить на следующем примере. Представьте, что вы выкладываете несколько палочек:
\[
    \bm{/~~~/~/~~~/~/~~~/~/~~~/~~~/}
\]
и начинаете их считать. В то же время кто-то подсчитывает эти же палочки, начиная с другого конца. Читателю, вероятно, понятно, что результат получится одинаковый. Результат подсчета не зависит от того, как этот подсчет делается. Было бы бессмысленно пытаться доказать это предположение о свойствах сложения, настолько оно первично: либо вы его понимаете, либо нет \--- но в последнем случае вам не поможет никакое доказательство. Из этого предположения вытекают свойства коммутативности и ассоциативности сложения (первое заключается в том, что $b + c = c + b$ во всех случаях; второе \--- в том, что $b + (c + d) = (b + c) + d$ во всех случаях). То же предположение приводит нас к свойствам коммутативности и ассоциативности в умножении; достаточно представить множество кубиков, собранных вместе таким образом, что они составляют большое прямоугольное твердое тело. Коммутативность и ассоциативность умножения означают, что как бы вы ни поворачивали это тело, количество кубиков в нем не изменится. Эти предположения невозможно проверить во всех случаях, так как количество комбинаций бесконечно. Мы принимаем их как данное и верим в них (если мы вообще когда-нибудь о них задумываемся) так глубоко, как только можно во что-либо верить. Количество монет у нас в кармане не меняется оттого, что при ходьбе они перемещаются и бренчат; количество наших книг не изменится, если мы упакуем их в коробку, бросим коробку в багажник машины, отъедем на 100~километров, распакуем коробку и поставим книги на новую полку. Всё это \--- часть того, что мы понимаем под словом \emph{число}.

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

Все мы любим изобретать поговорки, которые, нарушая основные законы арифметики, иллюстрируют некие более глубокие «истины»: «1~да~1 равно~1» (любовники) или «1~плюс 1 плюс~1 равно~1» (святая Троица). Можно легко найти изъяны в подобных «формулах» \--- скажем, показав, что употребление знака «плюс» в них неверно. Так или иначе, подобных высказываний множество. По забрызганному дождем оконному стеклу сползают две капли; у самой рамы они сливаются в одну. Значит ли это, что $1 + 1 = 1$? Из одного облака рождаются два; не доказательство ли это той же идеи? Отличить случаи, в которых мы можем говорить о сложении, от тех, где нам нужно какое-то другое понятие, не так-то просто. Размышляя об этом, мы, возможно, додумаемся до таких критериев, как разделение объектов в пространстве и их четкое отличие друг от друга. Но как подсчитать идеи? Или количество газов в атмосфере? Во многих источниках можно встретить высказывания типа: «В Индии 17~языков и 462~диалекта». В точных утверждениях такого рода есть нечто странное, так как сами понятия «язык» и «диалект» довольно расплывчаты.


\subsection{Идеальные числа}

В повседневном мире числа часто ведут себя плохо. Однако у людей имеется врожденное, пришедшее из древности чувство, что этого быть не должно. В абстрактном понятии числа, взятого вне связи с подсчетом бусинок, диалектов или облаков, есть нечто чистое и точное; должен существовать способ говорить о числах, не примешивая к ним глупую повседневность. Твердые правила, управляющие идеальными числами, являются основой арифметики, в то время как их следствия лежат в основе теории чисел. При переходе от чисел как объектов повседневной жизни к числам как объектам формальной системы возникает следующий важный вопрос: возможно ли заключить всю теорию чисел в рамки одной формальной системы? Действительно ли числа так чисты, ясны и регулярны, что их природа может быть полностью описана правилами какой-либо формальной системы? Картина «Освобождение», одно из самых прекрасных произведений Эшера, иллюстрирует этот удивительный контраст между формальным и неформальным и поразительную зону перехода между ними. Действительно ли числа свободны, как птицы? Страдают ли они, уловленные в тесную клетку формальной системы? Существует ли магическая зона перехода между числами, используемыми в повседневной жизни, и числами, написанными на бумаге?

Говоря о свойствах натуральных чисел, я имею в виду не только такие свойства, как, скажем, сумма определенной пары чисел. Её легко можно подсчитать; никто из нас, выросших в двадцатом веке, не сомневается в возможности механизации таких процессов, как подсчет, сложение, умножение, и~т.\,д.\@ Я имею в виду такие свойства чисел, исследованием которых занимаются математики и для познания которых не достаточно, даже теоретически, никакого подсчета. Рассмотрим классический пример: утверждение «существует бесконечно много простых чисел». Прежде всего, не существует такого метода подсчета, который мог бы доказать или опровергнуть это утверждение. Лучшее, что мы можем сделать, \--- это затратить некоторое время на подсчет простых чисел и заключить, что их действительно имеется «целая куча». Однако никакой подсчет не скажет нам того, конечно или бесконечно количество простых чисел; любой подсчет всегда останется неполным. Это утверждение, называющееся «Теорема Эвклида» (обратите внимание на заглавную~«Т»), совсем не очевидно. Однако со времен Эвклида все математики считают его истинным. В чем же дело?

% illustration 13
\adjustimage{
    max width=\textwidth,
    max totalheight=\textheight-\baselineskip-\abovecaptionskip-\belowcaptionskip-3pt,
    center,
    caption={М.\,К.~Эшер «Освобождение» (литография, 1955)},
    label={fig:escher-liberation},
    figure,
}{escher-liberation.png}


\subsection{Доказательство Эвклида}

Дело в том, что этот факт следует из неких рассуждений. Давайте проследим за этими \emph{рассуждениями}. Рассмотрим вариант доказательства Эвклида, показывающий, что какое бы число мы ни взяли, всегда найдется большее простое число. Возьмем число~$N$. Перемножим все положительные целые числа, начиная с~1 и кончая~$N$; иными словами, найдем факториал~$N$ (он~пишется~«$N!$»). Полученный результат делится на все числа, меньшие чем~$N$. Если прибавить 1 к~$N!$, то результат
%
\begin{itemize}[label={}, noitemsep, topsep=6pt]
    \item не будет делиться на 2 (так как при делении на 2 получится 1 в остатке);
    \item не будет делиться на 3 (так как при делении на 3 получится 1 в остатке);
    \item не будет делиться на 4 (так как при делении на 4 получится 1 в остатке);
    \item $\vdots$
    \item не будет делиться на $N$ (так как при делении на N получится 1 в остатке);
\end{itemize}

Другими словами, если $N! + 1$ и делимо на какое-то число, кроме самого себя и единицы, оно делимо только на числа, большие, чем~$N$. Следовательно, либо $N! + 1$ само простое число, либо его простые делители больше~$N$. В любом случае, мы показали, что должно существовать простое число, большее~$N$, и что, следовательно, количество простых чисел бесконечно.

Кстати, этот последний шаг называется \emph{обобщением}; мы ещё встретимся с этим понятием в более сложном контексте. Оно заключается в том, что, начав наши рассуждения с какого-либо числа~$N$, мы указываем, что $N$ может быть любым числом \--- следовательно, наше доказательство носит общий характер.

Эвклидово доказательство типично для так называемой «реальной математики». Оно просто, точно и изящно и иллюстрирует тот факт, что несколько коротких шагов могут увести нас весьма далеко от начального пункта. В нашем случае, таким начальным пунктом являлись основные идеи о свойствах умножения, деления, и так далее. Короткие шаги \--- это этапы рассуждения. Хотя каждый отдельный шаг кажется очевидным, конечный результат таковым не является. Нам никогда не удастся проверить, верно ли это утверждение Эвклида; однако мы верим в его истинность, поскольку мы верим в логические рассуждения. Если вы принимаете эти рассуждения, вам не остается выхода; раз вы согласились выслушать Эвклида, вам придется согласиться с его выводом. Этот отрадный факт означает, что математики всегда могут придти к согласию по поводу того, какие утверждения считать «истинными», а какие \--- «ложными».

Это доказательство \--- пример упорядоченного процесса мысли. Каждое утверждение соотносится с предыдущим неоспоримым образом; именно поэтому мы говорим скорее о «доказательстве», чем об «очевидном свидетельстве». Целью математики всегда являлось нахождение строгого доказательства какого-либо неочевидного утверждения. Сам факт строгого соотношения шагов доказательства указывает на то, что должна существовать определенная схема, связывающая эти утверждения в одно логическое целое. Об этой схеме лучше всего рассуждать при помощи специального нового лексикона, состоящего из символов, годных только для описания утверждений о числах. Таким образом, мы сможем рассмотреть версию доказательства в «переводе». Это будет набор утверждений, строго соотносящихся между собой; причем эти отношения всегда можно описать. Утверждения, поскольку они записаны компактными, стилизованными символами, выглядят как определенные \emph{структуры}. Другими словами, при прочтении вслух мы видим, что эти утверждения говорят о числах и их свойствах; записанные же на бумаге, они выглядят как абстрактные структуры. Таким образом, последовательно, строка за строкой прочитанная схема доказательства начинает казаться постепенной трансформацией структур по определенным типографским правилам.


\subsection{Минуя бесконечность}

Хотя Эвклид доказывает, что \emph{каждое} число обладает определенным свойством, он, тем не менее, не рассматривает в отдельности каждый из бесконечно многих случаев. Для этого он использует выражения типа «каким бы числом N ни было», или «неважно, какое N мы возьмем». Мы могли бы перефразировать доказательство, используя фразу «все~N». Умело обращаясь с подобными выражениями, мы всегда можем избежать возни с бесконечным количеством утверждений. Вместо этого мы будем иметь дело лишь с двумя-тремя понятиями, например, такими, как слово «все». Сами по себе конечные, они воплощают в себе бесконечность и поэтому позволяют нам обойти такое препятствие, как необходимость доказывать бесконечное количество фактов.

Мы используем слово «все» по-разному, что определено нашим мыслительным процессом: существуют правила, которым подчиняется наш выбор. Возможно, что мы не сознаем этого и утверждаем, что руководствуемся \emph{значением} слова; однако это лишь иносказание, выражающее всё ту же идею; наше мышление подчиняется определенным негласным законам. Всю жизнь мы используем слова как часть определенных структур; но, вместо того, чтобы называть эти структуры «правилами», мы приписываем их возникновение и развитие «значениям» слов. Это открытие было решающим шагом на пути формализации теории чисел.

Рассмотрев доказательство Эвклида более внимательно, мы увидели бы, что оно складывается из многих крохотных, почти бесконечно малых шагов. Если бы мы записали их одно за другим, доказательство показалось бы невероятно сложным. Оно кажется нам легче, когда несколько шагов складываются на манер телескопа и составляют одно-единственное предложение. Если бы мы рассмотрели это доказательство, как в замедленной съемке, перед нами предстали бы отдельные «секции». Другими словами, деление может идти лишь до определенного предела, за которым мы сталкиваемся с «атомной» природой мыслительных процессов. Доказательство может быть разбито на серию крохотных, но отдельных этапов; рассмотренные «издалека», они сливаются в непрерывный поток. В главе VIII я приведу пример такой «атомизации» доказательства, и вы увидите, какое множество шагов в нем участвует. Возможно, что это вас не удивит. В мозгу у Эвклида, когда он изобретал свое доказательство, работали миллионы нейронов, многие из которых давали сотни импульсов в секунду. Чтобы произнести одно-единственное предложение, в мозгу задействованы сотни тысяч нейронов. Если мысли Эвклида были настолько сложны, логично ожидать, что его доказательство также состоит из огромного количества шагов! (Хотя, скорее всего, прямой связи между нейронной активностью мозга и доказательством в нашей формальной системе не существует, они, тем не менее, сравнимы по своей сложности \--- словно природа желает сохранить сложность доказательства бесконечного множества простых чисел, несмотря на то, что это доказательство представлено в таких различных системах.)

В последующих главах мы разработаем такую формальную систему, которая (1)~включает стилизованный лексикон, способный выразить все высказывания о натуральных числах и (2)~имеет правила, соответствующие всем необходимым типам рассуждений. При этом возникает вопрос, сравнима ли мощность подобных формальных правил (по крайней мере, в сфере теории чисел) с мощностью тех правил, которыми мы регулярно пользуемся в наших мыслительных процессах. Иными словами, существует ли теоретическая возможность, используя формальную систему, достичь уровня наших мыслительных способностей?

\end{document}