Стремление придать бóльшую убедительность математическим доказательствам привело к появлению так называемого аксиоматического метода. Если говорить вкратце, он состоит в следующем. Выбирают основные положения рассматриваемой математической теории, которые принимают без доказательств, а из них уже все остальные положения выводят чисто логическими рассуждениями. Эти основные положения получили название аксиом, а те, которые из них выводятся, – теорем. Ясно, что всякая аксиома также выводится из списка аксиом, поэтому удобно аксиомы рассматривать как частный случай теорем (в противном случае слову «теорема» надо было бы дать такое длинное определение: теорема – это то, что выводится из списка аксиом, однако в этот список не входит).

Первая попытка создать систему аксиом для какой-нибудь теории была предпринята Евклидом в III в. до н. э. Система аксиом из его «Начал» оставалась единственной системой аксиом геометрии вплоть до конца XIX в., когда появились новые системы, отвечающие современным требованиям. Вот как Евклид определяет, что такое точка и что такое прямая: «Точка есть то, что не имеет частей», «Прямая линия есть та, которая равно расположена к точкам на ней». С современных позиций эти определения непонятны и не могут быть использованы в доказательствах.

А как же определяются точка и прямая в современных аксиоматических системах? Ответ может удивить неискушённого читателя (искушённого читателя ничто не может удивить). Эти понятия не определяются никак. Не определяется и значение выражений «точка лежит на прямой», «прямая проходит через точку». Если вдуматься, то чего-то подобного, т. е. предъявления основных понятий без определения, и следовало ожидать, ведь всё определить невозможно: одно определяется через другое, другое – через третье, и где-то приходится остановиться. Уж лучше сделать такую остановку честно и открыто. Спрашивается: а как же в таком случае можно использовать эти понятия в доказательствах? Вот тут на помощь и приходят аксиомы.

В аксиомах вместо определений основных понятий формулируются их главные исходные свойства. На эти свойства и опираются доказательства. Поясним сказанное на примере. Среди основных понятий геометрии присутствуют такие: 'точка', 'прямая', 'лежать на', 'лежать между'. Что такое точки и прямые, не разъясняется, а говорится лишь, что бывают такие объекты: одни называются точками, другие – прямыми. А про лежать на говорится, что это некоторое отношение между точками и прямыми. Это означает следующее: если взять произвольную точку и произвольную прямую, то осмысленно спросить, лежит ли эта точка на этой прямой; точка либо лежит на прямой, либо нет. А вот спрашивать, скажем, лежит ли прямая на прямой, бессмысленно: отношение 'лежать на' для пары прямых не определено, как не определено оно и для пары точек, и для пары (прямая, точка). Лежать между – это некоторое трёхместное отношение между точками; сказанное означает, что если даны три точки A, B, C, то точка B либо лежит между точками A и C, либо нет. Природа предметов 'точка' и 'прямая' и отношений 'лежать на' и 'лежать между' никак не раскрывается. Вместо этого в аксиомах формулируются основные свойства этих объектов и отношений и основные связи между ними. Вот как выглядят некоторые из аксиом:

1. На каждой прямой лежат по меньшей мере две точки.

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

3. Если три точки таковы, что одна из них лежит между двумя другими, то все эти три точки различны.

4. Если три точки таковы, что одна из них лежит между двумя другими, то все эти три точки лежат на одной прямой.

5. Для любых двух различных точек A и B существует такая точка С, что B лежит между A и C.

Покажем на примере, как на основе аксиом совершаются доказательства. Докажем, опираясь на выписанные пять аксиом, такую теорему: на каждой прямой лежат по меньшей мере три точки.

Вот доказательство. Итак, пусть p – прямая. Надо обнаружить на ней три различные точки. По аксиоме 1 на ней лежат какие-то две различные точки; обозначим их A и B. По аксиоме 5 находим такую точку C, что B лежит между A и C. Согласно аксиоме 3, все они различны, а согласно аксиоме 4, все они лежат на одной прямой. Обозначим эту прямую буквой q. Точки A и B лежат на прямой p и в то же время лежат на прямой q. Но в силу аксиомы 2 две различные точки не могут лежать на двух различных прямых; следовательно, q совпадает с p. Поскольку через q была обозначена та прямая, на которой лежат все три точки A, B и C, а q совпадает с p, то все эти точки лежат на p. Вот мы и нашли на p три различные точки.

Казалось бы, тем же способом можно далее доказать, что на p лежат четыре точки: надо применить аксиому 5 к точкам B и C и получить такую точку D на той же прямой, что C лежит между B и D. Действительно, все точки B, C и D будут различны; однако ведь может случиться, что точка D совпадает с точкой А, из аксиом не вытекает, что такое невозможно!

