Однако следует ли считать высказывание G
(F) неопровержимо истинным всякий раз, когда мы признаем неопровержимо обоснованной формальную систему F? Полагаю, утвердительный ответ на этот вопрос не должен вызывать никаких сомнений; и это тем более так, если придерживаться в отношении воспроизведения математического доказательства той «принципиальной» позиции, которой мы придерживались до сих пор. Единственная возникающая в этой связи реальная проблема касается деталей фактического кодирования утверждения «система F непротиворечива» в форме арифметического утверждения (Π1-высказывания). Сама по себе базовая идея неопровержимо очевидна: если система F является обоснованной, то она, безусловно, непротиворечива. (Так как если бы она не была непротиворечивой, то среди ее утверждений присутствовало бы утверждение «1 = 2», т.е. система была бы необоснованной.) Что касается деталей этого самого кодирования, то здесь нам вновь предстоит иметь дело с различием между «принципиальным» и «практическим» уровнями. Не составит особого труда убедиться в том, что такое кодирование в принципе возможно (хотя сам процесс убеждения может занять некоторое время), однако убедиться в корректном выполнении того или иного конкретного действительного кодирования — дело совсем другое. Детали кодирования, как правило, бывают в известной степени произвольными и в разных изложениях могут весьма значительно отличаться. Возможно, где-то закрадется незначительная ошибка или просто опечатка, которая, в формальном смысле, должна бы сделать недействительным данное конкретное предназначенное для выражения «G(F)» теоретико-числовое предположение, однако в действительности этого не происходит.Надеюсь, читатель понимает, что возможность возникновения таких ошибок не существенна, когда речь заходит о том, что мы подразумеваем здесь под принятием предположения G
(F) в качестве неопровержимой истины. Я, разумеется, говорю о действительном предположении G(F), а не о возможном случайном предположении, непреднамеренно сформулированном благодаря опечатке или незначительной ошибке. В этой связи мне вспоминается одна история о великом американском физике Ричарде Фейнмане. Фейнман, по-видимому, объяснял одному из студентов какое-то понятие, но оговорился. Когда студент выразил недоумение, Фейнман вспылил: «Не слушайте, что я говорю; слушайте, что я имею в виду!»[16].Один из возможных способов такого явного кодирования состоит в использовании представленных еще в НРК спецификаций машин Тьюринга и точном воспроизведении доказательства гёделевского типа, описанного в §2.5
(пример такого кодирования приводится в Приложении А). Впрочем, даже и в этом случае об абсолютной «явности» говорить нельзя, поскольку нам понадобится еще и каким-то явным образом закодировать правила формальной системы F в системе обозначений действий машин Тьюринга; обозначим такой код, скажем, через TF- (Код TF должен удовлетворять определенному свойству: если некоторому высказыванию P, выводимому в рамках системы F, ставится в соответствие некоторое число р, то необходимо, скажем, чтобы равенство TF(p) = 1 выполнялось всякий раз, когда высказывание P является теоремой системы F, в противном же случае вычисление TF(p) не должно завершаться вовсе.) Безусловно, все это открывает широкий простор для формальных ошибок. Помимо возможных трудностей, связанных с практическим построением кода TF на основе системы F и отысканием числа p на основе высказывания P, отсутствует ясность и в отношении другого вопроса: а не ошибся ли я сам где-нибудь в спецификациях машин Тьюринга, — иными словами, можем ли мы быть полностью уверены в корректности приведенного в Приложении А этой книги кода, если вдруг решим использовать для отыскания вычисления Ck(k) именно это определение? Лично я думаю, что ошибок там нет, однако в собственной непогрешимости я уверен куда как меньше, нежели в первоначальных построениях Гёделя (пусть и более сложных). Впрочем, всякому дочитавшему до этого места, смею надеяться, уже ясно, что возможные ошибки подобного рода существенной роли здесь не играют. Помните, что говорил Фейнман?