принципах:

1. Каждое формальное доказательство есть текст, т. е. конечная цепочка знаков, выбранных из некоторого алфавита;

2. Каждый текст, составленный из букв рассматриваемого алфавита, поддается алгоритмической проверке на предмет того, является ли он формальным доказательством или нет, и если да, то какого именно утверждения;

3. Только истинные утверждения могут обладать формальными доказательствами.

В силу третьего принципа предъявление формального доказательства какого-либо утверждения гарантирует его истинность и, следовательно, может считаться его доказательством. Обратное, конечно, не предполагается: не предполагается, что каждое истинное или даже содержательно доказуемое утверждение имеет – при заранее заданном понятии формального доказательства – формальное доказательство. Анализ теоремы Гёделя о неполноте показывает, что утверждение, о котором в ней идёт речь, всегда имеет вид

 – некоторое свойство натурального числа х. Это свойство зависит от рассматриваемого понятия формального доказательства, но всегда алгоритмически проверяемо[162] (подобно тому, как алгоритмически проверяемо свойство четвёрки чисел «быть четвёркой Ферма»). Итак, теорема Гёделя утверждает, что не имеют формального доказательства.

Ужесточим наши требования к представлениям о формальном доказательстве. А именно потребуем, чтобы выполнялось следующее условие: коль скоро для какого-то алгоритмически проверяемого свойства

утверждение оказывается истинным, то это утверждение обладает формальным доказательством. Это требование довольно естественно; оно реализуется при формализации следующих уже встречавшихся выше этапов: 1) предъявления некоторого с; 2) проверки, что это с удовлетворяет свойству здесь существенно и то, что с можно фактически предъявить, и то, что можно фактически проверить.

Наше требование вытекает, в частности, из следующих двух ещё более естественных требований:

1) если для числа с справедливо (алгоритмически) проверяемое свойство

то обладает формальным доказательством;

2) для какого угодно свойства

если для некоторого с утверждение обладает формальным доказательством, то и обладает формальным доказательством.

Теперь, прибегнув к рассуждениям, аналогичным тем, которые применялись в связи с теоремой Ферма, приходим к следующему выводу: если ни утверждение

ни его отрицание не обладают формальным доказательством, то одно это уже позволяет заключить, которое из этих двух утверждений верно, а именно: верно

В самом деле, если бы было верно

то это утверждение обладало бы формальным доказательством; стало быть, неверно, а верно[163].

Давайте ещё раз оценим парадоксальность ситуации: из одного только факта, что ни А, ни не-А не обладают формальным доказательством, можно заключить, которое из этих двух высказываний истинно на самом деле.

6. Что такое доказательство?

Если мы читаем книгу, написанную 50 лет назад, то рассуждения, которые мы в ней находим, кажутся нам большей частью лишёнными логической строгости.

анри пуанкаре. наука и метод. 1908 [2, с. 356]

В предыдущем размышлении встречался как термин «доказательство», так и термин «формальное доказательство». Иногда считают, что формальное доказательство – это такое доказательство, которое формально. Мы предпочитаем смотреть на эти понятия иначе.

Формальное доказательство – это математический объект, подобный, скажем, матрице или треугольнику. Это конечная цепочка знаков некоторого заранее фиксированного алфавита, т. е., как говорят в математике, слово в этом алфавите. Говоря «знак», мы не имеем в виду – в данном случае – какую-либо смысловую, содержательную сторону, но только внешнюю, графическую. Чтобы подчеркнуть это обстоятельство, в математике, когда имеют в виду внешнюю, графическую сторону, говорят не «знак», а «буква». К числу букв относят обычно буквы алфавитов реальных языков (русского, латинского и т. д.), цифры, знаки препинания. Разумно отнести к числу букв и пробел между словами (словами в обычном, не математическом смысле), изобретая для его обозначения какой-либо специальный символ, например #. Это даёт возможность рассматривать текст, т. е. последовательность слов, как слово (в уточнённом выше математическом смысле). Итак, формальное доказательство – это прежде всего слово в некотором алфавите, алфавите формальных доказательств. Разумеется, этим ни в малейшей степени не исчерпывается понятие формального доказательства; мы просто хотели подчеркнуть, что понятие формального доказательства относится к разряду слов, так же как понятие треугольника – к разряду геометрических фигур.

Какие именно слова следует считать формальными доказательствами – это тема особого разговора, выходящего за круг предметов, которые мы хотели бы здесь обсудить. Подчеркнём, что можно дать различные определения понятию формального доказательства, каждое из которых приводит к своему множеству формальных доказательств. Некоторые общие положения, которым должно подчиняться любое разумное определение, были изложены в предыдущем размышлении. Заметим, впрочем, что иногда делают ещё один шаг в сторону общности и не требуют заранее, чтобы формальными доказательствами обладали только истинные утверждения, полностью отделяя понятие формального доказательства от понятия истины. А затем это отброшенное требование вводят в виде дополнительного свойства (которым формальные доказательства, вообще говоря, могут и не обладать), а именно: множество формальных доказательств называют семантически непротиворечивым, если всякое утверждение, обладающее формальным доказательством, истинно. Более точно общие представления о формальных доказательствах излагаются с помощью понятия дедуктики (см., например, [21]).

Подчеркнём ещё, что формальными доказательствами могут обладать (или не обладать) не сами содержательно понимаемые утверждения, а лишь их записи (т. е. опять-таки слова) в каком-либо точно заданном логико-математическом языке.

Определение понятия формального доказательства – быть может, лучше сказать «определение множества формальных доказательств» – в широких пределах (обусловленных указанными выше общими ограничительными свойствами множества формальных доказательств) произвольно. Здесь имеется в виду тот «юридический» произвол, который отличает математические определения вообще. Мы имеем «юридическое» право, например, произвольно определить класс функций и назвать их «как хотим», например непрерывными.

Другое дело, что всякое разумное математическое определение обычно претендует на то, чтобы соответствовать некоторым интуитивным представлениям, отражать их. Законность определения ещё не означает его разумности. Так, математическое понятие непрерывной кривой отражает (с той или иной точностью) наши интуитивные, содержательные представления о траектории движущейся точки. Аналогично понятие формального доказательства отражает интуитивные представления о содержательном доказательстве.

Можно сказать, что понятие формального доказательства является математической моделью понятия доказательства – в том же смысле, в каком понятие непрерывной кривой является