<< Пред. стр.

стр. 3
(общее количество: 5)

ОГЛАВЛЕНИЕ

След. стр. >>


• не существует алгоритма, определяющего по тексту программы, будет ли эта
программа вычислять некоторую конкретную вычислимую функцию.

Из теоремы Райса (и следствий из нее) очевидна неразрешимость многих задач,
связанных с программированием. Например, если имеется некоторая программа, то по
ней, вообще говоря, ничего нельзя сказать о функции, реализуемой программой. По
двум программам нельзя установить, реализуют ли они одну и ту же функцию, а это
приводит к неразрешимости многих задач, связанных с эквивалентными преобразова-
ниями и минимизацией программ. В любом алгоритмическом языке, какие бы прави-
ла синтаксиса там ни применялись, всегда будут иметься "бессмысленные"программы,
задающие функции не определенные ни в одной из точек (“эти программы нельзя об-
наружить, потому что они никогда не работают, не являясь при этом ошибочными”).
Теорема Райса доказывает алгоритмическую неразрешимость многих задач, связанных
с вычислениями на компьютерах.


4 Разрешимость и перечислимость множества тавто-
логий
Мы уже упоминали о том, что эффективные вычисления реализуются как вычисли-
тельными машинами, так и человеком. Только что мы установили некоторые факты о
языках программирования, теперь мы попробуем применить их к языкам логики.
Возьмем язык логики первого порядка L? с сигнатурой ?, множество формул ? ? L?
и конкретную формулу P ? L? . Требуется проверить, является ли формула P семан-
тическим следствием из ?. Очевидно, что мы не можем напрямую проверить принад-
лежность формулы P всем возможным моделям множества ?. Следовательно, нужно
попробовать синтаксически вывести эту формулу, то есть, доказать ее истинность, и
(по теореме о корректности) получить также и семантическую справедливость.
Здесь возникает ряд вопросов: можно ли построить такое доказательство? Можно
ли написать алгоритм, который будет последовательно выдавать следствия из (пусть
конечного) множества ?, то есть, являются ли следствия из него перечислимым мно-
жеством? Существует ли алгоритм, определяющий, является ли P следствием из ?, то
есть, разрешимо ли это множество? (При отсутствии данного алгоритма процесс доказа-
тельства некой формулы является “шаманством”.) Можно также решать более простую
21


