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

¬ ∃ 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. Теорема Гёделя

Словосочетание «теорема Гёделя» довольно популярно, и не только в математической среде. И это совершенно заслуженно. Ведь теорема Гёделя (точнее, теорема Гёделя о неполноте) не только одна из самых замечательных и неожиданных теорем математической логики, да и всей математики, но и, пожалуй, единственная на сегодняшний день теорема теории познания.

Говоря совсем грубо, теорема Гёделя утверждает, что не всё можно доказать, говоря чуть более точно – что существуют истинные утверждения, которые нельзя доказать, а подробнее – что такие утверждения найдутся даже среди утверждений о натуральных числах. Но эта формулировка заключает в себе некое противоречие. В самом деле, если мы обнаружили истинное утверждение, которое невозможно доказать, то откуда, спрашивается, мы знаем, что оно истинное? Ведь, чтобы убеждённо заявлять о его истинности, мы должны эту истинность доказать. Но тогда как же можно говорить о его недоказуемости?

Разгадка в том, что в грубых, подобно приведённым, формулировках теоремы Гёделя смешиваются два понятия доказательства – содержательное (неформальное, психологическое) и формальное. Теорему Гёделя надлежит понимать в следующем смысле: существуют не имеющие формального доказательства утверждения, являющиеся тем не менее истинными, причём истинность их подтверждается содержательными доказательствами. Иными словами, эти утверждения доказуемы содержательно и недоказуемы формально. Отметим, что в применении к какому бы то ни было утверждению более корректно было бы говорить о формальных доказательствах не самого этого утверждения, а предложения, служащего записью этого утверждения в виде слова, составленного из букв подходящего алфавита. Однако мы этого делать не будем, чтобы не утяжелять изложения.