2.8. Условие -непротиворечивости 153

если система F является обоснованной, то она непременно будет и ^-непротиворечивой.

В дальнейшем утверждения "формальная система F является непротиворечивой" и "формальная система F является -непротиворечивой" я буду обозначать, соответственно, символами . В сущности (если полагать систему F достаточно обширной), сами утверждения G (F) и (F) формулируются как операции этой системы. Согласно знаменитой теореме Гёделя о неполноте, утверждение G (F) не является теоремой системы F (т. е. его нельзя доказать с помощью процедур, допустимых в рамках системы F); не является теоремой и утверждение - если, разумеется, система F действительно непротиворечива. Несколько более строгий вариант теоремы Гёделя, сформулированный позднее Россером, гласит, что если система F непротиворечива, то утверждение ~ G (F) также не является теоремой этой системы. В оставшейся части этой главы я буду формулировать свои доводы не столько исходя из утверждения сколько на основе более привычного нам G (F), хотя для большей части наших рассуждений в равной степени сгодится любое из них. (В некоторых наиболее явных аргументах главы 3 я буду иногда обозначать через "G(F)>> конкретное утверждение "вычисление Ck (k) не завершается" (см. §2.5); надеюсь, никто не сочтет это слишком большой вольностью с моей стороны.)

В большей части предлагаемых рассуждений я не стану проводить четкую границу между непротиворечивостью и непротиворечивостью, однако тот вариант теоремы Гёделя, что представлен в § 2.5, по сути, гласит, что если формальная система F непротиворечива, то она не может быть полной, так как не может включать в себя в качестве теоремы утверждение G (F). Здесь я всего этого демонстрировать не буду (интересующиеся же могут обратиться к . Вообще говоря, для того чтобы эту форму гёделевского доказательства можно было свести к доказательству в моей формулировке, система F должна содержать в себе нечто большее, нежели просто "арифметику и обыкновенную логику". Необходимо, чтобы система F была обширной настолько, чтобы включать в себя действия любой машины Тьюринга. Иначе говоря, среди утверждений, корректно формулируемых с помощью символов системы F, должны присутствовать утверждения типа: "Такая-то машина Тьюринга, оперируя над натуральным числом , дает на выходе натуральное число

154 Глава 2

Более того, имеется теорема (см. [223], главы 11 и 13), согласно которой так оно само собой и получается, если, помимо обычных арифметических операций, система F содержит следующую операцию (так называемую -операцию, или операцию минимизации): "найти наименьшее натуральное число, обладающее таким-то арифметическим свойством". Вспомним, что в нашем первом вычислительном примере, (А), предложенная процедура действительно позволяла отыскать наименьшее число, не являющееся суммой трех квадратов. То есть, вообще говоря, право на подобные вещи за вычислительными процедурами следует сохранить. С другой стороны, именно благодаря этой их особенности мы и сталкиваемся с вычислениями, которые принципиально не завершаются, - например, вычисление (В), где мы пытаемся отыскать наименьшее число, не являющееся суммой четырех квадратов, а такого числа в природе не существует.