Вот доказательство. Итак, пусть 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'', содержательный вывод которого из аксиом-утверждений был приведён выше.
Прежде всего надо построить тот язык, в виде предложений которого будут записываться как аксиомы, так и все другие задействованные утверждения. Построение языка начинается с предъявления алфавита, т. е. списка символов, которые мы собираемся использовать. Для наших целей удобен такой алфавит:
() ⇒ ¬ ∃ = xy 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. Формальный метод на то и называется формальным, что форма записи имеет здесь первенствующее значение. Продолжим список:
