Некоторые алгоритмические вопросы для полимодальных логик доказуемости Пахомов Федор Николаевич

Замкнутые фрагменты логик GLPn

Правильно построенные формулы логики GLPn — это GLP-формулы, в которых из модальных связок встречаются только [0], [1],... , [п]. Исчисление в гильбертовском стиле для логики GLPn задается теми аксиомами и правилами вывода исчисления для GLP, которые лежат в языке логики GLPn. Отметим, что множество теорем логики GLPn совпадает со множеством теорем логики GLP, которые являются GLPyj-формулами [10]. Метод использованный в предыдущем разделе существенно использует бесконечно много модальностей и, тем самым этот метод не может быть использован для доказательства PSPACE-трудности проблемы распознавания выводимости замкнутых формул в логиках GLPn.

Центральным результатом этого раздела является следующая теорема. Теорема 2. При всех натуральных п проблема распознавания выводимости в логике GLPn для замкнутых формул разрешим/! за полиномиальное время.

Начнём с плана доказательства. Мы используем модель Крипке (определение понятия модели Крипке см. [11]) Ы такую, что замкнутый фрагмент логики GLPn является полным относительно этой модели. Каждой замкнутой GLPjj-формуле мы ставим в соответствие множество миров модели Ы , в которых она выполняется. Полнота замкнутого фрагмента GLPn относительно модели Ы означает, что всякая замкнутая GLPfj-формула доказуема в GLPn тогда и только тогда, когда этой формуле соответствует множество всех миров модели Ы . Отметим, что для всякой замкнутой GLPjj-формулы (р соответствующее ей множество может быть получено интерпретацией пропозициональных констант и пропозициональных связок из ср, как специальных множеств миров Ы и специальных операций на множествах миров Ы , соответственно.

Мы используем коды из множества С" для эффективного представления множеств миров моделиЫ (отметим, что существуют множества миров, которым не соответствует ни одного кода). В разрешающем алгоритме мы используем следующие вычислимые функции (в полном доказательстве у них имеются дополнительные аргументы и параметры):

Теперь опишем наш метод оценки времени работы алгоритма. Мы вводим функции с" и w для измерения сложности кодов, переданных на вход. Далее мы получаем оценки времени работы и сложности результирующих кодов для функций Сшрі, Intr, RQ-IHV, R\-Inv,..., Rn-Inv в терминах сложности кодов на входе. Это дает нам полиномиальную оценку на сложности используемых кодов, в смысле указанных выше функций, и на время работы разрешающего алгоритма. В большинстве лемм этого раздела мы одновременно даем описание алгоритма и верхнюю оценку на время его работы.

Теперь мы переходим к точному описанию требуемой нам модели Крипке. Обозначим через On класс всех ординалов. Теорема Кантора о нормальной форме ординалов утверждает, что каждый ординал а 0 может быть единственным образом представлен в виде суммы

Мы будем использовать модель вычислений RAM (машина с произвольным доступом к памяти). Точнее говоря, мы используем определение RAM из [16] со временем исполнения всех инструкций равным 1. Все ограничения на время исполнения даны для этой модели вычислений. Отметим, что в [16] было показано, что RAM может быть симулирована на многоленточных машинах Тьюринга с не более чем кубическим ростом времени исполнения.

Мы даем эффективное кодирование некоторых подмножеств U. Для доказательства этого мы используем кодирование ординалов, меньших о, известное как канторовская система ординальных обозначений. Каждый ординал (3 Єо кодируется, либо символом 0, если он равен где при каждом і от 0 до т — 1 строка Sj представляет ординал /. Из технических соображений одновременно со строкой s, представляющей ординал /3, мы храним массив а натуральных чисел такой, что

Ясно, что для строки s, представляющей некоторый ординал, мы можем сконструировать соответствующий ей массив а за время (9(s). Очевидно, это дает нам код для каждого ординала меньшего е$. В силу теоремы Кантора о нормальной форме ординалов этот код единственен. Когда мы говорим о вычислимых функциях от ординалов а Єо, мы передаем ЭТИ ОрДИНаЛЫ На ВХОД фуНКЦИИ В ВИДЄ Четверок (siink, ЛЦпк, ferst, Mast); где siink является ссылкой на строку s, ацпк является ссылкой на массив а, а пара s и а образуют код ординала, 0 fcfirst fciast s, и подстрока s = s[fcfirst]s[fcfirst + 1] . .. s[Mast — 1] является представлением ординала а. Это соглашение позволяет нам работать с ординалами (3 = UJP + UJ m l, как с неизменяемыми списками ординалов (/Зо,. .. , /3m_i), т.е. мы можем хранить ссылки на /Зг- в (9(1) памяти, строить ссылки на /Зг+і и /3j_i из ссылки на (ЗІ за 0{\) времени и делать вызовы функции с аргументом /Зг- за 0{\) (без учета времени работы самой функции), передавая ей ссылку на (ЗІ. Далее в этом разделе нас будут интересовать только ординалы, меньшие о. В этом разделе мы отождествляем ординалы меньшие Єо и и их коды.

Определимые в полурешетках слов свойства

В этом разделе мы определяем понятие GLP-слова и изучаем некоторые свойства GLP-слов, которые мы в дальнейшем будем использовать для получения результатов о разрешимости и неразрешимости элементарных теорий структур, определяемых на основе GLP-слов.

Мы рассматриваем множество W всех формул вида (щ)(щ) ... (щ)Т. Такие формулы называются GLP-слоеалш; также для краткости в рамках данной диссертации мы называем их просто словами. Для обозначения слов мы используем буквы А, В,.... Из соображений удобства мы часто будем опускать знаки модальностей и Т, записывая слово (ni)(n2) . .. (щ)Т как щщ ... щ. Для слов А = щщ.-.щ и В = m\im i...m\ запись АВ означает слово п\п і... щт\т і... т\. Через Wn мы обозначаем множество всех слов т\ гщ ... ті, для которых все гщ п.

На множестве всех GLP-формул имеются бинарные отношения и, определяемые следующим образом (см. [7]):

Обозначим через Sn множ;ество всех слов, любой символ которых больше или равен п. Мы обозначаем через отношение GLP-доказуемой эквивалентности на формулах и, в частности, на словах:

Отметим, что всякое непустое слово А Є Sk может быть единственным образом представлено в виде A = AikA2k... кАп, где Аг Є Sk+i Функции оп: Sn — On одновременно определяются следующими рекуррентными соотношениями:

Тем самым каждая оп задает изоморфизм (5п/ ; п) и упорядоченного множества (єо; ). Также, отсюда несложно видеть, что для к,1 п ограничения бинарных отношений & и і на множество Sn совпадают. Определим множество NF всех слов, находящихся в нормальной форме. Зададим принадлежность слов к NF индукцией по длине.

Пусть минимальный символ слова А Т равен к и А = А1&А2&... кАп, где все Aj Є Sk+i- Тогда А Є NF, если и только если Ai,..., Ап Є NF и Аг-__і fc+i Aj при і от 1 до п — 1. Для каждого слова А слово В Є ATF называется нормальной формой слова А, если В А. Предложение 2.2. [8, следствие 5] Для каждого слова А существует единственное эквивалентное ему слово В Є NF.

Приведем здесь без доказательства процедуру приведения слова к нормальной форме, которая является незначительно перестроенной процедурой из доказательства [8, предложение 3]. Будем сводить построение нормальной формы слова к построению нормальных форм слов меньшей длины. Пустое слово уже приведено к нормальной форме. Перейдем к случаю непустого слова А. Пусть минимальный символ слова А равен к и оно имеет вид А = А\к. .. кАп, где Ai,..., Ап Є »%+і-Приведем слова А і и А2&. .. кЛп к нормальной форме — это будут слова Ві и В2к...кВт соответственно, где Bi,...,Bm Є Sk+i- Положим A = {s I 2 s m, Bs -ftk+i Bi}. Если множество А непусто, то нормальная форма А равна В\кЕ ік... кВт, где / = min(A), иначе нормальная форма А равна Bi.

Вг-, как слова в алфавите из натуральных чисел, являются подсло-вами В от первого вхождения г, включительно, до первого вхождения г — 1, не включая его (до правого конца для г = 0). Из определения о$ видно, что для всех і к мы имеем Оо(Bj) 0о(В). Тем самым для всех г к Вг- о А, а в силу согласованности о и г- на мы имеем Bj j А. Отсюда GLP \ А — Вг для всех г А;. Следовательно GLP h А — В.

Мы обозначаем через Wn, множество всех слов А = (mi) (77) {тк)Т для которых все т« п. Для всех ординалов а ш обозначим через Wa множество Wa П NF. Несложная проверка показывает, что доказательство леммы 9 из [8] дает следующую лемму. Пусть даны ординал а ш число к а. Тогда для любых слов А, В Є Sk П Wa эффективно строится слово С Є Sk П Wa такое, что GLP Ь А Л В + С. Введем операцию конъюнкции слов. Пусть А и В — слова, а С — единственное слово из NF такое, что GLP Ь А Л В -о- С. Положим АПВ = С.

Кроме того, для всех натуральных к введем функции d : W — W. Для всякого слова А мы полагаем i&(A) равным единственному слову из NF эквивалентному (к)А.

Несложно видеть, что для любых а ш и п а, для всякого А Є Wa мы имеем dn(A) Є Wa и для всяких А, В Є Wa мы имеем АПВЄ W%.

Предположим, что /ijfc(A) /fyfc(B) и докажем, что /i&+i(A) /ife_i_i(B). Слово /i)k(A) имеет вид /г&(А) = hk+i(hk(A))kAikA2k... кАп, где Аі,...,Ап Є iS%__i. Заметим, что /i&+i(A) = /ijfc+i(/ifc(A)) и тем самым MA) = +i( A) ... ,

Пусть слово С — нормальная форма слова /і&(А). Рассмотрим построение С по описанной ранее процедуре приведения слова к нормальной форме (см. стр. 38). Пусть нормальная форма Аік к... к/\п имеет вид С\кС2к.. . кСт, где все Q Є Sk+i, а нормальная форма /і&+і(А) равна слову Со- Исходя из процедуры построения нормальной формы слова мы выводим, что либо С = CokCik... кСт для некоторого положительного натурального числа I т, либо С = Со- Следовательно, /ijH-i(C) = Со /IJH-I(A).

Проведя аналогичное рассуждение для В и нормальной формы слова /ifc(B), равной D, мы получим, что /i&+i(D) /І&+І(В). В силу единственности нормальной формы слова и предположения индукции С = D. Тем самым hk+\(A) hk+\(B), что завершает доказательство

Слова из двух символов

Пусть даны теория Ті сигнатуры а\ и теория Т2 сигнатуры о"2 без функциональных символов. Пусть дана интерпретация Г сигнатуры о"2 в о"! и ей соответствует перевод формул trr : F 1— F . При этом мы предполагаем, что Г интерпретирует равенства равенствами. Мы называем Г правой тотальной интерпретацией [21, глава 5.3], если всякая первопорядковая формула А сигнатуры о"2 такова, что если ее перевод А является теоремой Ті, то и сама А оказывается теоремой теории Т2. Отметим, что это определение отлично от обычного понятия интерпретации, которое, в рамках такой терминологии, можно называть левой тотальной интерпретацией. Правая тотальная интерпретация называется эффективной, если соответствующий ей перевод рекурсивен. В силу того, что нам будут встречаться только эффективные правые тотальные интерпретации и их эффективность всегда будет очевидна из их конструкции, мы всегда, ничего дополнительно не оговаривая, предполагаем эффективность правых тотальных интерпретаций.

Пусть имеются классы моделей А сигнатуры и\ и В сигнатуры о"2, а также интерпретация Г сигнатуры о"2 в сигнатуре и\. Рассмотрим класс моделей С сигнатуры о"2, являющийся совокупностью образов всех моделей из А под действие преобразования моделей, задаваемого Г. Ясно, что Г является правой тотальной интерпретацией Th(A) в Th(B) тогда и только тогда, когда для каждой модели из В найдется изоморфная ей модель из С.

Теория Т называется наследственно неразрешимой если всякая ее подтеория неразрешима.

Если теория Т2 наследственно неразрешима и имеется эффективная правая тотальная интерпретация теории Т2 в теории Т\, то теория Т\ неразрешима.

Доказательство. Пусть и\ сигнатура теории Ті, а 0"2 сигнатура теории Т2, Г является эффективной правой тотальной интерпретацией Т2 в Ті и Г соответствует перевод trr : F 1— F . Для завершения доказательства предположим противное и придем к противоречию — предположим Ті разрешима. Рассмотрим теорию Е сигнатуры ст А є Е Л Є Ті.

Очевидно, Е в самом деле является теорией. Е разрешима в силу эф фективности trp и разрешимости Ті. Но в силу того, что Г является правой тотальной интерпретацией, Е является подтеорией Т2 и тем са мым неразрешима — противоречие. Теорема 5. Если а ординал ш, а р и q натуральные числа такие, что 0 р и р+1 q а, то теория Th(Wa; о, (р), ( ?)) неразрешима.

Известно, что элементарная теория класса L n наследственно неразрешима [5]. Пусть с — константный символ. Рассмотрим множество А всех моделей вида (Wa; о, (р), ( /),с), где с оценивается произвольным словом А Є Wa. Заметим, что теории Th(A) и ТЬ±(И а; о, (р), (q)) разрешимы или неразрешимы одновременно. В самом деле, из разрешимости первой очевидно следует разрешимость второй. Если же разрешима Th( Wa; о, (р), (q)), то следующая эквивалентность дает разрешимость Th(A):

Далее мы строим правую тотальную интерпретацию ТЪ.(Ь п) в Th(A) и тем самым с помощью леммы 3.3 получаем искомое. Мы полагаем, что универсум интерпретации задается формулой Sl(c,x). Предикат Х\ Li Х і интерпретируется формулой Х\ о Х2, а предикат Х\ hz Х2 интерпретируется формулой (q)x\ о {q)x2 Определим модель 3/\ как результат преобразования, задаваемого определенной выше интерпретацией, примененного к модели ( Wa; o, (p), (Q),C) С константой с оцениваемой как А. Тем самым задано семейство, проиндексированное А Є Wa, моделей Зд той же сигнатуры, что и модели из Lnn. Покажем, что для всякой модели [В, Li, L2) Є L n найдется А Є Wa такое, что Зд изоморфна (В; Li, L2). Положим к = \В\. Обозначим элементы В в соответствие с порядком Li:

Для всех і от 1 до к положим Si равным мощности множества {d Є В d L2 bi}. В силу леммы 3.2, найдется такое А, что u(A) = (Kjt)Sl+i, KfcjS2+b ..., КА)8к+і). Несложно видеть, что 3А изоморфна (5;Li,L2). Тем самым, мы построили требуемую интерпретацию. П

Мы переходим к доказательству разрешимости элементарных теорий Th( Wa; о, Т, (0), (1), (2)) для а Є [2, а;). Для таких а мы построим интерпретации элементарной теории Th( Wa; о, Т, (0), (1), (2)) в разрешимой слабой монадической теории модели (uja\ R) [13]; здесь R — это специальное бинарное отношение, определяемое через кофинальные последовательности. Для этого мы при всех а Є [2, о;) построим цепочку интерпретаций моделей:

Мы строим в лемме 3.9 интерпретацию (Wa; о, Т, (0), (1), (2)) в (uja\ ,ф)+. Модель {иоа] ,ф)+ состоит из ординалов меньших ша, конечных мультимнож;еств ординалов, стандартного порядка на ординалах, специальной функции ф на ординалах и некоторых естественных предикатов для работы с мультимножествами.

В лемме 3.10 мы строи интерпретация (ша; }ф)+ в (ша; ,ф) . 3. Мы строим в лемме 3.12 интерпретацию (ша; ,ф) в (uja]R) . Бинарное отношение R — это отношение определяемое на основе стандартной системы кофинальных последовательностей.

