Апология математики (сборник статей) - Владимир Андреевич Успенский
Шрифт:
Интервал:
Закладка:
если 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'').
На этом примере состоялось знакомство с важнейшим понятием формального доказательства. Неформальные доказательства (которые называют ещё содержательными или психологическими) представляют собою убедительные рассуждения, т. е. прежде всего тексты, состоящие из утверждений (не любые такие тексты, разумеется). Формальное же доказательство есть цепочка предложений, особым образом организованная. Читатель может возразить, что в начальном разделе статьи сообщалось, что формальное доказательство есть цепочка символов. Тут нет противоречия: ведь каждое предложение есть цепочка символов, и если составить их вместе, разделив каким-либо разделительным знаком, то снова возникнет не что иное, как цепочка символов, как это и видно из нашего примера. Таким образом, формальное доказательство есть слово, которое составлено из букв дополненного разделительным знаком алфавита.
Общее определение формального доказательства очевидно. Формальное доказательство есть такая цепочка предложений, каждое предложение которой либо является аксиомой, либо получено из каких-то предшествующих предложений цепочки применением одного из правил вывода.
Возьмём любое формальное доказательство, а в нём – какое-либо его подслово (т. е. часть слова, образованную подряд идущими буквами слова), не содержащее знака решётки и представляющее собой такую часть слова, которая ограничена решётками слева и справа, либо же начало слова, ограниченное решёткой справа, либо же конец слова, ограниченный решёткой слева, либо всё слово. Всякое такое подслово является доказуемым предложением. Если это предложение представляет собою конец формального доказательства, то это формальное доказательство называется формальным доказательством данного предложения. Ясно, что предложение тогда, и только тогда, является доказуемым, когда оно имеет формальное доказательство.
§ 13. Теорема Гёделя
Словосочетание «теорема Гёделя» довольно популярно, и не только в математической среде. И это совершенно заслуженно. Ведь теорема Гёделя (точнее, теорема Гёделя о неполноте) не только одна из самых замечательных и неожиданных теорем математической логики, да и всей математики, но и, пожалуй, единственная на сегодняшний день теорема теории познания.
Говоря совсем грубо, теорема Гёделя утверждает, что не всё можно доказать, говоря чуть более точно – что существуют истинные утверждения, которые нельзя доказать, а подробнее – что такие утверждения найдутся даже среди утверждений о натуральных числах. Но эта формулировка заключает в себе некое противоречие. В самом деле, если мы обнаружили истинное утверждение, которое невозможно доказать, то откуда, спрашивается, мы знаем, что оно истинное? Ведь, чтобы убеждённо заявлять о его истинности, мы должны эту истинность доказать. Но тогда как же можно говорить о его недоказуемости?
Разгадка в том, что в грубых, подобно приведённым, формулировках теоремы Гёделя смешиваются два понятия доказательства – содержательное (неформальное, психологическое) и формальное. Теорему Гёделя надлежит понимать в следующем смысле: существуют не имеющие формального доказательства утверждения, являющиеся тем не менее истинными, причём истинность их подтверждается содержательными доказательствами. Иными
