В силу третьего принципа предъявление формального доказательства какого-либо утверждения гарантирует его истинность и, следовательно, может считаться его доказательством. Обратное, конечно, не предполагается: не предполагается, что каждое истинное или даже содержательно доказуемое утверждение имеет – при заранее заданном понятии формального доказательства – формальное доказательство. Анализ теоремы Гёделя о неполноте показывает, что утверждение, о котором в ней идёт речь, всегда имеет вид – некоторое свойство натурального числа х.
Это свойство зависит от рассматриваемого понятия формального доказательства, но всегда алгоритмически проверяемо[162] (подобно тому, как алгоритмически проверяемо свойство четвёрки чисел «быть четвёркой Ферма»). Итак, теорема Гёделя утверждает, что не имеют формального доказательства.Ужесточим наши требования к представлениям о формальном доказательстве. А именно потребуем, чтобы выполнялось следующее условие: коль скоро для какого-то алгоритмически проверяемого свойства утверждение оказывается истинным, то это утверждение обладает формальным доказательством. Это требование довольно естественно; оно реализуется при формализации следующих уже встречавшихся выше этапов: 1) предъявления некоторого с
; 2) проверки, что это с удовлетворяет свойству здесь существенно и то, что с можно фактически предъявить, и то, что можно фактически проверить.Наше требование вытекает, в частности, из следующих двух ещё более естественных требований:
1) если для числа с
справедливо (алгоритмически) проверяемое свойство то обладает формальным доказательством;2) для какого угодно свойства если для некоторого с
утверждение обладает формальным доказательством, то и обладает формальным доказательством.Теперь, прибегнув к рассуждениям, аналогичным тем, которые применялись в связи с теоремой Ферма, приходим к следующему выводу: если ни утверждение ни его отрицание не обладают формальным доказательством, то одно это уже позволяет заключить, которое из этих двух утверждений верно, а именно: верно
В самом деле, если бы было верно то это утверждение обладало бы формальным доказательством; стало быть, неверно, а верно[163]
.Давайте ещё раз оценим парадоксальность ситуации: из одного только факта, что ни А, ни не-А не обладают формальным доказательством, можно заключить, которое из этих двух высказываний истинно на самом деле.
6. Что такое доказательство?
Если мы читаем книгу, написанную 50 лет назад, то рассуждения, которые мы в ней находим, кажутся нам большей частью лишёнными логической строгости.
анри пуанкаре. наука и метод. 1908 [2, с. 356]В предыдущем размышлении встречался как термин «доказательство», так и термин «формальное доказательство». Иногда считают, что формальное доказательство – это такое доказательство, которое формально. Мы предпочитаем смотреть на эти понятия иначе.
Формальное доказательство
– это математический объект, подобный, скажем, матрице или треугольнику. Это конечная цепочка знаков некоторого заранее фиксированного алфавита, т. е., как говорят в математике, слово в этом алфавите. Говоря «знак», мы не имеем в виду – в данном случае – какую-либо смысловую, содержательную сторону, но только внешнюю, графическую. Чтобы подчеркнуть это обстоятельство, в математике, когда имеют в виду внешнюю, графическую сторону, говорят не «знак», а «буква». К числу букв относят обычно буквы алфавитов реальных языков (русского, латинского и т. д.), цифры, знаки препинания. Разумно отнести к числу букв и пробел между словами (словами в обычном, не математическом смысле), изобретая для его обозначения какой-либо специальный символ, например #. Это даёт возможность рассматривать текст, т. е. последовательность слов, как слово (в уточнённом выше математическом смысле). Итак, формальное доказательство – это прежде всего слово в некотором алфавите, алфавите формальных доказательств. Разумеется, этим ни в малейшей степени не исчерпывается понятие формального доказательства; мы просто хотели подчеркнуть, что понятие формального доказательства относится к разряду слов, так же как понятие треугольника – к разряду геометрических фигур.