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

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

Проиллюстрируем сказанное на примере того, как в формальном методе доказывается утверждение 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. Формальный метод на то и называется формальным, что форма записи имеет здесь первенствующее значение. Продолжим список:

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''):