Тени разума. В поисках науки о сознании

В большей части предлагаемых рассуждений я не стану проводить четкую границу между непротиворечивостью и ω-непротиворечивостью, однако тот вариант теоремы Гёделя, что представлен в §2.5, по сути, гласит, что если формальная система F непротиворечива, то она не может быть полной, так как не может включать в себя в качестве теоремы утверждение G(F). Здесь я всего этого демонстрировать не буду (интересующиеся же могут обратиться к [223]). Вообще говоря, для того чтобы эту форму гёделевского доказательства можно было свести к доказательству в моей формулировке, система F должна содержать в себе нечто большее, нежели просто «арифметику и обыкновенную логику». Необходимо, чтобы система F была обширной настолько, чтобы включать в себя действия любой машины Тьюринга. Иначе говоря, среди утверждений, корректно формулируемых с помощью символов системы F, должны присутствовать утверждения типа: «Такая-то машина Тьюринга, оперируя над натуральным числом n, дает на выходе натуральное число p». Более того, имеется теорема (см. [223], главы 11 и 13), согласно которой так оно само собой и получается, если, помимо обычных арифметических операций, система F содержит следующую операцию (так называемую μ-операцию, или операцию минимизации): «найти наименьшее натуральное число, обладающее таким-то арифметическим свойством». Вспомним, что в нашем первом вычислительном примере, (A), предложенная процедура действительно позволяла отыскать наименьшее число, не являющееся суммой трех квадратов. То есть, вообще говоря, право на подобные вещи за вычислительными процедурами следует сохранить. С другой стороны, именно благодаря этой их особенности мы и сталкиваемся с вычислениями, которые принципиально не завершаются, — например, вычисление (В), где мы пытаемся отыскать наименьшее число, не являющееся суммой четырех квадратов, а такого числа в природе не существует.

2.9. Формальные системы и алгоритмическое доказательство

 В предложенной мною формулировке доказательства Гёделя—Тьюринга (см. §2.5) говорится только о «вычислениях» и ни словом не упоминается о «формальных системах». Тем не менее, между этими двумя концепциями существует очень тесная связь. Одним из существенных свойств формальной системы является непременная необходимость существования алгоритмической (т.е. «вычислительной») процедуры F, предназначенной для проверки правильности применения правил этой системы. Если, в соответствии с правилами системы F, некое высказывание является ИСТИННЫМ, то вычисление F этот факт установит. (Для достижения этого результата вычисление F, возможно, «просмотрит» все возможные последовательности строк символов, принадлежащих «алфавиту» системы F, и успешно завершится, обнаружив заключительной строкой искомое высказывание P; при этом любые сочетания строк символов являются, согласно правилам системы F, допустимыми.)

Напротив, располагая некоторой заданной вычислительной процедурой E, предназначенной для установления истинности определенных математических утверждений, мы можем построить формальную систему E, которая эффективно выражает как ИСТИННЫЕ все те истины, что можно получить с помощью процедуры E. Имеется, впрочем, и небольшая оговорка: как правило, формальная система должна содержать стандартные логические операции, однако заданная процедура E может оказаться недостаточно обширной, чтобы непосредственно включить и их. Если сама заданная процедура E не содержит этих элементарных логических операций, то при построении системы E уместно будет присоединить их к E с тем, чтобы ИСТИННЫМИ положениями системы E оказались не только утверждения, получаемые непосредственно из процедуры E, но и утверждения, являющиеся элементарными логическими следствиями утверждений, получаемых непосредственно из E. При таком построении система E не будет строго эквивалентна процедуре E, но вместо этого приобретет несколько большую мощность.

(Среди таких логических операций могут, к примеру, оказаться следующие: «если P&Q, то P»; «если P и P ⇒ Q, то Q»; «если ∀x[P(x)], то P(n)»; «если ~ ∀x[P(x)], то ∃x[~ P(x)]» и т.п. Символы «&», «⇒», «∀», «∃», «~» означают здесь, соответственно, «и», «следует», «для всех [натуральных чисел]», «существует [натуральное число]», «не»; в этот ряд можно включить и некоторые другие аналогичные символы.)