Ещё один пример. Дано множество N каких-то объектов. Задана операция, которая каждому объекту из множества N ставит в соответствие некоторый другой (а впрочем, может случиться, что и тот же самый) объект из того же множества N. Объект, ставящийся в соответствии объекту x, будем обозначать как х'. Некоторый объект из множества N выделен особо, его будем обозначать как 0. Всё это подчиняется двум аксиомам.

I. Если х' = у', то x = y.

II. Не существует такого x, что х' = 0.

Требуется доказать утверждение 0'''' ≠ 0''.

Доказываем от противного. Предположим, что 0'''' = 0''.

Тогда в силу первой аксиомы 0''' = 0'. В силу той же первой аксиомы 0'' = 0. Но это противоречит второй аксиоме, потому что получается, что 0 есть результат применения операции «'» к объекту 0'. Точно так же доказывается различие любых двух объектов вида 0''…', имеющих в своей записи различное количество штрихов. Поэтому выражения 0, 0', 0'', … часто используются в качестве обозначений натуральных чисел (включая ноль). Если принять эти обозначения, то видно, что только что была доказана формула 4 ≠ 2.

Заметим, что доказательства в обоих примерах понимались в соответствии с разъяснениями, предложенными в начальном разделе данного очерка, как убедительные рассуждения. Специфика состояла в том, что мы не знали, о каких сущностях идёт речь. Мы не знали, что такое точка, прямая, отношение 'лежать на' и 'лежать между' в первом примере. Во втором примере мы не знали, ни какие объекты образуют множество N, ни который из них выделен, ни в чём состоит операция «'», ставящая в соответствие каждому объекту x объект х'. Мы знали лишь те свойства этих таинственных сущностей, которые были перечислены в аксиомах, и именно на эти свойства, и только на них, опирались в рассуждениях, образующих доказательства. Таким образом, сами наши доказательства были неформальными, психологическими. Поэтому тот вариант аксиоматического метода, который был проиллюстрирован на двух примерах, принято называть неформальным аксиоматическим методом.

Формальный аксиоматический метод отличается от неформального тем, что совершенно чётко определяет не только исходные понятия и записанные в виде аксиом исходные положения, но и дозволенные способы рассуждения. Точно указываются допустимые логические переходы. Более того, и аксиомы, и разрешённые логические переходы должны быть оформлены таким образом, чтобы первые можно было использовать, а вторые – делать чисто механически, не вникая в их содержание, так чтобы и то и другое было по силам исполнительному лаборанту, а теперь и компьютеру. Для этого нужно уметь оперировать с используемыми в доказательствах утверждениями, опираясь только на их внешний вид, а не на содержание, непонятное ни лаборанту, ни компьютеру. Такое оперирование довольно затруднительно, если утверждения записаны на естественном языке, т. е. на одном из тех языков, которыми пользуются люди в повседневной жизни. Приходится записывать утверждения на специальном языке, отражающем структуру утверждений.

Скажем, тот факт, что из A следует B, на русском языке может быть записан многими разными способами: «из A следует B», «из A вытекает B», «если A, то B», «B верно при условии, что верно A», «B верно при условии, что справедливо A», «B справедливо при условии, что верно А» – и ещё многими другими, которые, без сомнения, сможет предложить любезный читатель. Заставить компьютер во всём этом разбираться было бы слишком накладно. А ведь помимо русского языка существует ещё немало других. В специальном, искусственном языке математической логики (точнее было бы сказать – в одном из орфографических вариантов такого языка) указанный факт записывается так: (A ⇒ B). Аналогично, вместо того чтобы анализировать все способы, которыми в русском языке можно выразить тот факт, что утверждение A неверно, пишут просто ¬A.

Вот здесь скрыто очень важное отличие формального аксиоматического метода от неформального. Для неформального метода несущественно, на каком языке – древнегреческом, русском или китайском – записаны утверждения. Для формального метода утверждений вне способов записи как бы не существует. Поэтому грамотнее говорить, что формальный метод имеет дело не с утверждениями, а с предложениями.

Посмотрим, например, как рассуждение от противного выглядит в рамках формального метода. На содержательном уровне это рассуждение происходит по следующей схеме:

из двух утверждений, (1) и (2):

(1) B,

(2) из утверждения не-A (т. е. из отрицания утверждения A) следует утверждение не-B (т. е. отрицание утверждения B) –

вытекает утверждение A.

В формальном методе указанное содержательное рассуждение оформляется в виде такого правила: если доказано предложение B и доказано предложение (¬A ⇒ ¬B), то считается доказанным и предложение A.

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

Проиллюстрируем сказанное на примере того, как в формальном методе доказывается утверждение 0'''' ≠ 0'', содержательный вывод которого из аксиом-утверждений был приведён выше.

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

Символы алфавита принято называть буквами, а цепочки букв – словами.

