Апология математики (сборник статей)

Ещё один пример. Дано множество 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.