Как можно трактовать в теории EA операцию возведения в степень, если соответствующего символа в языке теории нет? Другой вопрос: мы уже несколько раз писали формулы, заменяющие в EA интуитивно понимаемые предикаты вроде "x - простое число":
1<x & ~(EyEz)(y<x & z<x & x=y*z).
Какие требования мы должны предъявлять к такого рода формулам? Если кто-то предлагает формулу и утверждает, что она "выражает" то-то и то-то, как это проверить? Для таких ситуаций вводятся понятия выразимости предикатов и представимости функций.
Будем говорить, что формула A(x,y) (x, y - единственные ее свободные переменные) выражает в теории EA предикат a(x,y) (x,y пробегают по натуральным числам), если для любых натуральных чисел m, n
а) если имеет место a(m, n), то EA |- A(m, n), - -
б) если a(m, n) не имеет места, то EA |- ~A(m, n).
Напоминаем, что m, n - термы EA, обозначающие числа m, n: 2 - это 1+1 и т.д. Можно спорить, являются ли эти требования достаточными, чтобы признать формулу A действительно выражающей предикат a, но, вне всякого сомнения, эти требования необходимы. (Мы сформулировали определение для случая двухместных предикатов, аналогично определяется выразимость одноместных, трехместных и т.д. предикатов.)
Легко проверить, что формула x=y выражает в EA обычное интуитивно понимаемое равенство натуральных чисел. В самом деле, для любых m, n: а) если m=n, то EA |- m=n (термы m, n в этом случае просто совпадают), б) если m<>n, то EA |- ~(m=n) (проверьте).
Интересно было бы получить какую-то характеристику класса тех предикатов, которые выразимы в EA. Если теория EA противоречива, то в ней доказуема любая формула и поэтому - в смысле принятого нами определения - в EA можно выразить любой предикат (например, формула x=y выражает любой двухместный предикат). Если же теория EA непротиворечива, то каждая формула может выражать не более одного предиката, и поскольку формул существует только счетное число, то и выразимых предикатов будет не более чем счетное число. Но даже всевозможных одно- местных предикатов "существует" несчетное число, т.е. должны "существовать" невыразимые предикаты.
Какие же предикаты выразимы в EA, а какие - нет (если предположить, что эта теория непротиворечива)? Легко заметить, что всякий выразимый в EA предикат должен быть эффективно разрешимым (по другой терминологии - рекурсивным) предикатом. В самом деле, если формула A(x,y) выражает в EA предикат a(x,y), то для решения вопроса об истинности a(m, n) мы должны установить, которая из формул A(m, n), ~A(m, n) доказуема в EA (точно известно, что одна из них доказуема). Множество всех теорем EA эффективно перечислимо (см.упражнение 1.4). Перечисляя всевозможные теоремы EA, мы рано или поздно встретим либо формулу A(m, n), либо ~A(m, n) (но только одну из них, поскольку EA - по предположению - непротиворечива). Это и решит вопрос об истинности a(m, n). Таким образом, a(x,y) - эффективно разрешимый предикат.
Решить вопрос, противоречива теория EA или нет, мы не в состоянии. Все, что можно сделать, - это попытаться доказать независимо от предположения о непротиворечивости EA, что все эффективно разрешимые предикаты выразимы в EA. Несколько позднее мы это сделаем.
Будем говорить, что формула F(x,y,z) представляет в EA функцию f(x,y) (отображающую натуральные числа в натуральные), если для всех k, m, n таких, что f(k, m)=n,
а) EA |- F(k, m, n),
б) EA |- (Az)(~(z=n)->~F(k, m, z)).
Можно спросить по поводу этого определения: если отождествлять функцию f с предикатом f(x,y)=z, то почему бы не считать ее представлением формулу, выражающую в EA этот предикат? Это означало бы замену условия б) условием
б1) если f(k, m)<>n, то EA|- ~F(k, m, n).
Легко видеть, что из б) вытекает б1). В самом деле, если f(k, m)<>n, но f(k,m)=q, то EA |- ~(n=q), а согласно условию б) EA |- ~(n=q)->~F(k, m, n), т.е. EA|- ~F(k, m, n), что и требовалось. Однако вывести б) из б1) мы уже не в состоянии. Поэтому можно сказать, что формула F, обладающая свойствами а+б), представляет функцию f "лучше", чем формула, которая обладает только свойствами а+б1). Если в случае а+б1) для каждого n, отличного от f(k, m), достаточно иметь отдельное доказательство формулы ~F(k, m, n), то в случае а+б) для всех таких n должно быть дано единое доказательство: EA |- ~(z=q)->~F(k, m, z), где q=f(k, m).
Если теория EA противоречива, то в ней представима любая функция.
Упражнение 3.7. Убедитесь, что если EA непротиворечива, то всякая всюду определенная функция, представимая в EA, должна быть вычислимой.
Мы хотим доказать, что в EA (независимо от предположения непротиворечивости) представима любая вычислимая функция.
Между выразимостью предикатов и представимостью функций существует простая и естественная связь.
Упражнение 3.8. Докажите, что некоторый предикат выразим в EA тогда и только тогда, когда его характеристическая функция представима в EA.
Достаточно, таким образом, установить представимость в EA всякой вычислимой функции, чтобы одновременно можно было утверждать, что всякий разрешимый предикат выразим в EA.
ТЕОРЕМА О ПРЕДСТАВИМОСТИ. Всякая вычислимая функция представима в теории EA.
Доказательству теоремы о представимости посвящена оставшаяся часть этого раздела.
Сначала рассмотрим одно из точных определений понятия вычислимой функции: функция, отображающая натуральные числа в натуральные числа, называется вычислимой, если существует машина Тьюринга, вычисляющая ее значения. Всякая машина Тьюринга M определяется:
а) алфавитом внутренних состояний (программист может считать их состояниями оперативной памяти, тогда m=2k, где k - количество бит в памяти):
QM = {qstart, qstop, q1 ,..., qm},
б) алфавитом ленты:
AM = {0, 1, a1, ..., an},
в) программой PM, состоящей из конечного числа команд вида qa -> q'a'e, где q, q' in QM (q - "старое", q' - "новое" состояние машины), a,a' in AM (a - "старый", a' - "новый" символ в клетке, обозреваемой головкой машины), e = -1, 0, +1 (указание, куда переместить головку). В программе не должно быть двух команд с одинаковыми левыми частями.
Под этим формальным определением скрыта следующая наглядная модель:
M-------------| q |
| a | ... |
В каждый момент (выражаемый, например, целым числом секунд)
а) машина M находится в одном из состояний QM,
б) каждая клетка ленты (она бесконечна только вправо) находится в одном из состояний AM,
в) головка машины обозревает некоторую клетку ленты. Если в момент t машина M находилась в состоянии q, головка обозревала в клетке символ a и в программе PM содержится команда qa -> q'a'e, то к моменту t+1 машина перейдет в состояние q', символ a она заменит символом a' и в зависимости от e головка перейдет: если e=-1, то на одну клетку влево, если e=0 - останется на месте, если e=+1 - на одну клетку вправо (если головка обозревает самую левую клетку ленты, то e=-1 равносильно e=0).
Мы будем говорить, что машина M вычисляет (всюду определенную) функцию f(x,y), если для всех значений x,y, отправляясь от ситуации, в которой
a) M находится в состоянии qstart,
б) головка обозревает левую клетку ленты,
в) в начале ленты находится последовательность символов
0 1 1...1 0 1 1...1 0,
-------- --------
x ------- y
через конечное число шагов, следующих по программе PM, машина приходит к ситуации, в которой
а) она находится в состоянии qstop,
б) на ленте находится последовательность
0 11...1 0.
------
f(x,y)
Если для функции f(x,y) удалось построить такую машину M, мы будем называть f вычислимой. Это определение оказывается эквивалентным всем другим точным определениям понятия вычислимой функции.
В качестве примера напишем программу для машины Тьюринга, которая вычисляет функцию f(x)=x+1. Задача этой программы - пройти через массив единиц до нуля, заменить нуль единицей, а рядом записать новый нуль:
QM = {qstart, qstop, q, q'}, AM = {0,1},
PM = {qstart, 0 -> q, 0, +1;
q, 1 -> q, 1, +1;
q, 0 -> q', 1, +1;
q', 0 -> qstop, 0, 0;
q', 1 -> qstop, 0, 0}
Упражнение 3.9. а) Напишите программы для машин Тьюринга, вычисляющих функции x+y, x*2, x*y, 2x, [log2 x].
б) Используя какой-либо язык программирования, напишите интерпретатор машин Тьюринга. Это программа, которая получает программу машины и начальное состояние ленты, а затем "симулирует" работу введенной программы и после ее остановки печатает заключительное состояние ленты. Такой интерпретатор позволяет отлаживать программы для машин Тьюринга, физически этих машин не имея.
Для доказательства теоремы о представимости мы должны записать отношение f(x,y)=z в виде некоторой формулы F(x,y,z) на языке EA. При этом будем использовать то, что между парой аргументов x, y и значением z должна существовать связь в виде вычислительного процесса, следующего по программе PM подходящей машины Тьюринга.
Своей цели мы достигли бы значительно быстрее, если бы в языке EA имелись специальные переменные для так называемых ситуаций. Ситуацией (полным состоянием машины) в момент времени t будем называть последовательность
(q, l, d0, d1, ..., ds-1),
где q - внутреннее состояние машины в данный момент, l - номер клетки, обозреваемой головкой машины (нумерация начинается с нуля), d0, d1, ..., ds-1 - символы в клетках с номерами 0, 1, ..., s-1. Если C1, C2,... - переменные, значениями которых являются такие ситуации, было бы удобно иметь в языке EA также специальные символы для функций:
q(C)=q в ситуации C,
l(C)=l в ситуации C,
s(C)= число клеток, учитываемых в C,
di(C)=di в ситуации C.
Имея все это в языке EA, мы могли бы поступить следующим образом. Сначала строим формулы START и STOP. Формула START(C, x, y) должна утверждать, что C - начальная ситуация, в которой на ленте задана пара аргументов x, y:
q(C)=qstart & l(C)=0 & x+y+3=s(C) & d0(C)=0 &
& Ai (0<i<x+y+3 -> di(C)=1 V di(C)=0 & (i=x V i=x+y+1)).
Формула STOP(C,z) должна утверждать, что C - заключительная ситуация, в которой вычислено значение z:
q(C)=qstop & z<s(C) & d0(C)=0 & Ai (0<i<z+1 -> di(C)=1 V (di(C)=0 & i=z)).
Далее, каждой команде kappa in PM (где M - машина, вычисляющая функцию f), имеющей вид qa -> q'a'e, мы сопоставим формулу STEPkappa (C1, C2 ), которая утверждает, что ситуация C2 получается из ситуации C1 в результате выполнения команды kappa. Рассмотрим случай e=+1:
(EuEv)[q(C1)=q & l(C1)=u & s(C1)=v & du(C1)=a &
& q(C2)=q' & du(C2)=a' & l(C2)=u+1 & (Ai<=v)(i=u V (Ej)(di(C1)=j & di(C2)=j)) &
& ((u<v & s(C2)=v) V (u=v & s(C2)=v+1))].
Упражнение 3.10. Напишите аналоги этой формулы для случаев e=-1, 0.
Следующий этап - формула CHAINEM(C1, C2), утверждающая, что ситуация C2 получается из C1 с помощью конечного числа шагов по программе PM. Здесь удобно ввести уже специальные переменные L1, L2, принимающие в качестве значений конечные последовательности ситуаций. Соответственно нам потребуются также символы функций:
delta(L)= число ситуаций в последовательности L,
gammai(L)= i-я ситуация в L.
В языке EA таких средств нет, но мы будем пока игнорировать это обстоятельство. Формула CHAINEM(C1, C2) имеет вид
(ELEw)[delta(L)=w+1 & gamma0(L)=C1 & gammaw(L)=C2 &
& (Ai<w)(EC3EC4) (gammai(L)=C3 & gammai+1(L)=C4 & STEPM(C3, C4)],
где STEPM(C3, C4) - формула
STEPk1(C3, C4) V STEPk2(C3, C4) V ... V STEPkt(C3, C4),
а команды k1, k2, ..., kt составляют программу PM.
Если машина M вычисляет функцию f(x,y), то формулу F(x,y,z), утверждающую, что f(x,y)=z, можно написать теперь следующим образом:
(EC1EC2 )(START(C1, x, y) & CHAINEM (C1, C2) & STOP(C2, z)).
Одержав эту победу, мы вынуждены, однако, вернуться к языку EA. В нем нет переменных для ситуаций, нет функциональных символов, которые мы успели ввести, не говоря уже о переменных для последовательностей ситуаций. Поэтому, если мы хотим, чтобы формула F(x,y,z) действительно "вошла" в язык EA, мы должны воспроизвести все "излишества" средствами EA.
Константы вроде qstart, qstop, 0, 1, q, q', a, a' и т.д. "вложить" в EA нетрудно - каждую из них можно заменить некоторым натуральным числом - ее кодом (при этом будет использован только конечный набор чисел - алфавиты QM , AM конечны). Но что делать с ситуациями? Чтобы они "вошли" в EA, их также нужно закодировать натуральными числами. Если внутренние состояния машины и символы на ленте уже закодированы натуральными числами, то ситуации превратились в конечные последовательности таких чисел. Мы должны научиться, следовательно, представлять любые конечные последовательности натуральных чисел одним натуральным числом (в худшем случае - двумя или тремя). Причем сделать это нужно так, чтобы функции q(C), di(C) и т.д. можно было представить формулами EA.
К.Геделю принадлежит идея использовать для этой цели так называемую китайскую теорему об остатках. Рассмотрим следующую задачу: найти число, которое при делении на 3 дает остаток 2, при делении на 5 - остаток 3, при делении на 7 - остаток 4. Если повезет, решение этой задачи можно угадать:
53=3*17+2=5*10+3=7*7+4.
Рассмотрим, однако, общий случай: найти число, которое при делении на заданные числа дает заданные остатки. Заданные числа обозначим через u1, u2, ..., un, это натуральные числа >=2. Заданные остатки обозначим через v1, v2, ..., vn; таким образом, 0 <= vi < ui. Если числа ui, uj имеют общий делитель, то остатки при делении на эти числа уже нельзя выбрать независимо. Например, если ui , uj - оба четные, то соответствующие остатки должны иметь одинаковую четность, иначе задача не будет иметь решения:
x=ui yi+vi = uj yj +vj, ui = 2ui', uj = 2uj', vi - vj = 2(ui'yi - uj'yj).
Поэтому ситуация упростится, если мы потребуем, чтобы числа u1, u2, ..., un были попарно взаимно простыми (т.е. чтобы никакие два из них не имели общих делителей). В таком случае задача всегда имеет решение, как утверждает
КИТАЙСКАЯ ТЕОРЕМА ОБ ОСТАТКАХ. Если даны попарно взаимно простые числа u1, u2, ..., un (ui>=2 для всех i) и числа v1, ..., vn (0<= vi < ui для всех i), то найдется число p, меньшее произведения u1u2...un, которое при делении на ui дает остаток vi (и так для всех i).
Д о к а з а т е л ь с т в о. Каждому числу p, где
0 <= p < P = u1u2...un,
сопоставим "вектор остатков" при делении на u1, ..., un. Покажите, что два числа могут иметь один и тот же вектор остатков, только если их разность делится на P.
С помощью китайской теоремы об остатках мы могли бы кодировать последовательность натуральных чисел v0, v1, ..., vn-1, представляя каждое vi как остаток от деления некоторого числа p на число ui из набора u0, u1, ..., un-1 , который мы должны научиться генерировать каким-то достаточно простым способом. Иначе кодирование не получится. Самый простой способ - представить ui как линейную функцию от i: u = yi+z. Но как подобрать коэффициенты y, z? Числа ui должны быть взаимно простыми. Если d общий делитель ui и uj , то d делит также разность ui - uj = y(i-j). Если возьмем z=y+1, т.е. ui = 1+y(1+i), то делители y не смогут быть общими делителями ui, uj. Ими могут быть тогда только делители разности |i-j|, т.е. числа <=n-1. Но если к тому же еще y делится на (n-1)!, то и эти числа не смогут быть общими делителями ui , uj, т.е. числа u0, ..., un-1 будут взаимно простыми. И если, кроме того, y настолько велико, что u0 > v0, u1 > v1, ..., un-1 > vn-1, то согласно китайской теореме об остатках найдется число p, которое при делении на u0 дает остаток v0, при делении на u1 - остаток v1, ... , при делении на un-1 - остаток vn-1.
Пару чисел (x, y) мы могли бы считать кодом последовательности v0, v1, ..., vn-1, но в этих числах никак не отражается число n. Если же вместо v0, v1, ..., vn-1 закодировать указанным способом последовательность n, v0, v1, ..., vn-1, то соответствующая пара (x, y) стала бы действительно полноценным кодом v0, v1, ..., vn-1.
Функцию
beta(x, y, i) = остаток от деления x на 1+y(1+i)
принято называть бета-функцией Геделя. Мы установили, что для любого набора натуральных чисел v0, ..., vn-1 можно подобрать числа x, y такие, что
beta(x, y, 0)=n, beta(x, y, 1)=v0,..., beta(x,y,n)=vn-1.
Отметим также, что бета-функцию можно представить в теории EA следующей формулой B(x, y, i, j) (утверждающей, что beta(x, y, i)=j):
(Ez)(x=(1+y*(1+i))*z+j & j<1+y*(1+i)).
Теперь можно переписать формулы START, STOP и т.д. средствами языка EA. О константах мы уже условились - все состояния машины M, все символы на ленте будем кодировать натуральными числами. Далее, ситуация - последовательность (q, l, d0, d1, ..., ds-1) становится теперь последовательностью натуральных чисел, которую можно закодировать двумя натуральными числами a, b, такими, что
beta(a, b, 0)=s, beta(a, b, 1)=q, beta(a, b, 2)=l, beta(a, b, i+3)=di
(для всех i). Кванторы вида EC, где C - переменная для ситуаций, можно заменить теперь кванторами EaEb, где a,b - уже переменные для натуральных чисел. Равенства, содержащие "незаконные" функциональные символы:
s(C)=s, q(C)=q, l(C)=l, di(C)=di,
можно заменить равенствами
beta(a, b, 0)=s, beta(a, b, 1)=q, beta(a, b, 2)=l , beta(a, b, i+3)=di.
Устранение "незаконных" символов из неравенств вида s1 < s(C) также не составляет проблемы:
(Es2)(beta(a, b, 0)=s2 & s1 < s2).
Упражнение 3.11. Перепишите средствами EA формулы START, STOP, STEPkappa, STEPM. Определите длину каждой формулы.
В формуле CHAINEM появились новые, еще более сложные переменные - для конечных последовательностей ситуаций, а также функциональные символы delta(L), gammai(L). Отдельную ситуацию мы научились кодировать двумя натуральными числами. Если ситуация Ci закодирована парой чисел (ai , bi), то последовательность L={C0, C1, ..., Cn-1} мы можем закодировать как последовательность чисел
n, a0, b0, a1, b1, ..., an-1, bn-1.
Если (a,b) - код этой последовательности, то формулу delta(L)=w можно заменить на beta(a, b, 0)=w, а формулу gammai(L)=C - на
beta(a, b, 2i+1)=a' & beta(a, b, 2i+2)=b',
где (a',b') - код ситуации C. Квантор EL, где L - переменная для последовательностей ситуаций, следует заменить кванторами EaEb.
Упражнение 3.12. Сделайте все эти замены в формуле CHAINEM и определите ее длину. То же сделайте и для формулы F(x,y,z), утверждающей, что f(x,y)=z.
Итак, для каждой вычислимой функции f(x, y) исходя из машины Тьюринга, вычисляющей ее, мы умеем строить формулу F(x, y, z) в языке EA, которая (в нашем интуитивном ее понимании) утверждает, что f(x, y)=z. Чтобы завершить доказательство теоремы о представимости, мы должны показать, что в EA доказуемы формулы
F(k, m, n), ~(z=n)->~F(k, m, z),
(при условии, что f(k, m)=n). Мы не будем этим заниматься (как не занимались выводом из аксиом EA сколько-нибудь полной системы основных свойств натуральных чисел). Желающие проследить за всеми деталями могут обратиться к книге Э.Мендельсона [1976].
Будем считать теорему о представимости доказанной.