Мы называем конечным мультимножеством функцию / такую, что ее область определения dom(/) конечна и ее область значений гап(/) вложена в [1, о;). Конечное мультимножество / вложено в конечное мультимножество д, если dom(/) С dom(g) и для всякого х Є dom(/) имеет место f(x) д(х); мы обозначаем это / См д- Определим і/(х) — кратность вхождения х в конечное мультимножество /. Если х Є dom(/), то і/(ж) = f(x). Иначе, і/(ж) = 0. Для всякого х и мультимножества / мы определяем

Для всякого множества А мы обозначаем через ЛЛ и){А) множество всех конечных мультимножеств, которым принадлежат лишь элементы А. Мы обозначаем через { 2i,...,an} мультимножество f(x) такое, что dom(/) = { 2i,... ,an} и для всякого х Є dom(/) значение f(x) равно мощности множества {i \ х = а,}.

Рассмотрим односортную модель 21 с носителем А. Определим двусортную модель 21+. Модель 21+ является расширением 21 дополнительной предметной областью ЛЛ и){А), предикатом Єм ограниченным на Л х М Ш(А) и предикатом См, ограниченным на М Ш(А) х М Ш(А).

Некоторые теории ординалов и слов

Во всех примерах, которые встречаются в этой диссертации сигнатуры счетны и допускают эффективное задание (все множества, о которых идет речь в определение сигнатуры разрешимы, а функции рекурсивны). Поэтому далее мы всегда, рассматривая некоторую сигнатуру, предполагаем, что она эффективно задана ничего дополнительно не оговаривая.

