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