10.5. Прямое доказательство теорем Тарского и Гёделя

В нашем изложении теоремы Тарского и Гёделя по­лучились как простые следствия определений и фактов, связанных с теорией алгоритмов. С одной стороны, это позволяет лучше понять место этих теорем в общем кон­тексте математической логики и теории алгоритмов. С другой стороны, возникает естественное желание раз­вернуть цепочку и получить более прямые доказатель­ства. Таковые мы сейчас и приведём.

Начиная доказывать теорему Тарского, предполо­жим, что множество номеров всех истинных арифмети­ческих формул (без параметров) арифметично. Пусть Т — это множество, а т(х) — соответствующая форму­ла. Перенумеруем также все формулы с одним параме­тром х; пусть Гп(х) — формула, имеющая номер п в этой нумерации. Рассмотрим формулу с единственным пара­метром х, утверждающую, что результат подстановки константы х в х-ую формулу с параметром ложен. Эту формулу можно написать так:

Зг(-1г(г) Л ЗиЬй^г, х, х))где 8иЪаЬ(р,д,г) — формула с тремя параметрами, вы­ражающая такое свойство: «р есть номер (в нумерации всех формул без параметров) той формулы, которая по­лучится, если в д-ю формулу с одним параметром подста­вить константу г вместо этого параметра». Записанное в кавычках свойство описывает график некоторой вы­числимой функции (соответствующей простым синтак­сическим действиям и переходу от одной нумерации к другой) и потому существует выражающая его формула.

Итак, мы написали некоторую формулу с единствен­ным параметром х. Пусть она имеет некоторый номер N. Подставим этот номер N вместо сё параметра. Полу­чится некоторая формула без параметров. Из построе­ния видно, что эта формула истинна тогда и только то­гда, когда результат подстановки числа N в формулу номер N (то есть сама эта формула!) ложен.

Полученное противоречие завершает прямое доказа­тельство теоремы Тарского. Мы видим, что нам потре­бовалась выразимость в арифметике не любых вычисли­мых функций, а одной вполне конкретной. При доста­точном терпении соответствующую формулу можно-та-ки написать, и тем самым доказательство станет совсем «осязаемым».

Теперь изложим в том же стиле доказательство тео­ремы Гёдсля. Как мы уже говорили, исчисление — это механизм (алгоритм), который позволяет порождать не­которые формулы языка арифметики (для простоты бу­дем считать, что порождаются только формулы без па­раметров). Таким образом, возникает некоторое персчи-слимос множество, которое обычно задают как проек­цию разрешимого множества. Именно, вводят некоторое понятие доказательства. При этом доказательства явля­ются словами в некотором алфавите. Множество доказа­тельств разрешимо, то есть есть алгоритм, отличающий настоящие доказательства от текстов, который таковы­ми не являются. Кроме того, есть (также разрешимое) свойство двух слов х ж у, которое гласит, что х есть доказательство формулы у. Перенумеровав все доказа­тельства и формулы и выразив указанные разрешимыесвойства в языке арифметики, мы приходим к формуле Proof (х, у), которая истинна, когда х есть номер доказа­тельства формулы с номером у.

Теперь напишем формулу с одним параметром х, ко­торая говорит, что результат подстановки числа х вме­сто параметра в х-ую формулу с одним параметром не имеет доказательства:

-i3z3p[Subst(z, х, х) Л Proof (р, г)]

Эта формула имеет единственный параметр (х); пусть сё номер в нумерации таких формул равен N. Подста­вим N вместо параметра. Получится формула без пара­метров р. По построению формула р истинна, когда ре­зультат подстановки N в N-ю формулу с одним параме­тром недоказуем. А этот результат есть сама формула р, так что она истинна тогда и только тогда, когда недока­зуема. Значит, наше исчисление либо позволяет доказать ложную формулу р (если р ложна; в таком случае его на­зывают неадекватным), либо не позволяет доказать ис­тинную формулу р.

Заметим, что оба этих доказательства напоминают как построение неподвижной точки, так и классический парадокс лжеца:

УТВЕРЖДЕНИЕ В РАМКЕ ЛОЖНО