Модель 21 сигнатуры а состоит из семейства играющих роль предметных областей множеств At, где t пробегает Т, оценок 1(Р) предикатных символов Р Є Pred и оценок /(/) функциональных символов / Є Fun . Пусть Р Є Pred и РТуре(Р) = (si,... , Sk). Тогда 1(Р) — это подмножество ASl х ... х А,ч. Пусть / Є Fun, FType(f) = ((si,... ,Sk),r). Тогда 1(f) — это функция ASl х ... х ASk — Ar.

Для каждого сорта г- Є Т мы обозначаем символами xtl,ytl, zfi... первопорядковые переменные этого сорта. Естественным образом вводятся многосортные формулы первого порядка с равенством данной многосортной сигнатуры. Также естественным образом вводится понятие истинности этих формул в моделях этой сигнатуры.

Для класса моделей А некоторой сигнатуры а мы обозначаем через Th(A) элементарную теорию этого класса моделей — множество всех первопорядковых предложений сигнатуры О" истинных во всех моделях 21 Є А. В этой диссертации мы придерживаемся теоретико-модельного взгляда на теории первого порядка. Мы называем множество формул первого порядка сигнатуры а теорией, если оно является элементарной теорией некоторого класса моделей А сигнатуры а. Для модели 21 ее элементарная теория — это теория Th({2l}).