Каждое предложение, таким образом, является словом в только что определённом смысле. Придирчивый читатель может спросить, все ли слова являются предложениями, а если нет, то какой процедурой они, предложения, выделяются среди всех слов. Ответим ему так: для наших локальных целей это знать необязательно, и он может спокойно всюду заменить встречающийся ниже термин «предложение» (коль скоро он представляется ему непонятным) на термин «слово». (Как сказал ещё принц Гамлет, «слова, слова, слова».)

Внимательный читатель заметит, что в выписанном алфавите отсутствует буква ≠. Она излишня, потому что вместо а ≠ b можно писать ¬ (a = b).

Слова вида 0, 0′, 0′′, 0′′′, … называют нумералами. Через A(m) будем обозначать то слово, которое получается из слова A подстановкой нумерала m вместо x. Например, если A есть )) 'yx ¬ x'' (, а m есть 0'', то A (m) есть )) 'y0'' ¬ 0''''(. Через A (m, n) будем обозначать то слово, которое получается из слова A одновременной подстановкой нумерала m вместо x и нумерала n вместо y. Сами такие подстановки будем обозначать записями х → m, y → n. Примеры:

если A есть (х'' = х'), а подстановка есть x → m, то A(m) есть (m'' = m');

если A есть (х'' = у'), а подстановки суть x → m, y → n, то A(m, n) есть (m'' = п').

При помощи букв нашего алфавита запишем аксиомы в виде предложений:

I. (х' = у') ⇒ (x = y);

II. ¬ ∃ х (х' = 0).

Далее сформулируем правила вывода. Каждое правило договоримся записывать в виде дроби, где в числителе – то предложение или те предложения, к которым это правило применяется, в знаменателе – результат применения. В скобках после названия правила пишем его условное обозначение. Правил будет четыре:

Покажем, что предложение ¬ (0'''' = 0'') доказуемо. Для этого предъявим список из девяти доказуемых предложений, справа от каждого из них указав в квадратных скобках причину, по которой оно признаётся доказуемым. Если предложение является аксиомой, указываем номер аксиомы; если оно получается из предыдущих предложений списка по одному из правил, указываем номера этих предложений в списке и это правило. Вот этот список:

1) ¬ ∃ x (x′ = 0) [Ax. II];

2) ¬ (0′′ = 0) [1; ¬ ∃: x → 0′].

Временно прервём выписывание списка, чтобы сделать два комментария. Первый комментарий: мы только что установили доказуемость предложения ¬ (0′′ = 0). На содержательном уровне это предложение выражает тот интересный факт, что два не равно нолю. Второй комментарий: уже выписанные две строки позволяют заметить одну важную особенность формального метода, отличающую его от метода неформального. Вспомним, что, излагая неформальный метод, аксиому II мы записали так: Не существует такого x, что х' = 0. Ясно, что смысл аксиомы не изменился бы, выбери мы для неё такую запись: Не существует такого y, что у' = 0. Поэтому доказательство утверждения 0'''' ≠ 0'', предъявленное нами в рамках неформального метода, осталось бы прежним. А вот если бы мы в формальном методе заменили аксиому ¬ ∃ х (х' = 0) на аксиому на ¬ ∃ у (у' = 0), то получить предложение ¬ (0'' = 0) нам бы не удалось, поскольку правило ¬ ∃ разрешает подстановку именно вместо буквы x, а не вместо буквы y. Формальный метод на то и называется формальным, что форма записи имеет здесь первенствующее значение. Продолжим список:

3) (х′ = у′) ⇒ (х = y) [Ax. I];

4) (0′′′ = 0′) ⇒ (0′′ = 0) [3; C: x → 0′′, y → 0];

5) ¬ (0'' = 0) ⇒ ¬ (0''' = 0') [4; ⇒ ¬];

6) (0'''' = 0'') ⇒ (0''' = 0') [3; С: х → 0''', у → 0'];

7) ¬ (0''' = 0') ⇒ ¬ (0'''' = 0'') [6; ⇒ ¬];

8) ¬ (0''' = 0') [5, 2; MP];

9) ¬ (0'''' = 0'') [7, 8; MP].

Остаётся заметить, что последним в списке стоит интересующее нас предложение ¬ (0′′′′ = 0′′).

Если мы теперь запишем все эти 9 предложений друг за другом, разделив их каким-нибудь знаком (для определённости – решёткой #), получим то, что называется формальным доказательством предложения ¬ (0'''' = 0''):

¬ ∃ x (x' = 0) # ¬ (0'' = 0) # (x' = у') ⇒ (х = у) # (0''' = 0') ⇒ (0'' = 0) # ¬ (0'' = 0) ⇒ ¬ (0''' = 0') # (0'''' = 0'') ⇒ (0''' = 0') # ¬ (0''' = 0') ⇒ ¬ (0'''' = 0'') # ¬ (0''' = 0') # ¬ (0'''' = 0'').

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

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

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