logo
Пенроуз Р

2.10. Возможные формальные возражения против 185

мыслительную деятельность исключительно в рамках системы F, то ее символы не должны изменять свой смысл "на полпути". Если же мы принимаем, что мыслительная деятельность может содержать что-то помимо операций самой системы F - т. е. изменение смысла символов, - то нам необходимо знать и правила, управляющие подробным изменением. Либо эти правила окажутся неалгоритмическими, и это сыграет в пользу , либо для них найдется какая-то конкретная алгоритмическая процедура, и тогда нам следовало бы изначально включить эту процедуру в нашу "систему F" - обозначим ее через - с тем, чтобы она представляла собой полную совокупность процедур, обусловливающих наши с вами понимание и проницательность, а значит, необходимости в изменении смысла символов не возникло бы вовсе. В последнем случае вместо гёделевского высказывания G (F) из предыдущего рассуждения нам предстоит разбираться уже с высказыванием G (F*), так что ничего мы в результате не выигрываем.

Q18. Даже в такой простой системе, как арифметика Пеано, можно сформулировать теорему, интерпретация которой имеет следующий смысл:

"система F обоснованна", а следовательно, "высказывание G (F) истинно".

Разве это не все, что нам нужно от теоремы Гёделя? Значит, теперь, полагая обоснованной какую угодно формальную систему F, мы вполне можем поверить и в истинность ее гёделевского высказывания - при условии, разумеется, что мы готовы принять арифметику Пеано, разве не так?

Подобную теорему действительно можно сформулировать в рамках арифметики Пеано. Точнее (поскольку мы не можем в пределах какой бы то ни было формальной системы должным образом выразить понятие "обоснованности" или "истинности", как это следует из знаменитой теоремы Тарского), мы, в сущности, формулируем более сильный результат:

"система F непротиворечива", а следовательно,

"высказывание G (F) истинно", либо иначе:

"система -непротиворечива", а следовательно, "высказывание истинно".

186 Глава 2

Из этих высказываний следует вывод, необходимый для Q18, поскольку если система F обоснованна, то она, разумеется, непротиворечива или омега-непротиворечива, в зависимости от обстоятельств. Понимая смысл присутствующего здесь символизма, мы и в самом деле можем поверить в истинность высказывания G (F) на основании одной лишь веры в обоснованность системы F. Это, впрочем, мы уже приняли. Если понимать смысл, то действительно возможно перейти от F к G (F). Сложности возникнут лишь в том случае, если нам вздумается исключить необходимость интерпретаций и сделать переход от F к G (F) автоматическим. Будь это возможно, мы смогли бы автоматизировать общую процедуру "гёделизации" и создать алгоритмическое устройство, которое действительно будет содержать в себе все, что нам нужно от теоремы Гёделя. Однако такой возможности у нас нет - захоти мы добавить эту предполагаемую алгоритмическую процедуру в какую угодно формальную систему F, выбранную нами в качестве отправной, в результате просто-напросто получилась бы, по сути, некоторая новая формальная система , а ее гёделевское высказывание оказалось бы уже за ее рамками. Таким образом, согласно теореме Гёделя, какой-то аспект понимания всегда остается "за нами", независимо от того, какая доля его оказалась включена в формализованную или алгоритмическую процедуру. Это "гёделево понимание" требует постоянного соотнесения с действительным смыслом символов какой бы то ни было формальной системы, к которой применяется процедура Гёделя. В этом смысле ошибка Q18 весьма похожа на ту, что мы обнаружили, комментируя возражение Q17. С невозможностью автоматизации процедуры гёделизации тесно связаны также рассуждения по поводу Q6 и Q19.

В возражении Q18 присутствует еще один аспект, который стоит рассмотреть. Представим себе, что у нас есть обоснованная формальная система И, содержащая арифметику Пеано. Теорема, о которой говорилось в Q18, окажется среди следствий системы И, а частным ее примером, применимым к конкретной системе F (т. е., собственно, ), будет теорема системы . Таким образом, можно сформулировать один из выводов формальной системы :

"система И обоснованна", а следовательно, "высказывание G (И) истинно";