Мы говорим, что теория разрешима, если она является разрешимым множеством формул. Мы для доказательства ряда фактов о разрешимости и неразрешимости теорий используем метод интерпретаций [30, 3]. Мы в целом следуем терминологии интерпретаций В. Ходжеса [21, глава 5]. Рассматриваемые нами в этом разделе интерпретации отличаются от используемых В. Ходжесом тем, что мы работаем с многосортными моделями и ограничиваемся одномерными интерпретациями. Кратко опишем связанные с этой техникой понятия в требуемом нам случае. Пусть даны сигнатуры о"! и о"2. Интерпретация Г состоит из:

Когда мы строим интерпретации, если мы не оговариваем иного, то мы считаем, что интерпретации равенств Едг(хг уг\уг у ) — это просто xi{t) _ yi{t). такие интерпретации равенств мы называем абсолютными. Интерпретация Г однозначно задает trr : F і—У F — перевод формул сигнатуры о"2 в формулы сигнатуры а\\ мы не приводим здесь точного задания trr, его построение аналогично построению перевода формул из [21, глава 5]. Пусть Ті теория сигнатуры и\ и Т2 теория сигнатуры о"2-Мы говорим, что Г является интерпретацией Т2 в Ті, если для всякой F Є Т2 мы имеем F Є Ті. Пусть есть модель 21 с универсумами Лі,... , Ап. Мы говорим, что в модели 21 определимо множество S С ASl х ... х ASk, если имеется формула F(xSi, х?22} , xskk) такая, что в таком случае мы говорим, что F определяет множество S. Если имеется определимое множество, то мы можем расширить сигнатуру модели 21 новым предикатным символом, оценкой которого будет это множество. При этом стандартным образом строится рекурсивная функция переводящая формулы расширенного языка в эквивалентные им над 21 формулы исходного. В таком случае мы говорим об определимых предикатах. Аналогично вводится понятие определимой функции.