задачу, то есть определять является ли формула тавтологией (проверять свойства |= P
или N D P.
Можно рассматривать “самый богатый” язык (далее мы поймем, какие требования
не принципиальны). “Самый богатый” язык содержит счетное число констант, функци-
ональных и предикатных симмволов, а также символ равенства. Назовем его L?? . В
качестве ? рассмотрим пустое множество формул и будем работать с множеством тав-
тологий P ? L? , справедливых в любой модели. Является ли хотя бы оно разрешимым
или по крайней мере перечислимым?

Теорема 4.1 Множество тавтологий “достаточно богатого” языка логики первого
порядка L?? не является разрешимым.

Замечание 4.1 Уточним утверждение теоремы. Множество тавтологий языка ло-
гики первого порядка является разрешимым только для весьма бедных языков, не силь-
но отличающихся от логики высказываний (для которых допускается наличие толь-
ко унарных предикатных символов). Для логики высказываний проверка истинности
осуществляется путем построения таблицы истинности.

Для дальнейших рассуждений нам существенно понадобится теория регистровых
машин. Мы попытаемся “связать” регистровые машины и логические формулы между
собой.

Определение 4.1 Вектор из чисел (L, m0 , m1 , . . . , mn ) является конфигурацией реги-
стровой машины, исполняющей программу P , после l шагов, если

• программа оканчивается меткой k и L ? k;

• начавшись с пустого слова, после l шагов имеет в регистре Ri число элементов,
равное mi для всех допустимых значений i;

• следующая инструкция имеет метку L.

С учетом этого определения условие конечности программы P с меткой k у команды
halt можно переформулировать: найдутся такие числа L, m0 , m1 , . . . , mn , что после l
шагов регистровая машина будет иметь конфигурацию (k, m0 , m1 , . . . , mn ).
Доказательство: Опишем на языке логики первого порядка работу регистровой ма-
шины (именно для этой цели и была выбрана такая большая мощность языка).
Определим круг рассматриваемых программ. Их алфавит состоит из элемента |, сло-
ва интерпретируются как числа (по количеству элементов в слове). Требуется построить
по программе формулу ?P , которая является тавтологией, если и только если данная
программа корректно работает с пустым начальным словом (|= ?P , IFF ?P ? ?halt ).
Пусть в регистровой машине, в которой работает эта программа, задействован n + 1
регистр R0 , R1 , R2 , . . . , Rn .
22 Разрешимость и перечислимость множества тавтологий


Для построения формулы ?P следует выбрать необходимые предикатные символы.
Пусть программа рано или поздно остановится (P : > halt), причем sP количество
шагов до остановки (для бесконечных программ будем считать sP = ?). Из ?? вы-
берем: символ унарной функции s, бинарный предикатный символ ’<’, (n + 3)-арный
символ предиката R, символ константы ’0’ и предикат равенства ’=’.
Построим специальную интерпретацию для удобной работы с формулами такого
вида.
Случай 1. P некорректно работает с пустым начальным словом, P : > ?. В
качестве универсума возьмем множество AP := N ? {0}, символ ’ < ’ будет соответ-
ствовать обычному отношению порядка на N, 0AP := 0, ’ = ’ интерпретируется как
равенство, sAP (x) := x + 1, RAP (l, L, m0 , m1 , . . . , mn ) (где все аргументы числа)
характеристическая функция некоторого отношения:
?
? 1, если после l шагов регистровая машина
имеет конфигурацию (L, mo , . . . , mr ) ;
?
0, в противном случае .

Случай 2. P корректно работает с пустым начальным словом, P : > halt.
Универсумом будет являться некоторый конечный отрезок ряда целых чисел AP :=
{0, 1, 2, . . . , e}, где e := max (k, sP ) максимум от длины программы и количества шагов
до останова. Функцию последователя определим следующим образом:

x + 1, x = e,
sAP (x) :=
e, x = e;
остальные символы аналогично первому случаю.
Обозначим 1 := s (0), n := s (n ? 1). Подчеркивание означает принадлежность дан-
ных символов к термам языка, а не числам.
Построим формулу ?P , которая описывает работу программы P , соблюдая при
этом два свойства: AP |= ?P (она истинна в интерпретации AP ) и если ?P верно в
некоторой другой модели A и (L, m0 , . . . , mn ) конфигурация регистровой машины по-
сле l шагов, то элементы 0A , 1A , . . . , lA попарно различны и в A истинна формула
R l, L, m0 , . . . , mn . Данные свойства проверяются в процессе построения формулы ?P
(первое подстановкой, второе индукцией по l). ? ?

Запишем формулу для ?P следующим образом: ?P := ?0 ? R ?0, 0, . . . , 0? ? ??0 ?
n+3
??1 ? . . . ? ??k?1 , где ?0 некоторая формула, диктующая правила обработки символов
’<’, s () и т. д. в данной модели (

?p = ??0 ? ??1 ? . . . ? ??k?1 ? ?x?y?z(x < y ? y < z > x < z)?

R(0, 0, . . . , 0) ? ?x(0 < x ? 0 = x) ? ?x(x < S(x) ? x = S(x))?
?x(?y(x < y) > (x < S(x) ? ?z(x < z > (S(x) < z ? S(x) = z)))
23


или, говоря неформальным языком

?0 := < порядок ? ?x (0 < x ? 0 = x) ? ?x x ? s (x) ?
s (x) единственный следующий за x, если x не последний

);
R (0, 0, . . . , 0) состояние машины перед выполнением программы; формулы ??i от-
вечают состоянию, в которое переходит машина при выполнении соответствующей ин-
струкции ?i .
Определим ??i в зависимости от типа инструкции ?i .

1. ?i . LET Rj = Rj + |;

??i := ?x?y0 . . . ?yn
(R (x, L, y0 , . . . , yn ) >
(x < s (x) ? R (s (x) , L + 1, y0 , . . . , yj?1 , yj + 1, yj+1 , . . . , yn )))

2. ?i . LET Rj = Rj ? |;

??i := ?x?y0 . . . ?yn
((R(x, L, y0 , . . . , yn ) > (x < s(x)?
(¬yj = 0 ? R(s(x), L + 1, y0 , . . . , yj?1 , yj ? 1, yj+1 , . . . , yn )?
(yj = 0 ? R(s(x), L + 1, y0 , . . . , yj?1 , 0, yj+1 , . . . , yn ))))

3. ?i . PRINT;

??i := ?x?y0 . . . ?yn
(R (x, L, y0 , . . . , yn ) >
(x < s (x) ? R (s (x) , L + 1, y0 , . . . , yn )))

4. ?i . IF Rj = THEN L ELSE L0

??i := ?x?y0 . . . ?yn
((R(x, L, y0 , . . . , yn ) >
(x < s(x) ? (yj = 0 ? R(s(x), L0 , y0 , . . . , yj?1 , 0, yj+1 , . . . , yn )?
(¬yj = 0 ? R(s(x), L0 , y0 , . . . , yn ))))

Теперь построим формулу ?P , являющуюся тавтологией в случае, если P корректно
работает с пустым начальным словом:

?P := ?P > ?x?y0 ?y1 . . . ?yn (R (x, k, y0 , y1 , . . . , yn ))

Докажем, что, действительно, |= ?P - P ? ?halt .
24 Разрешимость и перечислимость множества тавтологий


• ’ > ’. ?P тавтология (|= ?P ), следовательно, она истинна в любой интерпретации,
в том числе и в нашей, где истинна ?P . Из одновременной истинности ?P и ?P
получаем, что истинна и ?x?y0 ?y1 . . . ?yn (R (x, k, y0 , y1 , . . . , yn )), то есть, програм-
ма P остановится после k шагов и таким образом корректно работает с пустым
начальным словом.
• ’ < ’. |= ?P > A |= ?P (по определению, из лжи выводится что угодно, например,
истина). И, тогда A |= ?P > A |= R l, L, m0 , m1 , . . . , mn > A |= ?P
Мы правильно описали работу любой регистровой машины и построили формулу,
которая является тавтологией, если и только если регистровая машина, работу кото-
рой описывает эта формула, корректно работает с пустым словом. Пусть множество
тавтологий разрешимо, следовательно, существует разрешающий алгоритм, который
при этом после некоторого преобразования решает проблему останова (например, алго-
ритм, который получает на вход число Геделя, строит по нему формулу, описывающую
работу машины и проверяет ее принадлежность к множеству тавтологий, после чего
дает ответ о принадлежности программы множеству ?halt ). Но, в соответствии с ранее
доказанным, существование такого алгоритма невозможно, следовательно, множество
тавтологий неразрешимо.
Упражнение 4.1 Множество тавтологий языка логики первого порядка перечисли-
мо.
Указание: Мы уже умеем отождествлять тавтологии с программами, корректно
работающими с пустым словом. Перечеслимость же множества таких программ
уже обсуждалась.
Замечание 4.2 Если на языке можно записать аналог арифметики Пеано, для него
справедливы все вышеприведенные выкладки для языка с бесконечной сигнатурой.
Теорема 4.2 Множество тавтологий языка логики второго порядка неперечислимо.
Этот факт гораздо более сильный чем то, что нельзя построить одновременно кор-
ректную и полную формальную систему. Этот результат очевиден и из нашего резуль-
тата (а именно,если бы существовала корректная и полная формальная система, то
доказательство перечислимости множества тавтологий языков логики первого порядка
переносилось бы и на языки логики второго порядка). Более того, верно не только наше
утверждение о том, что нельзя построить корректную и полную формальную систему,
но нельзя построить формальную систему корректную и полную лишь в слабом смысле
(напомним, что ситема является корректной и полной в слабом смысле, если P тогда
и только тогда, когда |=? P, где P ? L? ).
Мы показали, что для достаточно богатых языков никакие семантические вопросы
о формулах их не допускают эффективного решения (нет алгоритма, который давал бы
ответ на эти вопросы). Это верно даже для языков логики первого порядка, не говоря
уже о языках логики второго порядка. Тем не менее если язык оказывается достоточно
беден, то для него можно проверить некоторые семантические факты.
25


5 Формальные теории
Мы уже говорили, что если на языке можно записать анаалог арифметики Пеано, то
для него справедливо всё, что утверждалось о достаточно богатых языках. Теперь мы
зададимся более интересным вопросом – вопросом создания системы аксиом некоторой
теории. Кроме того мы можем, например интересоваться вопросом, можно ли пере-
числить все формулы данной теории (что автоматически означает, что формулы этой
теории доказываются автоматически – путем их перечисления). Также любопытно, а
можно ли по данной формуле сказать, истинна ли она в данной теории.
Данные вопросы отнюдь не являются праздными. К началу XX в. в теории множеств
были обнаружены парадоксы – самые настоящие противоречия. К этому времени тео-
рия множеств уже успела показать себя как естественная основа и плодотворнейшее
орудие математики. Для спасения ее немецкий математик Дэвид Гильберт предложил
в 1904 г. свою программу перестройки оснований математики, которая состояла из двух
частей:

• Представить существующую математику (включая очищенный от парадоксов ва-
риант теории множеств) в виде формальной теории.

• Доказать непротиворечивость полученной теории (т.е. доказать, что в этой теории
никакое утверждение не может быть доказано вместе со своим отрицанием).

Для дальнейшего обсуждения данной программы нам понадобится определение тео-
рии.

Определение 5.1 Множество T ? L? называется теорией, если оно выполнимо и
замкнуто относительно семантического следствия (то есть если T |= P, то P ? T ).

Пример 5.1 В качестве примера формальной теории можно рассматривать игру в
шахматы - назовем это теорией C. Утверждениями в C будем считать позиции
(всевозможные расположения фигур на доске вместе с указанием “ход белых” или
“ход черных”, а также дополнительной информацией о том, делали ли стороны ходы
королем и каждой из ладей). Тогда аксиомой теории C естественно считать началь-
ную позицию, а правилами вывода - правила игры, которые определяют, какие ходы
допустимы в каждой позиции. Правила позволяют получать из одних утверждений
другие. В частности, отправляясь от нашей единственной аксиомы, мы можем по-
лучать теоремы С. Общая характеристика теорем С состоит, очевидно, в том, что
это - всевозможные позиции, которые могут получиться, если передвигать фигуры,
соблюдая правила.
Если нам предложена теорема А в теории С, вместе с ее доказательством, то
мы можем проверить истинность его (просто проверив, все ли переходы сооствет-
ствуют правилам)
Более того, множество всех теорем теории С оказывается конечным. Значит,
принципиально, можно проверить является ли данная теорема доказуемой в С (то
26 Формальные теории


есть достижима ли данная позиция). Можно также построить цепочку доказатель-
ства любой теоремы (последовательность позициций, приводящую к позиции А), по-
скольку количество всех цепочек также конечно.
Напомним, что мы говорим лишь о принципиальной разрешимости данных задач,
не касаясь проблемы трудоемкости их решения.

Отвлекаясь от нашего, не вполне серьезного, примера, заметим, что существует два
способа построения теорий:
1. Если M – алгебраическая система, то T h(M) := {P ? L? : M |= P}.

2. Задание теории при помощи системы аксиом. Пусть ? ? L? . Тогда ? |= T , где T –
теория.
В первом случае мы имеем некую интерпретацию, универсум и рассматриваем тео-
рию, как все предложения заранее выбранного языка L? , верные в этом универсуме,
то есть все теоремы, верные для данной интерпретации. Возникает вопрос, можно ли
каким-то образом конструктивно сгенерировать все такие теоремы. Поэтому обычно
идут другим путем. Существует такой хороший механизм, а именно одновременно кор-
ректная и полная формальная система. Их на самом деле много, но мы рассмотрели
одну – это естественная дедукция. Далее создают некую систему аксиом ?, обычно не
произвольную, а конечную систему аксиом или “обозримую” систему аксиом. Иными
словами систему аксиом, состоящую из отдельных аксиом и нескольких схем аксиом.
Система аксиом получается бесконечной, но обозримой в том смысле, что она реги-
строво разрешима (есть такой алгоритм, который для любой формулы может сказать,
является ли она аксиомой или не является). Разрешимость здесь как бы исключает про-
извольность этого множества, оно должно быть в каком-то смысле конструктивным.
Далее берется такое множество и строятся все семантические следствия. А так как
естественная дедукция является корректной и полной, можно утверждать, что все се-
мантические следствия – это и формальные следствия. Далее запускается аппарат, кото-
рый позволяет выводить из формул ? с использованием правил вывода другие теоремы
и знаем гарантированно, что все то, что мы выводим – это теоремы нашей теории.
Остается неразрешенным вопрос, а в каком соотношении находится теория, постро-
енная на множестве аксиом ? и теории исходной модели. Если ? подобрали удачно, в
том смысле, что все формулы верны в модели M, то ясно, что теория, построенная на
? будет подмножеством теории модели. А будет ли совпадение? Чуть позже выясним
этот вопрос конкретно для арифметики.
Рассмотрим некоторую теорию. В нашем примере про шахматы все формулы теории
получались из одной аксиомы. Вообще, если можно предъявить множество аксиом, из
которых выводятся все формулы тории, то теория называется эффективно аксиомати-
зируемой. Или, говоря более формальным языком:

Определение 5.2 Теория T называется эффективно аксиоматизируемой, если суще-
ствует такое разрешимое множество ? : T = ?|= .
27


Такое множество ?, не всегда конечно, если же оно все же оказалось конечным, то
такая теория называется конечно аксиоматизируемой.

Определение 5.3 Теория T называется конечно аксиоматизируемой, если существу-
ет такое конечное ? : T = ?|= .

Еще нам бы хотелось, чтобы теория не содержала формул, о которых “ничего нельзя
сказать”, то есть, чтобы была верна либо формула, либо ее отрицание.

Определение 5.4 Теория T называется полной, если для любого P ? L? выполняется
либо P ? T либо ¬P ? T .

Определение 5.5 Класс K алгебраических систем называется аксиоматизируемым,
если существует сигнатура ? и такое множество предложений Z сигнатуры ?, что
для любой системы ?

? ? K Если и только если ( сигнатура ? равна ? и ? ? для всех ? ? Z)

Замечание 5.1 Любая теория модели полна.

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

Замечание 5.2 Если эффективно аксиоматизируемая теория T полна, то она разре-
шима.

Упражнение 5.1 Если теория T суть перечислимое множество и она полна, то она
разрешима.

Упражнение 5.2 Если T = ? |= , где ? перечислимо, то сама теория эффективно
аксиоматизируема.

Лемма 5.1 Для любой программы P на регистровой машине с регистрами R0 , . . . , Rn
найдется фраза ?p (?1 , . . . , ?2n+3 ) ? L? (L? – достаточно богатый язык), такая что
для любой конфигурации k0 , . . . , kn , L, m0 , . . . , mn ) N ?(k0 , . . . , kn , L, m0 , . . . , mn ) если и
только если программа начав с (0, k0 , . . . , kn ) приходит за конечное время к (L, m0 , . . . , mn )

Теорема 5.1 Th(N) – регистрово неразрешима.
28 Формальные теории


Доказательство: Докажем что Th(N) не является регистрово разрешимой.
Воспользуемся регистровой неразрешимостью ?halt . Пусть задана программа P. По
лемма найдем для нее ?p .

?p : = ??n+3 , . . . , ??2n+3 ?p (0, . . . , 0, k, ? n+3 , . . . , ? 2n+3 )
n+1


где k – метка halt. Получаем соответствие: P > ?p , где N |= ?p или, что тоже, P : >
halt.
Если Th(N) – регистрово разрешимоe множество то и ?halt регистрово разрешимо,
а это не так.

Следствие 5.1 Th(N) не является перечислимой и не является эффективно аксио-
матизируемой.

Доказательство: Th(N) – полна. Значит, с одной стороны, если она перечислима, то
она и разрешима. С другой стороны, если она эффективно аксиоматизируема, то также
является разрешиомой.
Можно даже сказать, что Th(N) неразрешима, и добавляя в неё формулу (формулы)
мы не добьемся её полноты. Кроме того существует теорема теориии чисел о которой
ничего нельзя сказать пользуясь PA, вследствие её неполноты.
То есть наша теория (Th(N)) оказалась несовершенной. А несовершенную теорию
следует усовершенствовать. Может быть, мы “забыли” какие-то важные аксиомы? Сле-
дует найти их, присоединить к аксиомам Th(N), и в результате мы получим совершен-
ную систему? К сожалению наш результат распространяется и на любые расширения
теории. Если мы найдем эту “недостающую” теорему и добавим её в Th(N) в качестве
аксиомы, то Th(N) останется неполна. Таким образом P A|= не полна, а T h(N) нераз-
решима, и даже неперечислима. То есть, хотя мы можем перечислить все следствия из
аксиом, но мы не можем даже перечислить все теоремы теории чисел.
Заметим, что мы хотя и доказали неполноту P A|= , но мы не предъявили ту формулу,
для которой ни она, ни её отрицание не выводятся из системы аксиом. Мы собираемся
сформулировать теорему Геделя в форме независимой от арифметического языка, и,
кроме того, предъявим конструкивный алгоритм построения данной формулы. Для
того, чтобы перейти к этому нам понадобятся некоторые определения.

Определение 5.6 Будем говорить, что Q ? Nr , является выразимым в ? ? L?ar ,
если существует формула ?Q (?0 , ?1 , . . . , ?r?1 ), такая что

1. если (n0 , n1 , . . . , nr?1 ) ? Q, то ? |= ?Q ((n0 ), (n1 ), . . . , (nr?1 ))

2. если (n0 , n1 , . . . , nr?1 ) ? Q, то ? |= ¬?Q ((n0 ), (n1 ), . . . , (nr?1 ))

Если ? несовместно, то в нем выразимо любое Q ? N.
5.1 Теорема о неподвижной точке 29


Определение 5.7 Функция F : Nr > N называется выразимой в ? ? L?ar , если
существует формула ?Q (?0 , ?1 , . . . , ?r?1 ), такая что
1. если F (n0 , n1 , . . . , nr?1 ) = nr , то ? |= ?F (n0 , n1 , . . . , nr )
2. если F (n0 , n1 , . . . , nr?1 ) = nr , то ? |= ¬?F (n0 , n1 , . . . , nr )
3. ? |= ?r (?F (n0 , n1 , . . . , nr?1 , ?r ))
Функции выразимые в ? выразимы в ? ? ?. Если ? ? то всё выразимо в ?.
ND

Лемма 5.2 Если ? – все теоремы T h(N), то в нем выразимы все разрешимые мно-
жества и вычислимые функции.

<< Пред. стр.

стр. 3
(общее количество: 5)

ОГЛАВЛЕНИЕ

След. стр. >>