Пусть даны модель 21 сигнатуры и\ и модель 55 сигнатуры о 2-Интерпретация модели 55 в модели 21 состоит из функции i(t) из сортов сигнатуры о"2 в сорта сигнатуры а\\ емейства, проиндексированного сортами t из 0"2, формул Щ(хг ) сигнатуры о"! для всех сортов t из о"2; семейства, проиндексированного сортами t из о"2, сюръективных функции pt из множества всех элементов универсума сорта i(t) модели 21, на которых выполняется Ut в универсум сорта t модели 55 (для каждого объекта а сорта i(t) из области области определения функции pt мы говорим, что а является интерпретацией pt(a));

Отметим, что из такого выбора естественным образом извлекается интерпретация Г, которая является интерпретацией Th( B) в Th(2l). Пусть теперь дана некоторая интерпретация Г сигнатуры о"2 в сигнатуре и\ такая, что в о"2 нет функциональных символов и интерпретации равенств в Г абсолютны. И кроме того, пусть дана модель 21 сигнатуры и\. Тогда отсюда естественным образом восстанавливается единственная, с точностью до изоморфизма, модель В сигнатуры о"2 и ее интерпретация в 21 такая, что интерпретация извлекаемая из нее совпадает с Г. Ясно, что тем самым Г задает преобразование моделей сигнатуры и\ в модели сигнатуры о"2.

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